How do I use the command-line tools?

[James Fisher]

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?

[Markus Alexander Kuppe]

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

[Stephan Merz]

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

> --
> 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...@googlegroups.com.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[James Fisher]

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

[Leslie Lamport]

   It's a bit unfortunate that tlaplus.net is dead, because apparently at
   some point it was the "official" homepage, and references to it have
   made their way into books

People should know better.  I've proposed a solution to this problem,
but it's too simple and low-tech for anyone to have paid attention.
You can find it here

   http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#www9

and an example of its use is at the bottom of the TLA+ home page.

   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.

A pdf may seem "locked away", but a pdf file on the web is more likely
to look the same to all readers than an html file.  (Have you ever
come across a page with completely unreadable purple text on a black
background?  It looks fine on the author's browser.)  I have been
unable to do the simplest things in html and get them to look the same
on all browsers.  I would appreciate help from an html expert that
would allow me to improve the TLA+ web pages.  But I have seen no
evidence that there is any suitable way to put mathematical formulas
on the web other than with pdf files.

   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.

I don't know what "documentation", and "a summary" of what, you have in
mind.  In any event, man pages are of no interest to me because they
don't exist on all systems, and --help flags are meaningful only when
running a tool from a command line.  While there is some reason to use
TLC from a command line on very large specs, people should learn TLA+
and should do the initial debugging of even large specs with the
Toolbox.  Any useful documentation or summary should therefore be
accessed with the Toolbox.  I would be glad to discuss ways to make
the Toolbox more useful to beginners with anyone who volunteers to do
the work.  Licensing issues of the book should not be a problem.

Leslie