I'm not going to fully disclose the answer since you'll have more fun finding it out yourself. Small hint: check the distinction between Proc(i) and <<Proc(i)>>_vars, and look at the precise definition of WF_vars(Proc(i)).Best regards,StephanOn 21 Feb 2014, at 12:25, Brian Beckman <bc.be...@xxxxxxxxx> wrote:You received this message because you are subscribed to the Google Groups "tlaplus" group.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 seeP(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' = xwe 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?
--
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.