The package:

1. Install Cygwin

Cygwin version 1.7.24 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   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 32-bit package 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.3-*-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, cvc3, ls4, and translate binaries.

4. Set the Toolbox's library path

We strongly recommend that you install the Toolbox (version 1.4.7 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\.


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.