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.