Generic Instructions

These instructions apply to any UNIX-like system, including GNU/Linux, most BSD variants, Solaris, WSL on Windows, MacOSX, etc.

Notes for Windows users: TLAPS requires WSL (Windows Subsystem for Linux).

1. Obtain source code

TLAPS source code can be obtained as a release tarball or cloned from the git repository.

  1. Download the tarball: 202210041448.tar.gz

    You can unpack TLAPS by running the following command:

    $ tar -xzf 202210041448.tar.gz

  2. Clone the repository

    $ git clone https://github.com/tlaplus/tlapm/

2. Compile the TLA+ Proof Manager (TLAPM)

See instructions at INSTALL.md.

3. Verify the installation

Run the following command:

$ tlapm --config

It should report the versions of zenon and isabelle you installed in earlier steps.

You can also test the TLAPS on any of the examples in the examples directory (which you can easily refer to using the option -I +examples to tlapm). For instance:

$ tlapm -C -I +examples/cantor Cantor1.tla

You will see a lot of output from Isabelle, the most important being the message at the end stating that all obligations were proved. For more information on how to use TLAPS, read the tutorial.