Ah, I see. You should replace INIT / NEXT in the config file bySPECIFICATION Specotherwise the fairness condition will not be taken into account.StephanOn 9 Feb 2025, at 18:05, Frederic Marand (FGM) <fgma...@xxxxxxxxx> wrote:Indeed I did. What's more, I found out later that all examples after that actually fail:
- the ones about the diamond operator fails in two ways: adding Correct as in previous specs does not detect the counter=1 failure
- they do not pass with fair process or fair+ process either
- the ones about eventually always also fail, but that is expected. They do fail differently, however: it takes 10 steps to stutter with <>[] instead of 4 with just [].
FWIW, here is my CFG file:
INIT Init
NEXT Next
CONSTANT NULL = NULL
PROPERTY LivenessLe dimanche 9 février 2025 à 17:45:07 UTC+1, Stephan Merz a écrit :Just a triviality check: you did regenerate the TLA+ from your PlusCal algorithm after adding the fairness modifier?StephanOn 9 Feb 2025, at 17:33, Frederic Marand (FGM) <fgma...@xxxxxxxxx> wrote:Hello,I'm trying to understand page https://learntla.com/core/temporal-logic.html#anything-can-crash . In the "Anything can crash" section, in the part about weak fairness, the text says that this spec:https://learntla.com/_downloads/6b47d139d7a34a7d91ced863911a88dc/orchestrator.tlaWill pass because of the added "fair" modifier to the orchestrator process, which modifies the end of the spec, from this:Spec == Init /\ [][Next]_varsto:Spec == /\ Init /\ [][Next]_vars /\ WF_vars(orchestrator)or even, when using "fair+ process orchestrator, to that:Spec == /\ Init /\ [][Next]_vars /\ SF_vars(orchestrator)However, as soon as I add the `PROPERTY Liveness` to the CFG, the runs fail for "process", "fair process" and "fair+ process" for the exact same stuttering behavior that "fair" is supposed to forbid:
Error: Temporal properties were violated.
Error: The following behavior constitutes a counter-example:
State 1: <Initial predicate> _online_ = {"s1", "s2"}
State 2: StutteringAny suggestion what I could be missing here ?--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/5b6b8b3a-1418-4f63-94b3-b91c0c3d9f53n%40googlegroups.com.
--
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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/5dc688b3-e417-46a8-9a43-be9e7c46c643n%40googlegroups.com.