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

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

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

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?