Running the TLA+ Tools Standalone

   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

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/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

  java tlc2.TLC
  java tla2sany.SANY
  java pcal.trans
  java tla2tex.TLA