TLA+ Proof System

Windows

The package:

for 32-bit Cygwin: tlaps-1.4.5-i686-cygwin-inst.exe

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