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

[ma...@xxxxxxxxx]

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?
> 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