Are you using the Toolbox or VSCode? At the time I wrote Learntla, most people were using the Toolbox, but I think it's more common for people to use the VSCode extension now (which generates default cfg files slightly differently).
H
Thanks @Stephan Merz, @Markus Kuppe : that fixed it.--
Knowing that, I can now see that the TLC config format is defined at https://learntla.com/topics/cli.html?highlight=cfg#config-format but that is later in the site that the examples depending on it, hence my error.--Le dimanche 9 février 2025 à 18:08:16 UTC+1, Stephan Merz a écrit :
Ah, I see. You should replace INIT / NEXT in the config file by
SPECIFICATION Spec
otherwise the fairness condition will not be taken into account.
Stephan
On 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 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]_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: 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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5dc688b3-e417-46a8-9a43-be9e7c46c643n%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/7b6ef020-058b-4e4d-abf6-f427bd0785ecn%40googlegroups.com.