How does Fairness relate to the State Graph

[david streader <davidis...@xxxxxxxxx>]

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

Attachment: fairWorking1.pdf
Description: Adobe PDF document