Linux

Builds of the latest development version are attached to the 1.6.0 rolling pre-release: tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz

This archive is relocatable and needs no installer: unpack it wherever you like, then put its bin directory on your PATH.

Verify with tlapm --version; tlapm --config lists the bundled backend provers. If you use the Toolbox or the VS Code extension, the TLAPS.tla standard module is under tlapm/lib/tlapm/stdlib — add that directory to the TLA⁺ library path.

Alternatively, follow DEVELOPING.md to build TLAPS from source.

Release 1.5.0 (October 2022)

Past versioned releases are listed on the GitHub releases page. The most recent of those, 1.5.0, ships as an installer: tlaps-1.5.0-x86_64-linux-gnu-inst.bin

It predates several years of development, so prefer the build above unless you specifically need this version. The remaining instructions on this page apply to it.

1. Install the Proof System

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

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

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

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

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

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

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

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.

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 should download it from the CVC4 download page, then rename it and move it to /usr/local/lib/tlaps/bin with this command:

Uninstallation

To uninstall TLAPS, run:

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.