[tlaplus] LearnTLA+ "anything can crash" not fixed by fairness

["Frederic Marand (FGM)" <fgmarand@xxxxxxxxx>]

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.tla

Will pass because of the added "fair" modifier to the orchestrator process, which modifies the end of the spec, from this:

    Spec == Init /\ [][Next]_vars

to:

    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: Stuttering

Any 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5b6b8b3a-1418-4f63-94b3-b91c0c3d9f53n%40googlegroups.com.