Re: [tlaplus] How do I use the command-line tools?

[Stephan Merz <Stepha...@xxxxxxxxx>]

Hi,

you'll find a description of the command-line tools in the book "Specifying Systems". The TLA Web page also contains a note on the differences of the current versions from what is described in the book. Unfortunately, there is no option to print the full set of available options.

In practice, I recommend making an alias for invoking the command-line tools with default options set at your convenience. For example, I have

alias tlc='java -Xmx512m -cp /usr/local/tla tlc2.TLC -workers 2 -metadir /tmp/TLC'

for invoking the TLC model checker from the command line.

Regards,
Stephan


> On 17 Nov 2014, at 23:02, James Fisher <jamesh...@xxxxxxxxx> wrote:
> 
> I initially downloaded the .jar file, but couldn't figure out how it is meant to be used. This is what I tried:
> 
>> java -jar ~/bin/tla2tools.jar 
> no main manifest attribute, in /Users/jhf/bin/tla2tools.jar
> 
> I then downloaded the .zip file, and, following the instructions, tried:
> 
>> java -cp . tla2sany.SANY -help
> Illegal switch: -help
>> java -cp . tla2sany.SANY --help
> Illegal switch: --help
>> java -cp . tla2sany.SANY help
> 
> ****** SANY2 Version 2.1 created 24 February 2014
> 
> Cannot find the specified file help.
> 
> Okay, so the website describes the CLI as "one of these commands ... followed by the command arguments, which consist of zero or more switches followed by the name of a  .tla  file." So ... what are those switches? Where is the documentation?
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.