On Saturday, November 19, 2016 at 10:23:02 AM UTC+2, Stephan Merz wrote:
your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering...
Oh! Of course!
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.)
Ah, so does machine closure in addition to stuttering invariance place constraints on internal nondeterminism? My cursory reading of machine closure made me believe that in order for it to be violated, the liveness requirement would need to explicitly contain "safety subformulas", but I guess this is an example where this is not the case.
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.
Does that guarantee, then, that formulas with different nondeterminism would admit different behaviors and could be distinguished?
Ron