Tutorials
This page provides a list of tutorials on various aspects of TLA+, PlusCal, and the tools.
Leave a Reply
5981 views, 3 so far
today
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 models [...]
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 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 [...]
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. Please download the latest copy of the TLA+ Tools in the Tools Section. Also make sure that the Java Runtime Environment (at least version 1.4) is [...]
Recent Post
Popular Post
- TLA Toolbox (490437 views)
- Getting Started (453972 views)
- The TLA Tools (149051 views)
- Discussions (117985 views)
- Books (85978 views)
- Command Line Switches (57974 views)
- Examples (39568 views)
- Teaching (32238 views)
- TLA+ (24366 views)
- Publications (17014 views)