[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] What does it mean for a behavior to "end"?

On 4 Feb 2017, at 18:43, Andrew Wilcox <andrew...@xxxxxxxxx> wrote:

Oh, does "there exists" here mean existential quantification (i.e. ∃ ) ?

Correct: existential quantification over states.

The behavior does not end in a state sif there exists a state sn+1 such that the sequence s→ ... → sn+1 also satisfies condition 2.

Ah, so "state sn+1" refers not to the next state in the behavior, but to some state which satisfies condition 2?


How does this help?  Suppose the behavior is safe (it satisfies condition 2), and has also ended, so the behavior's next state (as well as all of its other future states) is the same state as s_n.  What prevents me from choosing s_n as the state to use as the s_{n+1} state here?  After all, it satisfies condition 2, and so would trivially make all safe behaviors weakly fair... what am I missing?

The stuttering transition s_n -> s_n (trivially) satisfies [Next]_vars, but it doesn't satisfy Next. In fact, the safety part of the specification has


so every transition must either satisfy Next or leave vars unchanged, but WF_vars(Next) requires that some transition satisfying

  << Next >>_vars

(i.e., satisfying Next and changing vars) must eventually occur provided some such transition remains always enabled. The description in section 6.4 somewhat glosses over the precise definitions and appears to have lost you.

Hope this helps,