Thanks for quick explanation.
"Now we can define proc(self) as the fact that one of the previous actions is being accomplished:
proc(self) == \/ a0(self) \/ a1(self) \/ a2(self) \/ a3a(self)
\/ a3b(self) \/ cs(self) \/ a4(self)
Finally, we define the Next action, as the fact that either proc is accomplished for one of the
processes, or the algorithm has finished (to prevent deadlock on termination).
Next == \E self \in {0,1}: proc(self)"
I have a few questions:
1. When TLC will check proc(self) formula? Will this happen after it checks all previous formula's from a0 to a4?
2. Will proc(self) formula be satisfied when all previous formula's satisfied (a0 to a4)?
3. Next formula is satisfied if proc(self) is satisfied where self is element of 0 and 1 (process 0 or 1). Is this correct?