[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



(* --fair algorithm counter

variable x = 0, y = 0;

fair+ process counter = "counter"

begin Count:

  while (x<Size) do


  await (x<Size);

  \* upx:+

    x := x + 1;


 \*  upy:+

    y := (y + 1)%Size;

  end either;    

 end while;

end process;

end algorithm; *)


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