Hourly clock spec: why it needs the temporal-logic operator box []

[xmz...@gmail.com]

Hi All,

In the page 16 of TLA+ book, it writes:
"To express (ii), we use the temporal-logic operator [] (pronounced box). the temporal formula []F asserts that formula F is always true."

HC == HCini /\ [][HCnxt]_hr

Also in the spec, HCnxt == hr' = IF hr# 12 THEN hr + 1 ELSE 1.

The next step relation is defined as the above formula., which by definition is always true. So my question is that why the spec needs the temporal-logic operator box to assert the next step relation is always true.

I just started reading the book and has zero knowledge of temporal logic. And the box operator looks very confusing to me. As the initial condition and the next step relation seem to be enough to define the behavior.

Thanks a lot,

Xiaoming

[Leslie Lamport]

You say that HCnxt is, by definition, always true.  By that reasoning, if the spec had defined HCini to equal hr = 1, would that always be true?  How would you specify an hour clock that had to begin with hr = 1?  And if I were to write the definition

   FalseTheorem == 1+2 = 4

would that mean that 1+2 = 4 is always true?  What is the difference between a definition and a theorem?

[xmz...@gmail.com]

Thank you very much for your answer.

Maybe I am not clear in my question. I can understand the spec. But I am just wondering where the box operator comes from.

In state equations of a physical system or in an automaton, two things are given, the initial state and the function to map the current state to the next state.

Initial state: hr = 1

Next state relation: hr' = IF hr # 12 THEN hr + 1 ELSE 1

The system starts in the initial state and the next state relation defines how the system evolves. Since the system follows this law, therefore the law is true.

Just wondering why there is a difference between TLA+ spec and the typical automaton definition.

Regards,

Xiaoming 

[Leslie Lamport]

Hi Xiaming,

TLA+ differs from the methods of specifying systems with which you're familiar because it describes the system with a single mathematical formula.  It does that by using formulas of temporal logic, which is an extension of ordinary math obtained by adding the [] operator.  The initial predicate and the next-state action are enough to define the behavior if you are only describing safety and not liveness properties.  For example, the specification  HCini /\ [][HCnxt]_hr  allows behaviors that stop at any point, as well as behaviors that continue forever.    The methods you are familiar with probably don't allow you to specify general liveness properties.  Most methods make the mistake of automatically assuming the liveness property that a specification such as the one given by HCIni and HCnxt does not allow behaviors that halt.  I won't explain here why that's a mistake.  In TLA+, to specify that the clock never stops, you have to add another conjunct to HC to assert that liveness requirement.  Unlike the methods you're probably familiar with, TLA+ provides a simple and powerful way to express the wide variety of liveness requirements that one wants concurrent systems to satisfy.  In general, those liveness requirements are expressed by conjoining to the formula  Init /\ [][Next]_vars  an expression defined in terms of the [] operator. 

Leslie

[xmz...@gmail.com]

Hi Leslie,

Thanks a lot for this explanation. As you pointed out, I didn't get the liveness the formula specifies.

Thanks for this different perspective. Really appreciated.

Regards,

Xiaoming