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

Re: [tlaplus] How does Fairness relate to the State Graph

If you look at your state graph, you see that there are loops between states where x remains unchanged (either 0 or 1) but y oscillates between 0 and 1. These loops correspond to "counter" (and therefore also "Next") actions, and therefore your fairness conditions are satisfied in an execution that remains in one of these loops forever, hence non-termination is possible. Substituting strong fairness for weak fairness doesn't make any difference in this example.


On 5 Feb 2019, at 21:38, david streader <davidis...@xxxxxxxxx> 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")

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.