[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 16:32, Andrew Wilcox <andrew...@xxxxxxxxx> wrote:

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"?

States are assignments of values to variables, so existence of a state satisfying some condition means being able to find suitable values for the variables. Concretely, formula Next is (equivalent to)

  \/ b=0 /\ b'=1 /\ box' = ...
  \/ b=1 /\ b'=0 /\ box' = ...

Therefore, starting from any state s_n where b equals 0 or 1, one can find some state s_{n+1} such that the pair (s_n, s_{n+1}) satisfies Next.