# A TLA+/PlusCal Mini-cookbook

I’ve been playing around with TLA+ for a while now and built one or two useful specifications. While I still struggle a bit with the actual modeling process at times, I’m getting much more comfortable with the language itself and wanted to write down a few notes on some things that weren’t clear or obvious to me. Hopefully not too many lies in here.

## Contents

- Types
- Recursion in functions
- Sequences can be expressed as functions
- Updating multiple structure fields in one step
- Sets of structures

## Types

Not sure I’ve seen a simple list of the fundamental types in TLA+, so:

- Numbers
- Strings
- Booleans
- Functions (and structures)
- Model values

Why no sequence/tuple type? Refer to Sequences can be expressed as functions for details.

## Recursion in functions

If you haven’t already read Hillel Wayne’s excellent section on functions in Learn TLA+ I highly recommend it. He describes TLA+ functions like so:

The word ‘function’ can cause a lot of misunderstanding. They are not similar to functions in other languages- that’s operators. Instead, functions are closer in nature to hashes or dictionaries, except that you can choose to programmatically determine the value from the key.

I think that’s perfect. A TLA+ *function* looks something like `Double`

below:

```
EXTENDS TLC, Integers
Double[k \in Nat] == k * 2
(*--algorithm OpFn1
begin
assert Double[3] = 6;
assert DOMAIN Double = Nat;
end algorithm;
*)
```

`Double`

accepts an argument `k`

and multiplies it by 2. Note that `k`

has a
*domain*, a set of values for which the function is valid. Here `Double`

is
valid for all natural numbers (`Nat`

).

Functions can also work with multiple arguments:

```
EXTENDS TLC, Integers
Mul[k \in Nat, j \in Nat] == k * j
(*--algorithm OpFn2
begin
assert Mul[3, 2] = 6;
\* the below fails model checking, but why?
assert DOMAIN Mul = Nat \X Nat
end algorithm;
*)
```

Here `Mul`

accepts `k`

and `j`

, both of which can be any natural number. What’s
`DOMAIN Mul`

here? For a finite domain it should be the cross product of the
domain of `k`

and `j`

, but if you try to model check this it will fail because
TLA+ can’t enumerate all the values in `Nat`

. That’s probably for the best. :)

No reason why we can’t define functions with finite domains:

```
EXTENDS TLC, Integers
Mul[k \in {1, 2, 3}, j \in {1, 2, 3}] == k * j
(*--algorithm OpFn3
begin
assert Mul[3, 2] = 6;
assert DOMAIN Mul = {1, 2, 3} \X {1, 2, 3}
end algorithm;
*)
```

Model checking this works just fine.

So far we haven’t done anything with functions that we couldn’t also do with an operator. One thing you can accomplish with functions that you can’t easily achieve with operators is recursion. Let’s look at how we might construct a sequence for all values in 1..N in order using a recursive function:

```
EXTENDS TLC, Integers, Sequences
F[k \in Nat] == IF k = 1 THEN << 1 >> ELSE Append(F[k-1], k)
(*--algorithm OpFn4
begin
assert F[3] = << 1, 2, 3 >>;
assert F[5] = << 1, 2, 3, 4, 5 >>;
end algorithm;
*)
```

If you look closely at the definition of `F`

you can see we’ve essentially set
`F[k] = Append(F[k-1], n)`

with a special base case for `k = 1`

, so `F`

is
obviously recursive here.

This is actually a great segue into the next section!

## Sequences can be expressed as functions

Most folks with some exposure to TLA+ can create a simple sequence and know how
to manipulate them using the `Sequences`

module:

```
EXTENDS TLC, Sequences, Integers
(*--algorithm Seq1
variables x = << 1, 2, 3 >>;
begin
appendFour:
x := Append(x, 4);
appendFive:
x := x \o << 5 >>;
checkSeq:
assert x = << 1, 2, 3, 4, 5 >>;
end algorithm;
*)
```

If you’re writing specifications you can get a long way just knowing this much.

What’s easy to miss when you’re learning TLA+ and PlusCal is that sequences are just functions:

```
EXTENDS TLC, Sequences, Integers
(*--algorithm Seq2
begin
assert << 1, 2, 3 >> = [k \in 1..3 |-> k];
assert DOMAIN << 1, 2, 3 >> = DOMAIN [k \in 1..3 |-> k];
end algorithm;
*)
```

Try it out, this passes model checking.

So what are the implications of this? Well, we can express sequences of length
N as a function with `DOMAIN x = 1..N`

and then operate on it using
operators like `Append`

and `Len`

from the `Sequences`

module:

```
EXTENDS TLC, Sequences, Integers
CONSTANTS N
(*--algorithm Seq3
variables x = [k \in 1..N |-> k];
begin
checkPreAppend:
assert Len(x) = N;
assert x[N] = N;
doAppend:
x := Append(x, N + 1);
checkPostAppend:
assert Len(x) = N + 1;
assert x[N + 1] = N + 1;
end algorithm;
*)
```

Again, try it out. Set N to some small integer value (I model checked this
with `N = 5`

).

I *think* it’s accurate to say that all sequences are functions but not all
functions are sequences (since a function may not be defined for all 1..N).
If you know differently you can send me hate mail or angry tweets and I’ll
correct this post.

## Updating multiple structure fields in one step

PlusCal will prevent you from updating multiple fields on the same structure
in a single step. For example, this **DOES NOT** work:

```
EXTENDS Integers
(*--algorithm AtomicUpdate1
variables x = [a |-> 1, b |-> 2, c |-> 3];
begin
oneStep:
x.a := x.a + 1;
x.b := x.b + 1;
end algorithm;
*)
```

You can bypass this by overwriting `x`

entirely (sometimes error-prone)
or by using `EXCEPT`

to only update the fields you want to modify:

```
EXTENDS Integers
(*--algorithm AtomicUpdate2
variables x = [a |-> 1, b |-> 2, c |-> 3];
begin
oneStep:
x := [x EXCEPT !.a = x.a + 1, !.b = x.b + 1];
assert x = [a |-> 2, b |-> 3, c |-> 3];
end algorithm;
*)
```

And you can achieve something similar using the `@@`

operator to compose
the structure/function with the updates you want to make:

```
EXTENDS Integers
(*--algorithm AtomicUpdate3
variables x = [a |-> 1, b |-> 2, c |-> 3];
begin
oneStep:
x := [a |-> x.a + 1, b |-> x.b + 1] @@ x;
assert x = [a |-> 2, b |-> 3, c |-> 3];
end algorithm;
*)
```

## Sets of structures

This one is “obvious” in that there’s nothing special about structures that would prevent you from using them to build a set but the syntax can be a bit hard to grok at a glance:

```
{[x |-> y] : y \in 1..N}
```

I often use this pattern for process identifiers:

```
EXTENDS TLC, Sequences, Integers
CONSTANTS NumNodes
MakeProcess(type, id) == [type |-> type, id |-> id]
NodeProcesses == {MakeProcess("Node", id) : id \in 1..NumNodes}
WaitProcess == MakeProcess("Wait", 1)
(*--algorithm SetsOfStructs
variables done = [nid \in {n.id : n \in NodeProcesses} |-> FALSE];
process nodeProcess \in NodeProcesses
begin
setDone:
done[self.id] := TRUE;
end process;
process waitProcess = WaitProcess
begin
awaitAllDone:
await \A nid \in DOMAIN done : done[nid];
end process;
end algorithm;
*)
```