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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 7 Feb 2019 09:34:17 +0100*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com> <d3d52ebe-da60-4b4e-ac07-ee2f6fad90b8@googlegroups.com>

Hi David,
As Leslie and Ron say, it is easy to express the desired effect in TLA+, and you can just add a fairness condition to that effect to the TLA+ spec that the PlusCal translator generates. See the module below. TLC will now confirm termination (remember to change "Spec" to "FairSpec" in "What is the behavior spec"). In fact, just adding WF_x(counter) to the default fairness condition is enough for this to hold. Regards, Stephan ------------------------------ MODULE Counter ------------------------------ EXTENDS TLC, Integers CONSTANT Size (* --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(counter) Termination == <>(\A self \in ProcSet: pc[self] = "Done") \* END TRANSLATION (***************************************************************************) (* The following condition states that control should not remain at label *) (* "Count" while leaving either x or y unchanged forever. *) (***************************************************************************) XYFair == WF_x(counter) /\ WF_y(counter) FairSpec == Spec /\ XYFair =============================================================================
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+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

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

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

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