[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: How to run TLA+ ToolBox model checking from command line?
On Tuesday, November 14, 2017 at 4:44:29 AM UTC-8, jar...@xxxxxxxxx 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?
I just have this shell script in my PATH:
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.