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

[Philip White <phi...@xxxxxxxxxxxxx>]

David, what tool(s) did you use to make the graph you attached to this email?

Thanks.

> On Feb 5, 2019, at 12:38 PM, david streader <davidis...@xxxxxxxxx> 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
> 
> -- 
> 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.
> <fairWorking1.pdf>