TLA+ Tools

10 April 2008 Release

The big news is the beta-test version of the 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. Check it out here.

The following minor changes have been made to the current tools:

TLC Typing of model values has been added.
+CAL await has been added as a synonym for when.

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

Except for the +CAL translator, the tools are described in the book Specifying Systems. Documentation of the +CAL translator is on the +CAL web page. The current versions of these tools, on the 10 April 2008 release, are:

   TLC:     Version 2.01 of  9 April     2008 
   SANY:    Version 1.0  of 29 February  2008
   +CAL:    Version 1.3  of 10 April     2008
   TLATeX:  Version 0.95 of 21 February  2004

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: Postscript PDF

Downloading and Installing the Tools

The distribution comes as a zip file. Download the file by clicking here:

TLA+ Tools

Separate directions for completing the installation on Windows and on Unix 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. How you do that depends on what version of Windows you're using:

Non-Ancient Versions of Windows

Choose Start / Settings / ControlPanel. On the Control Panel, choose System, click on Environment, 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 .

Windows 95 (and probably Windows 98)

You must modify your AUTOEXEC.BAT file. If there is a command

         set CLASSPATH = c:\foo\bar;d:\myjava\files

then you should change it to

         set CLASSPATH = c:\foo\bar;d:\myjava\files;c:\user\myfolder\tla

If there is no such command in the file, then you should add

         set CLASSPATH = c:\user\myfolder\tla

to your AUTOEXEC.BAT file.

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 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 tlc.TLC
  java tlasany.SANY
  java pcal.trans
  java tlatex.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.)