Introduction
The look and feel of the web page is often responsible for its popularity. In the same time, the Web 2.0 hype defined some new technologies and standards, which must be offered in order to gain user’s acceptance. The pre-2.0 communication channels like emails, discussion forums and CMSs has to be extended with RSS feeds, [...]
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.
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, [...]
Welcome to the TLA+ webpage.
The main purpose of this page is to help the community around the TLA+ and PlusCal projects communicate and grow. Thus, we start with a small blog and will integrate other technologies as soon as they are required.
Have a lot of fun!
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 [...]
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, [...]
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.
