Understanding Question 7.6

[Brian Beckman]

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?

[Stephan Merz]

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,

Stephan

--
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.

[Brian Beckman]

awesome :)  digging in . . .

[Brian Beckman]

Ok, I got it. I won't reveal the details either (in case someone else wants to dig in, too), but will add the hint that Section 6.7.2. has all the details.

--
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.

[Brian Beckman]

I'll also add the subjective point that I found it easier to reason by transforming definitions as follows. The various candidate definitions of weak fairness all have the form, letting A be some action and B being some behavior:

~\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.