# Solving Tower of Hanoi with Alloy

### david karapetyan ・3 min read

Last time we used Alloy model state traces to solve the river crossing puzzle. This time we use the same idea to solve Tower of Hanoi puzzle. My explanation for this one will be more terse. I'm going to assume you have a good grasp of the syntax and some of the simple relational patterns.

We start with signatures that describe components of the puzzle

```
open util/ordering[Ring]
open util/ordering[TowerPosition]
open util/ordering[State]
sig Ring { }
sig TowerPosition { }
sig Tower {
rings: set (TowerPosition -> lone Ring)
} {
let currentPositions = rings.Ring {
// No gaps
all position: currentPositions | position.prev in currentPositions
// Valid ring configuration with smaller disks being on top of larger disks
all position: currentPositions, positions': position.nexts {
positions'.rings in position.rings.nexts
}
}
}
```

To make the towers physical and conformant with the rules of the game we have to specify some invariants about disks/rings being in ascending order and there being no gaps. That's why we opened the ordering modules on these signatures.

Now we specify the state we will trace through

```
// A state consists of (l)eft, (m)iddle, (r)ight tower
sig State {
l, m, r: one Tower
} {
// Valid state must include all the rings/disks
Ring in (l + m + r).rings[TowerPosition]
// Towers must be disjoint
let lRings = l.rings[TowerPosition], mRings = m.rings[TowerPosition],
rRings = r.rings[TowerPosition] {
no lRings & (mRings + rRings) + mRings & rRings
}
}
```

Convince yourself that the above state invariants define a valid state. Physically the invariants say that a valid state uses all the disks and there are no repeated disks among the towers.

Next we have a few helper predicates for talking about the relationships between rings, towers, and states. Ultimately we're defining these because they are going to be used in some way to define the transition relation

```
// True only if `r` is a top ring in `t`
pred topRingInTower(t: Tower, r: Ring) {
let ringPosition = t.rings.r, nextPosition = ringPosition.next {
// `r` is on `t` and there are no disks above it
(one ringPosition && (no nextPosition || no t.rings[nextPosition]))
}
}
// Two towers `t1`, `t2` are compatible if
// we can put `r` on top of `t1` and get `t2`
pred ringTowerCompatibility(r: Ring, t1, t2: Tower) {
// The base case is that `t1` is the empty tower
no t1.rings => {
// Then `r` must be the only ring in `t2`
one t2.rings && one t2.rings.r
} else { // Otherwise `t1` is not empty
// `r` must be a new ring
no t1.rings.r
// `r` must be a top ring in `t2`
topRingInTower[t2, r]
// The ring ordering for `t1` must be in `t2`
t1.rings in t2.rings
// `t2` must differ from `t1` by only 1 ring
t2.rings[TowerPosition] - t1.rings[TowerPosition] = r
}
}
// `t1` and `t2` are compatible if they're equal or they are ring compatible
pred towerCompatibility(t1, t2: Tower) {
t1 = t2 ||
one r: Ring {
ringTowerCompatibility[r, t1, t2] ||
ringTowerCompatibility[r, t2, t1]
}
}
// True only if `ring` is a top ring in `s`
pred topRing(s: State, ring: Ring) {
topRingInTower[s.l, ring] ||
topRingInTower[s.m, ring] ||
topRingInTower[s.r, ring]
}
// Used to make sure the states are unique
pred equalState(s, s': State) {
s.l = s'.l && s.m = s'.m && s.r = s'.r
}
```

Now with those helper predicates we can define the transition relation

```
pred transition(s, s': State) {
s' = s.next
towerCompatibility[s.l, s'.l]
towerCompatibility[s.m, s'.m]
towerCompatibility[s.r, s'.r]
}
```

The transition relation basically says two consecutive states `s`

and `s'`

are related if their corresponding towers are compatible. It took me a long time to figure out this specification is what's required to specify a transition that only moves around 1 ring/disk. I don't have wise words for what led to this insight because I hit several dead ends and had to do a lot of debugging with the UI to stumble on this definition.

Finally some facts before we run the model and get the solution

```
// Different towers must have different ring orderings
fact { all disj t, t': Tower | t.rings != t'.rings }
// Starting state must have everything on the left tower
fact {
let firstState = first & State {
Ring in firstState.l.rings[TowerPosition]
}
}
// Last state must have everything on the right tower
fact {
let lastState = last & State {
Ring in lastState.r.rings[TowerPosition]
}
}
```

To run the model

```
run {
// Make sure consecutive states are related by a transition
all s: State, s': s.next | transition[s, s']
// Make sure the states are different
all disj s, s': State | !equalState[s, s']
} for exactly 3 Ring, exactly 3 TowerPosition,
exactly 8 Tower, exactly 8 State
```