TLA+ Version 2

TLA+ Version 2

Leslie Lamport

Last modified on 21 September 2018


You'll miss a lot on this web site unless you enable Javascript in your browser.

What is TLA+ Version 2?       [show]

TLA+ Version 2, here called TLA+2 for short, is the current version of TLA+.  TLA+ now means TLA+2.  The previous version is referred to here 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

Features for Writing Specifications       [show]

Recursive Operator Definitions

A RECURSIVE statement allows you to define operators recursively, including the use of mutual recursion.  For example, here's a silly way to define both fact1(n) and fact2(n) to equal n factorial, for any natural number n:
   RECURSIVE fact1(_), fact2(_)

   fact1(n) == IF n = 0 THEN  1 
                        ELSE n*fact2(n-1)

   fact2(n) == IF n = 0 THEN 1 
                        ELSE n*fact1(n-1)

LAMBDA Expressions   

TLA+ allows you to define a higher-order operator that takes an operator as an argument.  In TLA+1, you could use only the name of an operator that has already been defined or declared as such an argument.  TLA+2 allows the use of a LAMBDA expression as the argument.  For example, if F is an operator that takes as its argument an operator with two arguments, then you can write the expression
   LET Id(a, b) == a + 2*b
   IN  F(Id)
 
In TLA+2, you can write this as
   F(LAMBDA a, b : a + 2*b)
You can also use a LAMBDA expression to substitute for an operator in the WITH clause of an INSTANCE statement.

Writing Proofs       [show]

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.  The TLAPS project page contains a brief tutorial on writing TLA+ proofs.

Other Changes       [show]

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.  In TLA+1, if you wrote
   Foo(x) == INSTANCE M 
and module M defines the infix operator ++, then you had to write a weird expression like
   a  Foo(42)!++  b
to use the instantiated operator.  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 read Section 5.2 in the TLA+2 Preliminary Guide for an explanation.

Documentation       [show]

All current documentation written since 2008 describes TLA+2. That include the TLA+ Video Course and the TLA+ Hyperbook.  Here is some more detailed documentation:
TLA Version 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.

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.  There is also a pretty-printed PDF version.