This post shows how to write your first simple TLA+ specification.
What is a specification?
In software, the behaviour of a system is described as a sequence of states. Mathematically, each state is expressed as a function F(t), which represents the state of a system at time t. To completely specify a system, we write out each state to fully define the systems behaviour.
A simple clock
This example comes from Chapter 2 of the book Specifying Systems by the creator of TLA+, Leslie Lamport. If you are unfamiliar with the math used here, refer to basic math for writing TLA+ article.
This example is a simple clock that shows only the hour of the day. How can we specify this behaviour using TLA+? More abstractly, what are the sequence of states that specify the behaviour of the clock? If the current hour is represented as the variable h, then the behaviour of the clock is to change this variable for each hour:
[h = 1] -> [h = 2] -> [h = 3] -> ...
To define this in TLA+ requires writing an initial predicate for the starting value of h, and a next-state relation describing how the hour changes at each step.
The initial starting point of the clock is somewhat irrelevant, and we can simply set it to any value between 1 and 12. The behaviour of the clock is to, at each step, increment its value by 1, except if the hour is 12, where we will reset the clock to 1 (assuming a 12 hour clock). To completely specify the clock, we would create a single formula combining the initial predicate with the next-state relation using a conjunction:
h ∈ {1, …, 12} ∧ [h = 1] -> [h = 2] -> [h = 3] -> …
Any system that we build that satisfies this formula satisfies our specification for the simple clock. This must be true for all starting steps, and for all possible points in time (all steps).
A simple clock in TLA+
We can express this simple algorithm using TLA+. TLA+ divides partitions
into modules; the simple clock can be contained in a single module.
Modules are specified using a header, which is a sequence of four or more
- characters and the MODULE keyword. The following section begins
a TLA+ module:
---- MODULE Clock ----
Arithmetic operators like + are not defined in TLA+. This allows you to
write your own + operator that adds matrices or complex numbers, for
example. Thankfully, TLA+ provides a standard library that implements some
common arithmetic. We can add those libraries to our module using the
EXTENDS keyword.
---- MODULE Clock ----
EXTENDS Naturals
Variables in TLA+ need to be defined before use via the VARIABLE
keyword. The following section defines a variable h to represent the
hour value of the clock:
---- MODULE Clock ----
EXTENDS Naturals
VARIABLE h
Now, to define our initial condition of the clock we need a function.
Functions are defined using the == operator, which means is defined to be:
---- MODULE Clock ----
EXTENDS Naturals
VARIABLE h
HCinit == h \in (1 .. 12)
The ∈ operator is written as \in in TLA+, and the .. operator
defining a sequence of integers is part of the Naturals library. The
next-state relation is similarly written as previously defined:
---- MODULE Clock ----
EXTENDS Naturals
VARIABLE h
HCinit == h \in (1 .. 12)
HCnext == h’ = IF h /= 12 THEN h + 1 ELSE 1
The /= operator means not equal. IF, THEN, ELSE constructs take their
usual definitions in programming. h’ represents the new value of h,
i.e., the new state of the variable after the function completes.
Lastly, we express the clock itself as the conjunction of the initial
state and the next state, for all values of h:
---- MODULE Clock ----
EXTENDS Naturals
VARIABLE h
HCinit == h \in (1 .. 12)
HCnext == h’ = IF h /= 12 THEN h + 1 ELSE 1
HC == HCinit /\ [][HCnext]_h
The only tricky part here is the [][HCnext]_h syntax, which says “this
formula is true for all values of h”. To be more precise, the []
operator is the temporal logic operator, which asserts that the formula
following the operator is always logically true. The _h allows the
formula to make no changes to a state variable, allowing state transitions
from [h == 1] -> [h == 1], for example. Or, put another way [][HCnext]_h == [](HCNext \/ (hr’ = hr)).
Finally, we can add a THEOREM to our module. Theorem’s are formulas that
follow logically from the definitions in the module, any included library
modules, and the rules of TLA+ (set theory and logic).
---- MODULE Clock ----
EXTENDS Naturals
VARIABLE h
HCinit == h \in (1 .. 12)
HCnext == h' = IF h /= 12 THEN h + 1 ELSE 1
HC == HCinit /\ [][HCnext]_h
THEOREM HC => []HCinit
The complete specification of the clock is the formula definition of HC,
HCinit, HCnext, the operators .. and + from the Naturals module.
Checking our model with TLC and the TLA+ Toolbox
TLA+ comes with a set of tools for writing and verifying models. To start, download the latest TLA+ Toolbox release for your system from Github. Unzip the folder and you can run the precompiled Java application to start the toolbox. You should be presented with the following welcome screen:
From here, create a new specification from the file menu. In the following
example, I create a new root module and specification called
SimpleClock.
Clicking Finish will open up a blank module for you. You can copy in the specification above. The Toolbox is built on top of Eclipse and provides syntax parsing that marks the location of any parsing errors in your code. When you save your file, the box labelled ‘Parsed’ should remain green, showing that there are no syntax errors.
Now, we can create a model that verifies our specification does what it
says it does. Models are created through the File -> TLC Model Checker
window.
The model checker, TLC, is a program for finding errors in your specification. The model checker is run on a model of your specification, which tells the model checker what it should do. When creating a model you create a behaviour specification, which specifies the set of allowed behaviours of the system being specified. We also include explicitly what the model checker should check, and any initial values to substitute for parameters.
TLC works with formulas expressed as F == Init /\ [][Next]_var, which is
an initial state combined with a next-state relation. The next-state
relation can be built up from other formulas, but the entire specification
should be reduced to such a formula for checking via TLC. Together, the
initial state and the next-state are called the behaviour spec. TLC will
check this behaviour spec.
You can now run the model checker to verify that our specification does not contain any errors. The model checker is especially useful for checking concurrent algorithms for liveness or deadlock errors.
In this article, we have explored how to write a simple specification, and how to create and run a simple model check. In future articles we will look more closely at how to use the TLC model checker to verify more complex specifications.