TLA+ | The way to specify

The major change is PlusCal Version 1.5, which allows specification of an algorithm’s fairness properties. There have also been a number of minor bug fixes.

After the initial release of TLA Toolbox followed by a several maintenance releases a version containing a new tool has been released. TLA Toolbox now supports TLAPS, the TLA Proof Checker. Check the Tools Section

There are various tools available for the TLA+ specification language and PlusCal algorithm language, as described in the TLA Tools section in more detail. These command-line tools are now integrated in a full-featured IDE, called the TLA Toolbox, for writing and debugging TLA+ specifications and PlusCal algorithms. It combines editors for specifications and TLC models [...]

There are various tools available for the TLA+ specification language and PlusCal algorithm language, as described in the Tools section in more detail. An additional tool is coming soon: the TLA+ Toolbox.

This tutorial describes the command line switches accepted by the console-based TLA+ Tools: SANY, TLC, and the PlusCal Translator. Most users will run the tools from the Toolbox, in which case the switches for SANY and TLC are irrelevant. When running the Toolbox, command line switches for the PlusCal translator can be provided in a [...]

This tutorial provides a description of the installation procedure of the console-based version of TLA+ Tools. Separate directions for completing the installation on Windows and on Unix are provided.