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 ?On Tuesday, 11 February 2025 at 00:17:10 UTC+1 Hillel Wayne wrote: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
On 2/9/2025 11:43 AM, Frederic Marand (FGM) wrote:
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+u...@xxxxxxxxxxxxxxxx.To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7b6ef020-058b-4e4d-abf6-f427bd0785ecn%40googlegroups.com.
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.