Re: How does Fairness relate to the State Graph

Everything is correct from TLA+ and PlusCal. You are specifying (in PlusCal) that Count is fair. So, TLA+ is assuming that. This means (in case of strong fairness) if Count is enabled infinitely often, it is executed infinitely often. This is true for the behavior in which the system only executes the purple part of the specification, and never the red part. This is possible because you never mentioned to execute the red part infinitely often and if you run TLC with Size 2, that is exactly what you get.

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

This is also captured by the State graph. The blue arrows forming an infinite cycle between states (x=0,y=0) and (x=0,y=1) for example.

On Tuesday, February 5, 2019 at 6:23:49 PM UTC-5, david streader wrote:

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