Hi Stephan and Markus,
Thanks for the info. I'd be happy to contribute to the project to improve the documentation for the command-line tools. It might not be a popular sentiment with the inventor of LaTeX, but things in PDFs seem "locked away" compared to being on the web.
Low-hanging fruit for improvement IMO:
1. Add the TLA+ tools to common package managers.
2. Include aliases like yours in the package.
3. Port the documentation in Specifying Systems and its errata to some man pages.
4. Add a summary in a --help flag.
(3) and (4) are awkward due to licensing issues of the book.
(BTW, has anyone figured out how the .jar is supposed to be used?)
James
On Tuesday, November 18, 2014 12:28:20 PM UTC, Stephan Merz wrote:
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 <jame...@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...@googlegroups.com.
> 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.