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.

## 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 = 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 = << 1, 2, 3 >>;
assert F = << 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;
*)