Tuples and Structures

Tuples

Tuples are pretty much what you think they are. They have an ordering and everything. You specify them with <<>> and they are 1-indexed.

x == <<4, 5, 6>>;
x[1] + x[2] + x[3] = 15;

In addition, you have the DOMAIN operator. DOMAIN Tuple is the set 1..Len(Tuple). For example, DOMAIN <<"hello", "world", "!">> = {1, 2, 3}.

If you add EXTENDS Sequences to your spec, they also do double duty as sequences, which adds some more functionality. None of these operations will mutate the sequence. If you want to pop the head, for example, you have to do seq := Tail(seq).

Note that these use parenthesis, unlike DOMAIN, SUBSET, and UNION. A very rough rule of thumb is that if it’s from a module, it uses parenthesis, and if it’s part of the core language, it will be in ALL CAPS.

Reverse(Twople) == IF Len(Twople) = 2 THEN <<Twople[2], Twople[1]>> ELSE Twople

Sets of Tuples

Sometimes, you need a set of tuples or sequences. For example, given a chessboard, you might represent the squares as a pair of two integers. The construct, then, for every possible point in the grid would be (1..8) \X (1..8). \X here is the Cartesian product operator: set1 \X set2 is the set of all tuples t where t[1] \in set1 and t[2] \in set2.

chessboard_squares == {"a", "b", "c", "d", "e", "f", "g", "h"} \X (1..8)
<<"a", 2>> \in chessboard_squares
<<"b", 10>> \notin chessboard_squares

You can combine more than two sets with \X, but how they combine depends on how you group the sets. Given a \in A, b \in B, and c \in C:

<<a, b, c>> \in A \X B \X C
<<<<a, b>>, c>> \in (A \X B) \X C
<<a, <<b, c>>>> \in A \X (B \X C)

The first is a tuple of length three, the latter two are tuples of length two, one element of which is a tuple of length two.

Structures

Structures are hashes. They have keys and values. You specify them as [key |-> value] and query them with either ["key"] or .key. Both are legal and valid.

x == [a |-> 1, b |-> {2, 3}];
x.a = 1;
x["b"] = {2, 3};

Aside from that, there’s one extra trick structures have. Instead of key |-> value, you can do key : set. In that case, instead of a structure you get the set of all structures which have, for each given key, a value in the set.

x == [a : {1}, b : {2, 3}];
x = { [a |-> 1, b |-> 2], [a |-> 1, b |-> 3] }

You can also use DOMAIN on structures, which will give the set of keys, as strings.

Type Composition

Any type can be squeezed inside any other type.

x == [a |-> {<<>>, <<1, 2, 3>>, <<3, 2, 1>>}, b |-> <<[a |-> 0]>>];
x.b[1].a; \* 0

There’s nothing technically stopping you from writing a sequence with alternating 1’s and sets of structures, but that will end very badly, so please don’t do that.

Example

Solve the Tower of Hanoi.

This kind of problem flips TLA+ on its head. Instead of checking if our solution has no problems, we’re checking that our problem has a solution! A common way to do this is to turn the spec inside out: we say the spec is “valid” if the solution is unreachable. Then TLC will flag it as an “error” and show us the steps required to reproduce the solution.

---- MODULE hanoi ----
EXTENDS TLC, Sequences, Integers
                
(* --algorithm hanoi
variables tower = <<<<1, 2, 3>>, <<>>, <<>>>>, 

define 
  D == DOMAIN tower
end define;

begin
while TRUE do
  assert tower[3] /= <<1, 2, 3>>;
  with from \in {x \in D : tower[x] /= <<>>},
       to \in {
                y \in D : 
                  \/ tower[y] = <<>>
                  \/ Head(tower[from]) < Head(tower[y])
              } 
  do
    tower[from] := Tail(tower[from]) ||
    tower[to] := <<Head(tower[from])>> \o tower[to];
  end with;
end while;
end algorithm; *)
====

Everything should look familiar with the exception of the set syntax we use to define “from” and “to”. We’re covering that in more detail next section, but for now, it’s roughly a set filter. For example, from is defined as being one of the numbers such that that tower has at least one element in it.

For to, we pull it from a more restricted set: We either want the tower to be empty, or have a bigger top stone than the tower we’re moving from. Finally, in the block itself, we simulate a move with Tail and concatting. The concat is a bit of a hack, actually- while it seems like Append would be the appropriate operator here, it would put it at the wrong end of the sequence. For example, Append(<<2, 1>>, 3) = <<2, 1, 3>>, when we actually want <<3, 2, 1>>.

Running this model throws an ‘error’ and shows the steps required to reproduce the bug, aka find the solution. In general, TLA+ isn’t that well suited for solving constraint problems like these, but it can be used to do so in a pinch. Another common example is using TLA+ to solve the water bucket puzzle.