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 machineclosed" [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 subactions of the specification (essentially, disjuncts of the nextstate relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the nextstate 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.
