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