How to install TLA+ Tools
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.
TLA Toolbox Released
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 [...]
Tools and Methodologies for Formal Specifications and for Proofs
There are a number of existing tools for working on TLA+ specifications, the most important of which is the TLC model-checker. Although the proof side of TLA+ is not well-developed yet, with no proof tools and an incomplete definition of the proof language, TLA+ has already proved its worth in significant projects in hardware design, [...]
Command Line Switches
This tutorial describes the command line switches accepted by the console-based TLA+ Tools: SANY, TLC, and PlusCal Translator.
The command line switches are detected, by the fact that they begin with a ‘-’ character. Once the first command line element that is not a switch is encountered, the rest are presumed to be file names.
Recent Post
Popular Post
- Getting Started (8186 views)
- Command Line Switches (6708 views)
- TLA Toolbox (5097 views)
- Tools and Methodologies for Formal Specifications and for Proofs (2529 views)
- Discussions (2463 views)
- Coming soon: TLA+ Toolbox (1959 views)
- Books (1804 views)
- PlusCal (1800 views)
- TLA+ (1756 views)
- Teaching (1679 views)