Proofs

The current version of the TLA+ language contains several features not described in Specifying Systems.  Chief among them are constructs for writing hierarchically structured proofs.  The differences between the current and previous versions of TLA, including the proof language, are described here

The Toolbox aids reading and writing hierarchically structured TLA+ proofs by providing commands to view just the part of the structure that you want to see.  These commands are described in the subtopic Viewing and Editing Structured Proofs.

TLAPS, the TLA+ Proof System, can be used to mechanically check TLA+ proofs.  You can select the parts of a proof to be checked, and you can have the Toolbox display which steps' proofs have and have not been checked.  The Running TLAPS subtopic describes how to run it from the Toolbox.  But before you can run TLAPS, you must install it on your computer.  Instructions for doing this, as well as an explanation of how to use TLAPS, is on the TLAPS web page.  As described on that page, if you are using Windows, you will also have to install Cygwin on your computer.

Because new releases of the Toolbox and of TLAPS are not completely synchronized, the version of the standard TLAPS module used by the Toolbox (through the SANY parser) may differ from the one used by TLAPS.  That module will eventually stabilize to a final version, but until it does, you may want to copy the TLAPS.tla file needed by TLAPS into your spec's directory.  Alternatively, you can replace the version used by the Toolbox with the lastest version from TLAPS.  The Toolbox's version is in a subdirectory (subfolder) of the directory containing the Toolbox program; that subdirectory has a name something like:

   \plugins\org.lamport.tlatools_1.0.0.201201191425\tla2sany\StandardModules
The current version used by TLAPS should be available at
    http://msr-inria.inria.fr/~doligez/tlaps/dist/TLAPS.tla
 


Subtopics
Viewing and Editing Structured Proofs
Running TLAPS
↑ TLA+ Toolbox User's Guide