Oh, does "there exists" here mean existential quantification (i.e. ∃ ) ?
Correct: existential quantification over states.
The behavior does not end in a state sn if there exists a state sn+1 such that the sequence s1 → ... → 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?
Precisely.
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?
[][Next]_vars
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,
Stephan
|