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 DefinitionsA 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 ExpressionsTLA+ 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 expressionLET 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 Mand module M defines the infix operator ++, then you had to write a weird expression like a Foo(42)!++ bto 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:
|
|||