The ToolsThe 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 ToolsThe 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.
Separate directions for completing the installation on Windows and on Unix from the zip file are given below.
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 .
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/tlaHowever, 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 ToolsTo 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.TLAfollowed 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.)