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

Stephan

On 9 Feb 2025, at 18:05, Frederic Marand (FGM) <fgmarand@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 Liveness

Le 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?

Stephan

On 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.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+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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5dc688b3-e417-46a8-9a43-be9e7c46c643n%40googlegroups.com.