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

*From*: Philip White <phi...@xxxxxxxxxxxxx>*Date*: Wed, 6 Feb 2019 13:56:07 -0800*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com>

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>

**Follow-Ups**:**Re: [tlaplus] How does Fairness relate to the State Graph***From:*david streader

**References**:**How does Fairness relate to the State Graph***From:*david streader

- Prev by Date:
**Re: Unknown operator error during the TLA+ lectures** - Next by Date:
**Re: How does Fairness relate to the State Graph** - Previous by thread:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Next by thread:
**Re: [tlaplus] How does Fairness relate to the State Graph** - Index(es):