The TLA Home Page

Last modified 12 November 2016

A Correction

What is TLA?
News
The TLA+ Google Group
The TLA Tools
Resources for Learning About TLA

News

TLA+ Use at Amazon

A technical report describing TLA+ use at Amazon is available here.

TLA+ Tools Now an Open-Source Project

The TLA+ Toolbox and the TLA+ Tools have been released as an open-source project, under the MIT License. The source code is available on CodePlex. The executable files for the Toolbox are available from a new site accessible by a link on the Toolbox's web page. The stand-alone versions of the TLA+ Tools can be obtained through a new link on the TLA+ Tools web page.

You can use the TLA+ Google group to communicate with members of the TLA+ community, including the maintainers of the tools. Post a message if you have a question, want to report a bug, or just want to tell us what you're doing with TLA+. The easiest way to post a message is to send email to [email protected] where x should be replaced by tlaplus.

The TLA Tools

The TLA+ tools are: the SANY parser, the TLC model checker, the PlusCal translator, the TLATeX pretty printer, and the TLAPS proof system. These tools are all used from the TLA Toolbox, an IDE (integrated development environment). Downloading the Toolbox downloads all the tools except for TLAPS, which must be downloaded separately from the TLAPS web site. The tools can also be downloaded without the Toolbox to be used from a command line, as described here (for all tools except TLAPS). Some limitations of the tools and some enhancements to them are described only here.

Resources for Learning About TLA

The TLA+ Hyperbook This is a work in progress that is far from complete. However, the parts that are are written provide the best introduction to TLA+ and the tools, as well as being a good way to get started learning PlusCal. It also has a brief introduction to the TLAPS proof system.
The TLA+ Book This is a real, published book that you can download. It contains a complete description of TLA+ and the TLC model checker at the time of its publication. The first 90 or so pages are all that most engineers will want to read. There have been changes to the TLA+ language since then--the major changes being the addition of constructs for writing proofs. These changes are described here.
TLA+ Examples A somewhat random collection of example TLA+ specifications.
PlusCal See the PlusCal web page for documents that describe the PlusCal algorithm language.
TLAPS The TLAPS web site is currently the best place to go to find out how to use the proof system.
Summary of TLA+ A 7-page "cheat sheet" that compactly describes all of the TLA+ language and definitions from the standard modules.
Lamport's TLA Papers This web page lists almost everything Leslie Lamport has written about TLA. It includes some helpful introductory material.
Other TLA Links Links to work relevant to TLA not on the TLA+ or TLAPS web sites.

_______________________________________________________________________________________
This page can be found by searching the Web for the 21-letter string uidlamporttlahomepage. Please do not put this string in any document that could wind up on the web--including email messages and pdf and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamporttlahomepage".