The package:

1. Install Cygwin

Cygwin version 3.0.7 or later is required. You need to install the 32-bit version of Cygwin, even if your OS is 64-bit. This version of TLAPS does not work on 64-bit Cygwin.

2. Install the Cygwin packages   make, perl, wget

Consult the Cygwin manual for instructions on how to install Cygwin packages. Installing these packages will bring in a number of other packages, which are also needed.

3. Install the Proof System

Download the TLAPS installer and run the following command in a Cygwin terminal, from the directory in which the package has been downloaded (usually /cygdrive/c/Users/$USER/Downloads):

$ ./tlaps-1.4.5-*-cygwin-inst.exe

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.

4. 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 C:\cygwin\usr\local\lib\tlaps\.

5. 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:

$ mv cvc4-1.7-win64-opt.exe /usr/local/lib/tlaps/bin/cvc4.exe


To uninstall TLAPS, open a cygwin terminal and type:

$ `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 directory where TLAPS is installed.