# Re: [tlaplus] Understanding Question 7.6

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

On Friday, February 21, 2014 12:41:05 PM UTC-8, Brian Beckman wrote:
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.

On Fri, Feb 21, 2014 at 10:23 AM, Stephan Merz wrote:
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

On 21 Feb 2014, at 12:25, Brian Beckman <bc.be...@xxxxxxxxx> wrote:

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?

--
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+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.