Re: How does Fairness relate to the State Graph

Thanks This is very interesting.

As the TLA+ code was generated by the PlusCal translator are you saying that the PlusCal `fair process' does not translate correctly into TLA+? Or perhaps a better way to say this is what does the PlusCal `fair process' statement mean?

I had been interpreting strong fairness to mean if an action is offered infinitely often it must be taken. If this is correct and the State graph is to be believed then surely the algorithm would terminate. Have I made some mistake or should I not treat the State Graph as accurate?

many thanks david

On Wednesday, 6 February 2019 09:38:33 UTC+13, 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