The package: tlaps-1.4.3-i686-linux-gnu-inst.bin

1. Install the Proof System

You may have to change the installer's permissions with the following command-line:

$ chmod a+x tlaps-1.4.3-i686-linux-gnu-inst.bin

In order to install the proof system into /usr/local, run the installer as:

$ sudo ./tlaps-1.4.3-i686-linux-gnu-inst.bin

If you want to install it in some other directory dir, run:

$ sudo ./tlaps-1.4.3-i686-linux-gnu-inst.bin -d dir

(you will have to enter an administrator password)

This will install the tlapm binary in dir/bin and some other data in dir/lib/tlaps, including the zenon, isabelle, cvc3, ls4, and translate binaries.

2. Set the toolbox's library path

We strongly recommend that you install the Toolbox (version 1.4.7 or later). You will need to add the location of the TLAPS.tla file to the list of libraries used by the Toolbox. To do this, open the Toolbox and go to "File > Preferences > TLA+ Preferences". Add the directory where TLAPS.tla is located to the list of library path locations. If you have the default installation, this directory is /usr/local/lib/tlaps/.

3. Copy the example files

You will find some example files in /usr/local/lib/tlaps/examples (or in dir/lib/tlaps/examples), but you cannot open these files directly with the Toolbox because you do not have write permission to them. You should copy the files to your home directory and open the copies.


To uninstall TLAPS, run:

$ `tlapm --where`/un-inst

The uninstaller for an existing version of TLAPS is automatically run when the TLAPS installer (for any version of TLAPS, including the same version) tries to install into the same location. Because of this, never store any important files in the location where TLAPS is installed.