Re: [tlaplus] Nondeterminism and equivalence

[Stephan Merz <stepha...@xxxxxxxxx>]

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.

Not sure I understand your question but allow me to reformulate. The liveness requirement filters out behaviors that would be perfectly acceptable for the safety part of the specification. The idea of machine closure is that the state machine executing the safety part of the specification does not need "prescience" in order to make those choices that will be compatible with the liveness condition: any choice allowed by the next-state relation can be completed to an infinite behavior satisfying the overall specification, using a fair scheduler. A machine-closed specification does not place any constraints on internal non-determinism, whereas non machine-closed specifications may have such constraints.

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?

Morally, yes, assuming that the different choices are actually possible based on the safety part (think invariants). For example, the following (trivially machine-closed) variation of your example

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((x < 0 ∧ x'=x-1) ∨ x’ = x + 1)]_<<t,x>>

allows for an apparent choice of decrementing x that cannot be realized due to the invariant ☐(x > 0).

Stephan