LearnTLA+ "anything can crash" not fixed by fairness

[Frederic Marand (FGM)]

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 ?

[Stephan Merz]

Just a triviality check: you did regenerate the TLA+ from your PlusCal algorithm after adding the fairness modifier?

Stephan

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

[Frederic Marand (FGM)]

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

[Markus Kuppe]

Replace INIT and NEXT with SPECIFICATION Spec (assuming Spec == Init /\ [][Next]_vars).

M.

[Stephan Merz]

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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5dc688b3-e417-46a8-9a43-be9e7c46c643n%40googlegroups.com.

[Frederic Marand (FGM)]

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.

[Hillel Wayne]

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

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7b6ef020-058b-4e4d-abf6-f427bd0785ecn%40googlegroups.com.

[Frederic Marand (FGM)]

Actually, I use TLC and the IntelliJ plugin.

I also noticed that on the TLA+ page https://www.learntla.com/core/tla.html the basic clock example and the second one work but I had to stop the non-deterministic example at https://www.learntla.com/_downloads/148bdcbbec03267f2a9e389fc05ff863/hourclock.tla after 250M states found.

Here is a trace of a shorter TLC run:

tlc core11_3_clock_with.tla
TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
Running breadth-first search Model-Checking with fp 109 and seed 5122784111867585607 with 1 worker on 11 cores with 4096MB heap and 64MB offheap memory [pid: 26303] (Mac OS X 15.3.1 aarch64, Homebrew 23.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /<readacted>/core11_3_clock_with.tla
Parsing file /private/var/folders/_n/tb20d08d6p327llpm9yjvs1w0000gn/T/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module core11_3_clock_with
Starting... (2025-02-11 12:57:54)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2025-02-11 12:57:54.
Progress(3648672) at 2025-02-11 12:57:57: 14,594,664 states generated (14,594,664 s/min), 7,297,282 distinct states found (7,297,282 ds/min), 1 states left on queue.

Since the CFG is so important, it might make sense to consider adding it to all the downloadable specs ?

This email, including any attachments, is confidential and may be privileged. If you are not the intended recipient please notify the sender immediately, and please delete it; you should not copy it or use it for any purpose or disclose its contents to any other person. If the email, including any attachments, is legally privileged, you should not forward it to any other person.

[Frederic Marand (FGM)]

FWIW, modifying the algorithm from "if hr = 12 then" to "if hr >= 12 then" passes, because in the original version, incrementing by any behaviour combining 1 and 2 will never finish because it will skip 12.

[Hillel Wayne]

Could you submit this as an issue in the repo? I'm currently swamped with another project, but I'll be coming back to fix and improve learntla later this year.

H

This email, including any attachments, is confidential and may be privileged. If you are not the intended recipient please notify the sender immediately, and please delete it; you should not copy it or use it for any purpose or disclose its contents to any other person. If the email, including any attachments, is legally privileged, you should not forward it to any other person. --

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...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/a1f1c1d7-935a-4912-96ae-96c3e7447291n%40googlegroups.com.

[Frederic Marand (FGM)]

Done: https://github.com/hwayne/learntla-v2/issues/91