The TLA Home Page

Last modified 21 March 2017

 

A Correction

Contents

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

 

What is TLA?

Click here to find out.

 

News

 

TLA+ Video Course

The TLA+ Video Course will be a series of video lectures to teach how to write TLA+ specifications. The first two lectures have now been released. Here is the course's home page. The videos made Hacker News the day they were released.

The TLA+ Google Group

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 x@googlegroups.com 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

______________________________________________________________________________________________________

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".