TLA+ specifications are organized into modules. Modules can extend (import) other modules to use their functionality. Although the TLA+ standard is specified in typeset mathematical symbols, existing TLA+ tools use
LaTeX-like symbol definitions in
ASCII. TLA+ uses several terms which require definition: •
State – an assignment of values to variables •
Behaviour – a sequence of states •
Step – a pair of successive states in a behavior •
Stuttering step – a step during which variables are unchanged •
Next-state relation – a relation describing how variables can change in any step •
State function – an expression containing variables and constants that is not a next-state relation •
State predicate – a Boolean-valued state function •
Invariant – a state predicate true in all reachable states •
Temporal formula – an expression containing statements in temporal logic
Safety TLA+ concerns itself with defining the set of all correct system behaviours. For example, a one-bit clock ticking endlessly between 0 and 1 could be specified as follows: VARIABLE clock Init == clock \in {0, 1} Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0 Spec == Init /\ [][Tick]_> The next-state relation
Tick sets
clock′ (the value of
clock in the next state) to 1 if
clock is 0, and 0 if
clock is 1. The state predicate
Init is true if the value of
clock is either 0 or 1.
Spec is a temporal formula asserting all behaviours of one-bit clock must initially satisfy
Init and have all steps either match
Tick or be stuttering steps. Two such behaviours are: 0 -> 1 -> 0 -> 1 -> 0 -> ... 1 -> 0 -> 1 -> 0 -> 1 -> ... The safety properties of the one-bit clock – the set of reachable system states – are adequately described by the spec.
Liveness The above spec disallows strange states for the one-bit clock, but does not say the clock will ever tick. For example, the following perpetually-stuttering behaviours are accepted: 0 -> 0 -> 0 -> 0 -> 0 -> ... 1 -> 1 -> 1 -> 1 -> 1 -> ... A clock which does not tick is not useful, so these behaviours should be disallowed. One solution is to disable stuttering, but TLA+ requires stuttering always be enabled; a stuttering step represents a change to some part of the system not described in the spec, and is useful for
refinement. To ensure the clock must eventually tick, weak
fairness is asserted for
Tick: Spec == Init /\ [][Tick]_> /\ WF_>(Tick) Weak fairness over an action means if that action is continuously enabled, it must eventually be taken. With weak fairness on
Tick only a finite number of stuttering steps are permitted between ticks. This temporal logical statement about
Tick is called a liveness assertion. In general, a liveness assertion should be
machine-closed: it shouldn't constrain the set of reachable states, only the set of possible behaviours. Most specifications do not require assertion of liveness properties. Safety properties suffice both for model checking and guidance in system implementation.
Operators TLA+ is based on
ZF, so operations on variables involve set manipulation. The language includes set
membership,
union,
intersection,
difference,
powerset, and
subset operators.
First-order logic operators such as , , , , , are also included, as well as
universal and
existential quantifiers and .
Hilbert's is provided as the CHOOSE operator, which uniquely selects an arbitrary set element. Arithmetic operators over
reals,
integers, and
natural numbers are available from the standard modules. Temporal logic operators are built into TLA+. Temporal formulas use \Box P to mean
P is always true, and \Diamond P to mean
P is eventually true. The operators are combined into \Box \Diamond P to mean
P is true infinitely often, or \Diamond \Box P to mean eventually
P will always be true. Other temporal operators include weak and strong fairness. Weak fairness WFe(
A) means if action
A is enabled
continuously (i.e. without interruptions), it must eventually be taken. Strong fairness SFe(
A) means if action
A is enabled
continually (repeatedly, with or without interruptions), it must eventually be taken. Temporal existential and universal quantification are included in TLA+, although without support from the tools. User-defined operators are similar to
macros. Operators differ from functions in that their domain need not be a set: for example, the
set membership operator has the
category of sets as its domain, which is
not a valid set in ZFC (since its existence leads to
Russell's paradox). Recursive and anonymous user-defined operators were added in TLA+2.
Data structures The foundational data structure of TLA+ is the set. Sets are either explicitly enumerated or constructed from other sets using operators or with {x \in S : p} where
p is some condition on
x, or {e : x \in S} where
e is some function of
x. The unique
empty set is represented as {}.
Functions in TLA+ assign a value to each element in their domain, a set. [S -> T] is the set of all functions with f[
x] in
T, for each
x in the
domain set
S. For example, the TLA+ function Double[x \in Nat] == x*2 is an element of the set [Nat -> Nat] so Double \in [Nat -> Nat] is a true statement in TLA+. Functions are also defined with [x \in S |-> e] for some expression
e, or by modifying an existing function [f EXCEPT ![v1] = v2].
Records are a type of function in TLA+. The record [name |-> "John", age |-> 35] is a record with fields name and age, accessed with r.name and r.age, and belonging to the set of records [name : String, age : Nat].
Tuples are included in TLA+. They are explicitly defined with 1,e2,e3>> or constructed with operators from the standard Sequences module. Sets of tuples are defined by
Cartesian product; for example, the set of all pairs of natural numbers is defined Nat \X Nat. ==Standard modules==