Distributed model-checking

[A. Jesse Jiryu Davis]

Hello, I have one of those monster models that would benefit from distributed model checking on multiple machines. Years ago I recall that the TLA+ Toolbox could spread work across servers, and it would even set up servers in AWS for me. I found this page on the subject, but it seems old (the page isn't dated). In my version of the toolbox (1.7.1) I see no "Run in distributed mode" option. Is distributed mode still supported in the Toolbox? Can I use distributed mode from the command line or the VSCode extension?

[Markus Kuppe]

Hi Jesse,

there have been no reported issues, and nothing is fundamentally broken with either Distributed TLC or Cloud TLC. However, we no longer have sponsored access to AWS to run Cloud TLC as part of our CI testing. Additionally, cloud providers often change their APIs, and the jclouds library [1] that Cloud TLC depends on has not been updated in a while. The dropdown menu for selecting the cloud has been moved in the Toolbox’s nightly build (see attached screenshot). Distributed TLC can be used from the command line [2], but there is no support in the VSCode extension.

We've found that TLC’s simulation mode is very effective at finding counterexamples. For instance, simulation mode found a variant of a counterexample in about 10 minutes, which took model checking two days to find. I recommend running TLC in simulation mode on a multi-core machine for an extended period before attempting large-scale exhaustive model checking on a single machine or using distributed model checking.

Markus

PS: The HTML page you linked to is part of the Toolbox. You can find its history in our git repo [3].

[1] https://jclouds.apache.org <https://jclouds.apache.org/> and https://github.com/lemmy/jclouds2p2
[2] https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/distributed-mode.html
[3] https://github.com/tlaplus/tlaplus/tree/master/toolbox/org.lamport.tla.toolbox.doc/html/

[A. Jesse Jiryu Davis]

Thanks for the quick answer as usual Markus, this is helpful. I'll try simulation mode.

Is there a way to prevent TLC from outputting a trace file for successful runs (runs without invariant violations)? I want to run a lot of simulations to ease my anxiety about deeply-hidden bugs, e.g.:

java -jar tla2tools.jar -simulate num=100000,file=output_dir/ mcMySpec.tla -workers 8 -cleanup -deadlock

This produces num * workers = 800000 traces, and the output_dir/ directory grows very large. On macOS it takes a lot of disk space and it takes a very long time to delete! I want to output a trace only if/when there's an invariant violation.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/89F9C339-1C8A-459C-A7BC-79FA5BB37F00%40lemmster.de.

> On Jul 3, 2024, at 6:26 AM, A. Jesse Jiryu Davis <je...@emptysquare.net> wrote:
>
> Hello, I have one of those monster models that would benefit from distributed model checking on multiple machines. Years ago I recall that the TLA+ Toolbox could spread work across servers, and it would even set up servers in AWS for me. I found this page on the subject, but it seems old (the page isn't dated). In my version of the toolbox (1.7.1) I see no "Run in distributed mode" option. Is distributed mode still supported in the Toolbox? Can I use distributed mode from the command line or the VSCode extension?

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/89F9C339-1C8A-459C-A7BC-79FA5BB37F00%40lemmster.de.

[Markus Kuppe]

Hi Jesse,

TLC won't serialize the generated traces if you run it without (the optional) `file=output_dir`. The purpose of the `file` sub-command is to serialize traces if one wants to post-process them with third-party tools or subsequent TLC runs.

Markus

[A. Jesse Jiryu Davis]

Ah, and it seems like simulation mode stops and prints a trace if it finds a violation, with a nonzero exit code. Perfect, thanks!

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/C1529442-1659-4E86-AB1C-2B30239A737A%40lemmster.de.

[Markus Kuppe]

Note that TLC’s simulation mode also supports the `-continue` parameter, which causes the simulation to continue even after finding and printing an invariant violation.

M.