TLA+ Tools

The Toolbox

Most users of TLA+ will now use the TLA Toolbox. The TLA+ tools come with the Toolbox and are run from it. This page is of interest mainly to those who want to use the TLA+ tools outside the Toolbox, from a command-line interface.

TLA+2

The original version of TLA, has been retired. The current version of TLA is now TLA+2 tools. TLA+2 is a new version of TLA+ with additional features that are mostly for writing proofs. One new feature that is useful for writing ordinary specifications is the ability to write recursive operator definitions.

What are the TLA+ Tools?

TLA+ is a language for writing TLA specifications. See the TLA web page or the book Specifying Systems to find out about TLA and TLA+. A new TLA+ Hyperbook is being written. It provides what is hopefully a gentler introduction to TLA+. There are four TLA+ tools available, each described with its own web page:

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.
The PlusCal Translator: A translator from the PlusCal algorithm language to TLA+.
TLATeX: A program for typesetting TLA+ specifications.

Except for the PlusCal translator, the tools are described in the book Specifying Systems. Documentation of the PlusCal translator is on the PlusCal web page. The current versions of these tools are:

   TLC:     Version 2.05 of 24 October 2012
   SANY:    Version 2.1  of 22 February 2013
   PlusCal: Version 1.8  of 18 August 2012
   TLATeX:  Version 1.0  of 21 February 2013

These 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 this document:

Current Versions of the TLA+ Tools

Downloading and Installing the Tools

The distribution comes as a zip file or a jar file. They are available by following the link below. Please thank Microsoft and HP for the open-source release of the code by reading the following agreement.

By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license. Read the license.

-- DOWNLOAD THE TLA+ TOOLS --

Separate directions for completing the installation on Windows and on Unix from the zip file are given below.

WINDOWS

Choose (or create) a folder into which you want to put the tools and unzip the downloaded file into that folder. Let's suppose that your folder is c:\user\myfolder . This will create a subfolder of myfolder named tla that has three subfolders, each containing one of the tools. You must then add c:\user\myfolder\tla to your CLASSPATH variable. To do that, choose Start / ControlPanel. On the Control Panel, choose System, then click on Advanced and then Environment Variables, then look for the CLASSPATH variable. If it exists, append ;c:\user\myfolder\tla to the end of it. If not, create a new CLASSPATH variable whose value is c:\user\myfolder\tla .

UNIX

Choose (or create) a directory into which you want to put the tools and unzip the downloaded file into that directory. Let's suppose that your directory is /udir/user/mydir . This will create a subdirectory of mydir named tla that has three subdirectories, each containing one of the tools. You must now add /udir/user/mydir/tla to the CLASSPATH environment variable. Assuming you're running the C shell or some derivative, you do this by typing

      setenv CLASSPATH /udir/user/mydir/tla

However, you'll probably want to have the CLASSPATH variable set automatically when you login. To do this, your .login or .csh file must contain a command to set that variable. If a command

      setenv CLASSPATH ...

already exists in your .login or .csh file, just add the command

      setenv CLASSPATH $CLASSPATH":/udir/user/mydir/tla"

after it. Otherwise, just add the command

      setenv CLASSPATH /udir/user/mydir/tla

Running the Tools

To run the tools, you must have Java installed on your machine. If you're running Unix, it is probably already there. If you're running Windows, you can get Java here or here. After installing the tools and Java, you run them in a Windows Command Prompt window or in a Unix shell by typing the appropriate one of these commands

  java tlc2.TLC
  java tla2sany.SANY
  java pcal.trans
  java tla2tex.TLA

followed by the command arguments, which consist of zero or more switches followed by the name of a .tla file. (The extension .tla can be omitted when typing the file name.)