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.
-- DOWNLOAD
THE TLA+ TOOLS -- 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/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 commandsjava 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.) |
|||