TLA+ | The way to specify

This tutorial provides a description of the installation procedure of the console-based version of TLA+ Tools. Separate directions for completing the installation on Windows and on Unix are provided.
Please download the latest copy of the TLA+ Tools in the Tools Section. Also make sure that the Java Runtime Environment (at least version 1.4) is installed on your machine. You can download a version from the homepage of Sun Microsystems.

Installation on Windows

Choose (or create) a folder into which you want to put the tools and unzip the downloaded file into it. Suppose your folder is c:\user\myfolder, the sub folder named tla will be created in it, which contains the tools. Add c:\user\myfolder\tla to your CLASSPATH environment variable. How you do that depends on what version of Windows you’re using:

Non-Ancient Versions of Windows

Open Start > Settings > ControlPanel. On the Control Panel, open System, click on Advanced tab and open the Environment Variables, then look for the CLASSPATH variable among user or system variables. If it exists, append ;c:\user\myfolder\tla to the end of its value. If not, create a new CLASSPATH variable whose value is c:\user\myfolder\tla.

Windows 95 (and MS-DOS)

Modify your AUTOEXEC.BAT file. If there is a command
set CLASSPATH = c:\foo\bar;d:\myjava\files
then 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 add
set CLASSPATH = c:\user\myfolder\tla
to your AUTOEXEC.BAT file.

Installation on UNIX

Choose (or create) a directory into which you want to put the tools and unzip the downloaded file into that directory. Suppose that your directory is /udir/user/mydir, the sub directory named tla will be created in it, which contains the tools. 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

Validation of the installation

In order to validate if the TLA+ tools has been successfully installed, first create a file test.tla and paste the following content into it:

---- MODULE test ----
====

Then open the console (Start > Run > cmd on Windows) in the directory, the file is located in and type: java tla2sany.SANY test. If you did everything right, you should see:

****** SANY2 Version .91 created 10 April 2008
Parsing file test.tla
Semantic processing of module test

If you see

Exception in thread "main" java.lang.NoClassDefFoundError: tla2sany/SANY
Caused by: java.lang.ClassNotFoundException: tla2sany.SANY
        at java.net.URLClassLoader$1.run(URLClassLoader.java:200)
        at java.security.AccessController.doPrivileged(Native Method)
        at java.net.URLClassLoader.findClass(URLClassLoader.java:188)
        at java.lang.ClassLoader.loadClass(ClassLoader.java:307)
        at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:301)
        at java.lang.ClassLoader.loadClass(ClassLoader.java:252)
        at java.lang.ClassLoader.loadClassInternal(ClassLoader.java:320)
Could not find the main class: tla2sany.SANY.  Program will exit.

you probably misspelled the CLASSPATH. If you see something like:

'java' is not recognized as an internal or external command,
operable program or batch file.

you are missing the JRE.

Running from a script

In some scenarios, setting up the global CLASSPATH variable is not desirable. In this case it is possible to create scripts for each tool which set the CLASSPATH only for the execution. Here is an example script for calling SANY on Windows:

set TLA_PATH=c:/tools/tla2
java -cp %TLA_PATH% tla2sany.SANY %1 %2 %3 %4

The script should be invoked with the name of the TLA file.