Running the TLA+ Tools Standalone

Leslie Lamport

Last modified on 21 November 2018


The Tools

The TLA+ tools are described on the TLA+ Tools web page.  Most users run the TLA+ tools from the TLA+ Toolbox.  Instructions for running TLAPS, the TLA+ proof system, should be found on its web site.  This page describes how to run the other tools outside the Toolbox.  Those tools, and their current versions, are:
   SANY:    Version 2.1  of 23 July 2017
   TLC:     Version 2.13 of 18 July 2018
   PlusCal: Version 1.8  of 16 May 2018
   TLATeX:  Version 1.0  of 20 September 2017

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 --
       -- ALTERNATE DOWNLOAD SITE --

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

Windows       [show]

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, open the   Control Panel  and click on  System.  Click on  Advanced system settings,  select the Advanced tab, and then click on Environment Variables.  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       [show]

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.)