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

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

On Saturday, February 4, 2017 at 9:34:37 AM UTC-5, Stephan Merz wrote:
In TLA+, finite behaviors are represented by infinite stuttering from the final state. See also section 6.3, which says, "the only behaviors of this algorithm are the infinite behavior ... *and any finite prefix of it*". So a behavior ending in a state s_n formally means that it loops indefinitely at that state.

OK, a behavior is a sequence of states, and for a behavior to "end" means that all future states in the behavior's sequence are the same state.  (Ignoring stuttering which comes later).  Thanks!

3. 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.

What does it means for a state such as sn+1 to "exist"?