TLA+2

TLA+2


What is TLA+2?

TLA+2 is the current version of TLA+.  TLA+ now means TLA+2.  When necessary, the previous version will be referred to as TLA+1.  This page contains a brief description of how TLA+2 differs from TLA+1, which is the language described in the book Specifying Systems.  Available documentation on the language is listed below.

Almost all TLA+1 specifications are legal TLA+2 specifications.  It is highly unlikely that a TLA+1 spec you wrote will not still be a legal TLA+ spec.

Features for Writing Specifications

The following new features may induce ordinary users to try TLA+2. Other than introducing a few new keywords that can no longer be used as identifiers, there are two changes in TLA+2 that may make a TLA+ specification no longer legal.  The first is the handling of instantiated infix operators.  Currently, if you write
   Foo(x) == INSTANCE M 
and module M defines the infix operator ++, then you could have to write a weird expression like
   a  Foo(42)!++  b
In TLA+2, this is written  Foo(42)!++(a,b).

The second change is that certain operators can no longer be used to instantiate operator parameters in a constant module.  You're unlikely to encounter it.  However, if you get an error message of the form

   Error in instantiating module '...':
    A non-Leibniz operator substituted for '...'.
then you should check the TLA+2 documentation for an explanation.

Writing Proofs

The major new feature of TLA+2 is the introduction of constructs for writing proofs.  A checker for these proofs is being built as part of a project at the Microsoft Research / Inria Joint Centre.  It does not yet handle temporal-logic reasoning, but it can check most other parts of a proof.

The language supports hierarchically structured proofs.  The paper How to Write a Proof describes the basic hierarchical proof style and explains why it is much better than the way mathematicians and computer scientists now write proofs.  The TLA+2 documentation describes the language features for writing structured proofs.  See the project page for a brief tutorial on writing TLA+ proofs.

One feature introduced for writing proofs is the naming of subexpressions of a definition, which can be assisted by adding labels.  You can use subexpression names in specification, but you shouldn't.  However, they can be useful for writing tests when model checking a specification.  Moreover, labels could be useful in referring to parts of a specification in documentation.

Documentation

There is not yet a general introduction to TLA+ that is based on the current version of the language.  Such an introduction will eventually be provided by the TLA+ Hyperbook.  Here is the documentation that is currently available.
TLA+2: A Preliminary Guide
This is a fairly complete 30-page description of the features added to the language.  However, it is not easy reading, being written more as a guide for tool implementers than as a user manual.
PDF

A TLA+ Specification of the Grammar
This is a version of the TLAPlusGrammar module from Section 15.1 (page 276) of Specifying Systems (the TLA+ book), without comments, that has been updated for TLA+2.
The TLA file
PDF version produced by TLATeX

Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft