Constants
Let’s go back to our old Hanoi solver. As a refresher, this is the code we started with.
---- 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; *)
====
It works, but what if we wanted to change one of the parameters (more towers, more disks in a tower), we’d have to directly edit the code. It would be better to make a generic spec and test different parameters in the models instead. To do this, we introduce constants.
CONSTANTS TSIZE, TSPACES
FullTower[n \in 1..TSIZE] == n \* <<1, 2, 3, ...>>
Board[n \in 1..TSPACES] == IF n = 1 THEN FullTower ELSE <<>>
(* --algorithm hanoi
variables tower = Board;
define
D == DOMAIN tower
end define;
begin
while TRUE do
assert tower[TSPACES] /= FullTower;
\* rest is the same
This is the same as the old code, except that we now define the tower in terms of constants. Instead of the spec assigning the constant a value, the model does instead.
When we click edit we can assign a specific value to each constant.
Assumptions
What if we also wanted to vary the solution? For example, we all know that it’s possible to move the entire tower over. But is it possible to reach <<<<1, 2>>, <<>>, <<3, 4>>>>? By moving the solution to a constant, we can vary that in the model, too:
CONSTANT SOLUTION
\* ...
assert tower /= SOLUTION
And now we can put the new solution in an ordinary assignment:
One problem: this solution is nonsensical. It has four numbers when TSIZE is 3. In these cases, TLA+ can’t find a solution because the solution isn’t even defined! One way to catch this kind of error is with an ASSUME statement:
IsSensical(state) == /\ Len(state) = TSPACES \* Correct spaces
/\ \A tower \in DOMAIN state: \* Numbers do not exceed TSIZE
\A disc \in DOMAIN state[tower]:
state[tower][disc] \in 1..TSIZE
/\ \A n \in 1..TSIZE : \* All numbers appear
\E tower \in DOMAIN state:
\E disc \in DOMAIN state[tower]:
n = state[tower][disc]
\* ...
ASSUME IsSensical(SOLUTION)
TLC will check that our assignments don’t break any of the ASSUME expressions, so we can use ASSUME to make sure nobody makes a bad model. Of course, it can only check what we remember to check: for example, a solution with two “5”s can still slip through. As always, with programming, be paranoid.