Mac OS X (10.7 and later)

The package: tlaps-1.4.3-i386-darwin-inst.bin

1. Install   make

make is required. You can install either Apple's version from the Apple developer tools (Xcode is available for free in the Mac App store), or the GNU version via MacPorts or Homebrew, or from source

2. Install the Proof System

Do not try to run the installer by clicking it.

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

$ chmod a+x tlaps-1.4.3-i386-darwin-inst.bin

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

$ sudo ./tlaps-1.4.3-i386-darwin-inst.bin

(you must have an administrator account, and you will have to type your password)

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

It is not recommended to install the proof system in another directory. If you want to do it anyway, see the download instructions for Linux. You will also have to set the PATH variable used by GUI applications by following the instructions found on Stack Overflow

3. Set the toolbox's library path

We strongly recommend that you install the Toolbox (version 1.4.8 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/.


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.