The TLA Home Page

The TLA Home Page

Last modified 15 June 2013

 

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

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.  We promise to respond much more promptly than we did to postings on the old Forum site.

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".
Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft