Mac OS X (10.13 and later)

The package: tlaps-1.5.0-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 Homebrew or MacPorts, 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.5.0-i386-darwin-inst.bin

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

$ sudo ./tlaps-1.5.0-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, z3, 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.6.0 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/.

4. Install CVC4 (optional)

You may want to install CVC4 to use as an additional SMT back-end for TLAPS (the default, Z3, is included in the installer). Note that some of our example files use CVC4 for a few proof obligations.

To install CVC4, you first need to install Homebrew, then follow the instructions on the CVC4 installation page.

Uninstallation

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.