TLA+ Specification Language
TLA (the Temporal Logic of Actions) is a logic for specifying and reasoning about concurrent and reactive systems. Unlike other temporal logics, it is designed for writing specifications that consist mainly of ordinary (non-temporal) mathematics with just a tiny bit of temporal logic. It is the basis for TLA+, a complete specification language.
The Language
TLA+ is a powerful language for writing specifications. It is a language for ordinary math (first order logic, sets, and functions) plus the operators of the TLA logic. It also includes constructs for writing hierachical proofs. Specifications can also be written in the PlusCal algorithm language and translated to TLA+. Whichever way they are written, TLA+ specifications can be checked with the tools.
Using the tools for TLA+, the syntax of specifications can be checked. In addition, a model checker exists which helps finding bugs.
The Tools
The TLA+ tools TLA+, consist of a parser, a pretty printer, the TLC model checker, and the PlusCal to TLA+ translator. TLC can check a subclass of TLA+ specifications that seems to include all the specifications that engineers write of real systems. It uses parallel execution to achieve almost linear speedup with multiple processors.
Recently, the new TLA Toolbox has been released. It is a complete integrated development environment for TLA.
How to start
You may want to start with the TLA+ book Specifying Systems. We also recommend downloading the TLA Toolbox and trying out some examples. If you have any questions, check out the discussion forum to see if they have already been answered, and to ask them if they have not.
Another option is the TLA+ Hyperbook, a hypertext book that is now being written by Leslie Lamport. Only the very beginning has been written, but that beginning provides a very gentle introduction to TLA+ that also shows you how to start using the tools with the Toolbox.
