|
| 1 | +(***************************************************************************) |
| 2 | +(* Tower of Hanoi *) |
| 3 | +(* *) |
| 4 | +(* From https://en.wikipedia.org/wiki/Tower_of_Hanoi: *) |
| 5 | +(* *) |
| 6 | +(* The Tower of Hanoi is a mathematical game or puzzle. It consists of *) |
| 7 | +(* three rods and a number of disks of different sizes, which can slide *) |
| 8 | +(* onto any rod. The puzzle starts with the disks in a neat stack in *) |
| 9 | +(* ascending order of size on one rod, the smallest at the top, thus *) |
| 10 | +(* making a conical shape. *) |
| 11 | +(* *) |
| 12 | +(* The objective of the puzzle is to move the entire stack to another rod, *) |
| 13 | +(* obeying the following simple rules: *) |
| 14 | +(* *) |
| 15 | +(* 1. Only one disk can be moved at a time. *) |
| 16 | +(* 2. Each move consists of taking the upper disk from one of the stacks *) |
| 17 | +(* and placing it on top of another stack or on an empty rod. *) |
| 18 | +(* 2. No larger disk may be placed on top of a smaller disk. *) |
| 19 | +(***************************************************************************) |
| 20 | + |
| 21 | +------------------------------ MODULE HanoiSeq ------------------------------ |
| 22 | +EXTENDS TLC, Sequences, Integers |
| 23 | + |
| 24 | +CONSTANTS A, B, C |
| 25 | +VARIABLES towers |
| 26 | + |
| 27 | +(***************************************************************************) |
| 28 | +(* We model the three positions where a "tower" of disks can be present as *) |
| 29 | +(* sequences of natural numbers. The numbers represent the sizes of the *) |
| 30 | +(* disks. *) |
| 31 | +(* *) |
| 32 | +(* A, B, and C are the initial configurations of the towers. For example: *) |
| 33 | +(* A == <<1,2,3>> *) |
| 34 | +(* B == <<>> *) |
| 35 | +(* C == <<>> *) |
| 36 | +(***************************************************************************) |
| 37 | +ASSUME A \in [1..Len(A) -> Nat] |
| 38 | +ASSUME B \in [1..Len(B) -> Nat] |
| 39 | +ASSUME C \in [1..Len(C) -> Nat] |
| 40 | + |
| 41 | +Init == |
| 42 | + towers = <<A, B, C>> |
| 43 | + |
| 44 | +(***************************************************************************) |
| 45 | +(* A disk can be moved if: *) |
| 46 | +(* - The source position is different from the destination. *) |
| 47 | +(* - The source tower is not empty. *) |
| 48 | +(* - The top disk of the source tower is smaller than the top disk of *) |
| 49 | +(* the destination tower. *) |
| 50 | +(***************************************************************************) |
| 51 | +CanMove(from, to) == |
| 52 | + /\ from /= to |
| 53 | + /\ towers[from] /= <<>> |
| 54 | + /\ IF |
| 55 | + towers[to] = <<>> |
| 56 | + THEN |
| 57 | + TRUE |
| 58 | + ELSE |
| 59 | + Head(towers[from]) < Head(towers[to]) |
| 60 | + |
| 61 | +(***************************************************************************) |
| 62 | +(* Moving a disk means the source tower is left with all but the top disk, *) |
| 63 | +(* which is added to the destination tower. *) |
| 64 | +(***************************************************************************) |
| 65 | +Move(from, to) == |
| 66 | + towers' = [ |
| 67 | + towers EXCEPT |
| 68 | + ![from] = Tail(towers[from]), |
| 69 | + ![to] = <<Head(towers[from])>> \o towers[to] |
| 70 | + ] |
| 71 | + |
| 72 | +Next == |
| 73 | + \E from, to \in 1..Len(towers): |
| 74 | + /\ CanMove(from, to) |
| 75 | + /\ Move(from, to) |
| 76 | + |
| 77 | +(***************************************************************************) |
| 78 | +(* This finishes the spec. The next section are the invariants to check. *) |
| 79 | +(***************************************************************************) |
| 80 | + |
| 81 | +(***************************************************************************) |
| 82 | +(* Helper to get the elements of a sequence. *) |
| 83 | +(***************************************************************************) |
| 84 | +Range(sequence) == |
| 85 | + {sequence[i]: i \in DOMAIN sequence} |
| 86 | + |
| 87 | +(***************************************************************************) |
| 88 | +(* `towers` has 3 elements, each a sequence of numbers. *) |
| 89 | +(***************************************************************************) |
| 90 | +TypeOK == |
| 91 | + /\ DOMAIN towers = 1..3 |
| 92 | + /\ \A sequence \in Range(towers): |
| 93 | + sequence \in [1..Len(sequence) -> Nat] |
| 94 | + |
| 95 | +(***************************************************************************) |
| 96 | +(* In all towers there should never be elements which were not initially *) |
| 97 | +(* present. *) |
| 98 | +(***************************************************************************) |
| 99 | +NoNewElements == |
| 100 | + LET |
| 101 | + originalElements == |
| 102 | + UNION {Range(A), Range(B), Range(C)} |
| 103 | + towerElements == |
| 104 | + UNION {Range(towers[1]), Range(towers[2]), Range(towers[3])} |
| 105 | + IN |
| 106 | + towerElements = originalElements |
| 107 | + |
| 108 | +(***************************************************************************) |
| 109 | +(* The total number of disks should stay constant. *) |
| 110 | +(***************************************************************************) |
| 111 | +TotalConstant == |
| 112 | + LET |
| 113 | + originalTotal == |
| 114 | + Len(A) + Len(B) + Len(C) |
| 115 | + towerTotal== |
| 116 | + Len(towers[1]) + Len(towers[2]) + Len(towers[3]) |
| 117 | + IN |
| 118 | + towerTotal = originalTotal |
| 119 | + |
| 120 | +(***************************************************************************) |
| 121 | +(* The final configuration has all disks on the right tower with the disks *) |
| 122 | +(* ordered by size. If a violation of this invariant can be found, the *) |
| 123 | +(* stack trace shows the steps to solve the Hanoi problem. *) |
| 124 | +(***************************************************************************) |
| 125 | +NotSolved == |
| 126 | + ~( |
| 127 | + /\ towers[1] = <<>> |
| 128 | + /\ towers[2] = <<>> |
| 129 | + /\ towers[3] = [i \in 1..Len(towers[3]) |-> i] |
| 130 | + ) |
| 131 | +============================================================================= |
0 commit comments