| Hi Ron, your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering. The TLA+ specification x ∈ Nat ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100]_<<x,t>> has behaviors where x initially holds an arbitrary natural number, and t and x get incremented until t hits 100, at which point only stuttering is possible. So it cannot be equivalent to the TLA+ specification x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1]_<<t,x>> A similar observation holds for (the TLA+ version of) the third specification x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ (t = 100 ⇒ x = 100)]_<<x,t>> You can force the equivalence of the specifications by adding the conjunct ⬦(t > 100) and this observation shows that liveness conditions may sometimes constrain the safety part of the specifications. Such specifications are known as "not machine-closed" [1], and are hard to reason about. (You'd have to prove the invariant ☐(x=t), but this requires temporal logic reasoning since you must appeal to the liveness condition to show that the execution would be blocked when t hits 100.) The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation. Best regards, Stephan [1] M. Abadi, L. Lamport. The existence of refinement mappings. TCS 81(2), 1991. See also section 8.9.2 of Specifying Systems.
|