The TLA Tools
What are the TLA Tools?
There are following TLA tools available:
- The SANY Syntactic Analyzer: A parser and syntax checker for TLA+ specifications.
- TLC: A model checker and simulator for a subclass of “executable” TLA+ specifications.
- TLATeX: A program for typesetting TLA+ specifications.
- The PlusCal Translator: A translator from the PlusCal algorithm language to TLA+.
The first three tools are described in the book Specifying Systems. The manual for the PlusCal translator is accessible on the book page.
Important Note: The latest versions of the TLA Tools have been incorporated in the new TLA Toolbox. The version now available for separate download is an older one that will soon be updated. As part of the update, the version of TLA+ now called TLA+2 will become the standard version of TLA+. We expect that every spec that anyone has written in the original version of TLA+ will be correct in the new version, and that the new tools will still work on it. (The only problem that might occur with non-negligible probability is that an identifier used in the spec is one of the handful of new keywords added to the language.)
The current versions differ somewhat from the ones described in the book. In particular, several features have been added to TLC. The known differences are described in the document Release Notes.
tlatools-release-notes.pdf (June 06, 2009)
System requirements
In order to be able to run TLA+ Tools, the Java Runtime Environment (version 1.4 or newer) has to be installed on the computer. In order to be able to use TLATeX, the installation of LaTeX is required.
Download and Install
The distribution comes as a zip file. Download the version from Microsoft Research server:
TLA+ Tools (April 10, 2008)After downloading the file, unzip it. This will create the tla sub directory. Add an entry to the the CLASSPATH environment variable pointing to the newly created tla directory. A more detailed instructions are described in the How to Install TLA+ Tools tutorial are available in the Tutorial section.
Run
In order to run a tool the following has to be typed onto the console:
java TOOLNAME [SWITCHES] FILENAME
where TOOLNAME is one of tlasany.SANY, pcal.trans, tlatex.TLA, tlc.TLC, SWITCHES are optional, tool-dependent switches and FILENAME the name of the TLA+ file contaning the specification (with or without extension). For further information please consult the Command Line Switches tutorial, available in the Tutorial section.
