Re: [tlaplus] Distributed model-checking

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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/


-- 
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 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 <jesse@xxxxxxxxxxxxxxx> 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/89F9C339-1C8A-459C-A7BC-79FA5BB37F00%40lemmster.de.