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.