P(self) == ncs(self) \/ e1(self) \/ e2(self) \/ cs(self) \/ f(self)
Next == (\E self \in {0,1}: P(self))
so I take Proc(i) to be P(i). P(i) will be true and enabled if any one of its disjuncts is true and enabled, so let's look at e2(i). Because both processes are stuck with pc[i] = "e2", we check whether e2(i) is true and enabled.
e2(self) == /\ pc[self] = "e2"
/\ IF ~x[1-self]
THEN /\ pc' = [pc EXCEPT ![self] = "cs"]
ELSE /\ pc' = [pc EXCEPT ![self] = "e2"]
/\ x' = x
we see that all conditions are satisfied: pc[self] does equal "e2"; x[1-self] is true, therefore we take the ELSE branch and set pc' to pc with pc[self] = "e2"; and we can set x' to x. Because there exists a valid assignment to primed variables, there exists an s -> t step for e2(i) and that's the definition of "enabled": just whether there exists a step with valid assignments.
Looks to me like e2(i) is true and enabled, so P(i) is true and enabled, so \E self in {0,1}:P(self) is true and enabled, so Next is true and enabled.
Now, it also looks to me like every step in the deadlocked suffix of the behavior is, in fact, an e2(i) step for some i.
Where did I go wrong?
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/tmUjhQTDGfc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
~\E suffix of B : \A state \in B A is enabled /\ ~\E A step.
I found it easier to think with the following, equivalent form (derived by propagating the outer negation through):
\A suffix of B : (\E state \in B : A is disabled) \/ (\E A step).
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/tmUjhQTDGfc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.