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