TLA+2

What is TLA+2?

TLA+2 is a new version of TLA+. TLA+ will eventually mean TLA+2, and the current version will be referred to as TLA+1. This page contains a brief description of TLA+2 and its tools. Available documentation on the language is listed below.

Almost all TLA+ specifications are legal TLA+2 specifications. You are encouraged to start using the TLA+2 tools now and to try the new features at your leisure.

Features for Writing Specifications

The following new features may induce ordinary users to try TLA+2.

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 the current version, you can 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.

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 project is under way at the Microsoft Research / Inria Joint Centre to build a checker for these proofs. However, you may want to try writing them yourself, even though you check the proofs by hand. 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.

One feature introduced for writing proofs is the naming 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.

The TLA+2 Tools

The current TLA+ tools download includes versions of TLC, SANY, and TLATeX for use with TLA+2 specifications. (The PlusCal translator works for both TLA+ and TLA+2. You can use TLA+2 features in a PlusCal algorithm's expressions if you use the TLA+2 version of the TLC model checker.)

The TLA+2 versions of the tools work like the ordinary versions. They are executed with the following commands:

  java tlc2.TLC
  java tla2sany.SANY
  java tla2tex.TLA

The current versions of these tools, available on the 10 April 2008 release, are

   TLC2:    Version 2.01 of 23 February  2008
   SANY2:   Version  .91 of 10 April     2008
   TLA2TeX: Version  .9  of 19 September 2007

Documentation

Documentation on the TLA+2 language is quite preliminary. Here is what there is at the moment.

TLA+2: A Preliminary Guide