-
Notifications
You must be signed in to change notification settings - Fork 0
/
TowerOfHanoi.tla
131 lines (114 loc) · 6.43 KB
/
TowerOfHanoi.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
------------------------------- MODULE TowerOfHanoi -------------------------------
EXTENDS Naturals, Bits, FiniteSets, TLC
(***************************************************************************)
(* TRUE iff i is a power of two *)
(***************************************************************************)
PowerOfTwo(i) ==
i & (i - 1) = 0
(***************************************************************************)
(* A set of all powers of two up to n *)
(***************************************************************************)
SetOfPowerOfTwo(n) ==
{ x \in 1 .. (2 ^ n - 1): PowerOfTwo(x) }
(***************************************************************************)
(* Copied from TLA+'s Bags standard library. The sum of f[x] for all x in *)
(* DOMAIN f. *)
(***************************************************************************)
Sum(f) ==
LET
DSum[S \in SUBSET DOMAIN f] == LET
elt ==
CHOOSE e \in S: TRUE
IN
IF
S = {}
THEN
0
ELSE
f[elt] + DSum[S \ {elt}]
IN
DSum[DOMAIN f]
(***************************************************************************)
(* D is number of disks and N number of towers *)
(***************************************************************************)
CONSTANT
D,
N
(***************************************************************************)
(* Towers of Hanoi with N towers *)
(***************************************************************************)
VARIABLES
towers
vars ==
<<towers>>
(***************************************************************************)
(* The total sum of all towers must amount to the disks in the system *)
(***************************************************************************)
Inv ==
Sum(towers) = 2 ^ D - 1
(* Towers are naturals in the interval (0, 2^D] *)
TypeOK ==
/\ \A i \in DOMAIN towers: /\ towers[i] \in Nat
\* Towers are represented by natural numbers
/\ towers[i] < 2 ^ D
(***************************************************************************)
(* Now we define of the initial predicate, that specifies the initial *)
(* values of the variables. *)
(***************************************************************************)
Init ==
/\ towers = [i \in 1 .. N|-> IF
i = 1
THEN
2 ^ D - 1
ELSE
0]
\* all towers are empty except all disks are on the first Tower
(***************************************************************************)
(* TRUE iff the tower is empty *)
(***************************************************************************)
IsEmptyTower(tower) ==
tower = 0
(***************************************************************************)
(* TRUE iff the disk is located on the given tower *)
(***************************************************************************)
IsOnTower(tower, disk) ==
/\ tower & disk = disk
(***************************************************************************)
(* TRUE iff disk is the smallest disk on tower *)
(***************************************************************************)
IsSmallestDisk(tower, disk) ==
/\ IsOnTower(tower, disk)
/\ tower & (disk - 1) = 0
\* All less significant bits are 0
(***************************************************************************)
(* TRUE iff disk can be moved off of tower *)
(***************************************************************************)
CanMoveOff(tower, disk) ==
/\ IsOnTower(tower, disk)
/\ IsSmallestDisk(tower, disk)
(***************************************************************************)
(* TRUE iff disk can be moved to the tower *)
(***************************************************************************)
CanMoveTo(tower, disk) ==
\/ tower & (disk - 1) = 0
\/ IsEmptyTower(tower)
(***************************************************************************)
(* *)
(***************************************************************************)
Move(from, to, disk) ==
/\ CanMoveOff(towers[from], disk)
/\ CanMoveTo(towers[to], disk)
/\ towers' = [towers EXCEPT ![from]=towers[from] - disk,
\* Remaining tower does not change
![to]=towers[to] + disk]
(***************************************************************************)
(* Define all possible actions that disks can perform. *)
(***************************************************************************)
Next ==
\E d \in SetOfPowerOfTwo(D): \E idx1, idx2 \in DOMAIN towers: /\ idx1 # idx2
\* No need to try to move onto the same tower (Move(...) prevents it too)
/\ Move(idx1, idx2, d)
=============================================================================
\* Modification History
\* Last modified Tue May 17 14:55:33 CEST 2016 by markus
\* Created Sun Jul 17 10:20:57 CEST 2011 by markus