How to run TLA+ ToolBox model checking from command line?

[jarr...@gmail.com]

I write a TLA+ script, but it seems too slow for model checking in my laptop, even in the multithread mode. So I want to run it in a Linux server which do not have a GUI. Anybody know how to run model checking from command line?
Thx.

[Stephan Merz]

Hi Jarry,

at the bottom of the TLA+ tools page [1] you'll find a short description on how to use the tools from the command line. If you have any questions that are not answered there, please come back here.

Regards,
Stephan

[1] http://lamport.azurewebsites.net/tla/tools.html

> On 14 Nov 2017, at 13:42, jarr...@gmail.com wrote:
>
> I write a TLA+ script, but it seems too slow for model checking in my laptop, even in the multithread mode. So I want to run it in a Linux server which do not have a GUI. Anybody know how to run model checking from command line?
> Thx.
>

> --
> 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 post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[ma...@lytics.io]

On Tuesday, November 14, 2017 at 4:44:29 AM UTC-8, jarr...@gmail.com wrote:
> I write a TLA+ script, but it seems too slow for model checking in my laptop, even in the multithread mode. So I want to run it in a Linux server which do not have a GUI. Anybody know how to run model checking from command line?
> Thx.

Hi Jarry,

I just have this shell script in my PATH:


#! /bin/bash

export CLASSPATH=/home/marek/tla

java tlc2.TLC $@


I can then run the checker like so:

$ tlc DieHard.tla
TLC2 Version 2.08 of 21 December 2015
Running in Model-Checking mode.
Parsing file DieHard.tla
Parsing file /home/marek/tla/tla2sany/StandardModules/Integers.tla
Parsing file /home/marek/tla/tla2sany/StandardModules/TLC.tla
Parsing file /home/marek/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /home/marek/tla/tla2sany/StandardModules/Sequences.tla
...


The directory /home/marek/tla is just the unarchived java files of the tools:

$ ls /home/marek/tla/
com examples javax License.txt META-INF model pcal README tla2sany
tla2tex tla2tools.jar tlc2 util


I hope that is helpful.

-Marek

[jarr...@gmail.com]

Hi, Stephan

I run the raft protocol specification from Diego Ongaro's Ph.D. dissertation. Now I use a server and run 20 threads in parallel. After 3 hours, it still keeps running.

How can I estimate how long will it take for a complex spec. Or how to reduce the time consuming? 

PS: The symmetry sets optimization does not help a lot.