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

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

On Thursday, April 13, 2017 at 3:13:51 PM UTC-7, Leslie Lamport wrote:
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

On Thursday, April 13, 2017 at 11:15:04 AM UTC-7, xmzhou@... wrote:
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