Trying to understand the answer to question 7.6, deadlock in OneBit2Processes.
We're trying to see how WF_vars(Proc(i)) is true in an infinite, stuttering behavior in which x[1-i] and (pc[i] = "e2") for i in {0,1}.
WF_vars(Proc(i)) will be true if there is no suffix of the behavior in which Proc(i) is enabled in all steps but there is no Proc(i) step.
The proposed answer simply states that <Proc(i)> is not enabled in any suffix of the behavior, therefore it does not matter than there are no Proc(i) steps. But it looks to me like Proc(i) is enabled in every deadlock step AND that every deadlock step is a Proc(i) step. I believe that WF_vars(Proc(i)) is true, but for a different reason from the stated answer. My reasoning is below and I'd be grateful if someone would point out my mistake or misunderstanding.
Proc(i) is the next-state action of process i. In the translation of the PlusCal statement of the algorithm, we see
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?