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

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 17.11.2014 23:02, James Fisher 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?


Hi James,

not sure it helps, but you find all switches in the source code [1].

-S/-s: semantic analysis should be done
-L/-l: level checking should be done
-D/-d: control should be transferred to debugger
-STAT/-stat: statistics about builtin operator usage

Hope this helps,
Markus

[1]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tla2sany/drivers/SANY.java