Re: How does Fairness relate to the State Graph

The TLA+ spec (and therefore, the PlusCal algorithm) is not live (will not terminate) due to (1) the boldened part, and (2) there is no way to specify any fairness assumption of the red part.

Count == /\ pc["counter"] = "Count"

/\ IF (x < Size)

THEN /\ \/ /\ (x<Size)

/\ x' = x + 1

/\ y' = y

\/ /\ y' = (y + 1)%Size

/\ x' = x

/\ pc' = [pc EXCEPT !["counter"] = "Count"]

ELSE /\ pc' = [pc EXCEPT !["counter"] = "Done"]

/\ UNCHANGED << x, y >>

The following terminates under correct fairness assumptions. The difference is to split Count into its 3 disjuncts and specify Strong Fairness of Count1 which increments x. However, I'm not an expert in PlusCal, so I don't know the best algorithm that specifies this.

Count1 == /\ pc["counter"] = "Count"

/\ (x<Size)

/\ x' = x + 1

/\ y' = y

/\ pc' = [pc EXCEPT !["counter"] = "Count"]

Count2 == /\ pc["counter"] = "Count"

/\ (x<Size)

/\ y' = (y + 1)%Size

/\ x' = x

/\ pc' = [pc EXCEPT !["counter"] = "Count"]

Count3 == /\ pc["counter"] = "Count"

/\ ~(x<Size)

/\ pc' = [pc EXCEPT !["counter"] = "Done"]

/\ UNCHANGED << x, y >>

counter == Count1 \/ Count2 \/ Count3

Next == counter

\/ (* Disjunct to prevent deadlock on termination *)

((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars

/\ WF_vars(Next)

/\ SF_vars(Count1)

Best,

Saksham

On Tuesday, February 5, 2019 at 3:38:33 PM UTC-5, david streader wrote:

Hi
I wrote a simple Process that my intuition tells me under a strong fairness assumption will terminate (included below). The State graph (attached) also informally confirms that under strong fairness the loops will all exit and the process will terminate.

TLC fails the Termination check. I am interested in what I can do to remedy this?

I tried editing /\ WF_vars(Next)  to /\ SF_vars(Next) but to it did not change anything.

The Error Trace is simply two Count steps that form a loop. But with the specification /\ SF_vars(counter)  I think this should not stop the Termination.

Hopefully I have missed something simple?

kind regards david

EXTENDS TLC, Integers
CONSTANT Size
(* --fair algorithm counter
variable x = 0, y = 0;

fair+ process counter = "counter"
begin Count:
while (x<Size) do
either
await (x<Size);
\* upx:+
x := x + 1;
or
\* upy:+
y := (y + 1)%Size;
end either;
end while;
end process;

end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES x, y, pc

vars == << x, y, pc >>

ProcSet == {"counter"}

Init == (* Global variables *)
/\ x = 0
/\ y = 0
/\ pc = [self \in ProcSet |-> "Count"]

Count == /\ pc["counter"] = "Count"
   /\ IF (x<Size)
   THEN /\ \/ /\ (x<Size)
/\ x' = x + 1
/\ y' = y
   \/ /\ y' = (y + 1)%Size
/\ x' = x
/\ pc' = [pc EXCEPT !["counter"] = "Count"]
   ELSE /\ pc' = [pc EXCEPT !["counter"] = "Done"]
/\ UNCHANGED << x, y >>

counter == Count

Next == counter
   \/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
/\ SF_vars(counter)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION