Skip to content

Commit a56ec47

Browse files
lemmylemmy
committed
Merge pull request #1 from lemmy/master
Add MIT license for Examples repository and "Tower of Hanoi" example specification
2 parents fd65a94 + 7839ae2 commit a56ec47

File tree

5 files changed

+177
-0
lines changed

5 files changed

+177
-0
lines changed

‎LICENSE.md

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
All these TLA+ examples are licensed under the MIT License.
2+
3+
> Copyright (c) 2016: The TLA+ project and other contributors:
4+
> https://github.com/tlaplus/Examples/graphs/contributors
5+
>
6+
>
7+
> Permission is hereby granted, free of charge, to any person obtaining
8+
> a copy of this software and associated documentation files (the
9+
> "Software"), to deal in the Software without restriction, including
10+
> without limitation the rights to use, copy, modify, merge, publish,
11+
> distribute, sublicense, and/or sell copies of the Software, and to
12+
> permit persons to whom the Software is furnished to do so, subject to
13+
> the following conditions:
14+
>
15+
> The above copyright notice and this permission notice shall be
16+
> included in all copies or substantial portions of the Software.
17+
>
18+
> THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
19+
> EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
20+
> MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
21+
> NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
22+
> LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
23+
> OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
24+
> WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

‎specifications/tower_of_hanoi/Bits.java

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
import tlc2.value.IntValue;
2+
3+
public class Bits {
4+
public static IntValue And(IntValue x, IntValue y) {
5+
return IntValue.gen(x.val & y.val);
6+
}
7+
}
8+

‎specifications/tower_of_hanoi/Bits.tla

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
-------------------------------- MODULE Bits --------------------------------
2+
3+
\* Implemented by Bits.java. Manually create a
4+
\* .java file with the content from below copy&pasted
5+
\* and compile it (javac) against tla2tools.jar. Place
6+
\* resulting .class file on the CLASSPATH when running
7+
\* TLC.
8+
\*
9+
\* javac -cp /path/to/tla2tools.jar Bits.java
10+
LOCAL And(x,y) == FALSE
11+
12+
(***************************************************************************)
13+
(* Bitwise AND of x and y *)
14+
(***************************************************************************)
15+
x & y == And(x, y) \* Infix variant of And(x,y)
16+
17+
=============================================================================
18+
\* Modification History
19+
\* Last modified Tue May 17 15:07:08 CEST 2016 by markus
20+
\* Created Mon May 16 15:09:18 CEST 2016 by markus

‎specifications/tower_of_hanoi/Hanoi.tla

+122
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
------------------------------- MODULE Hanoi -------------------------------
2+
EXTENDS Naturals, Bits, FiniteSets, TLC
3+
4+
(***************************************************************************)
5+
(* TRUE iff i is a power of two *)
6+
(***************************************************************************)
7+
PowerOfTwo(i) == i & (i-1) = 0
8+
9+
(***************************************************************************)
10+
(* A set of all powers of two up to n *)
11+
(***************************************************************************)
12+
SetOfPowerOfTwo(n) == {x \in 1..(2^n-1): PowerOfTwo(x)}
13+
14+
(***************************************************************************)
15+
(* Copied from TLA+'s Bags standard library. The sum of f[x] for all x in *)
16+
(* DOMAIN f. *)
17+
(***************************************************************************)
18+
Sum(f) == LET DSum[S \in SUBSET DOMAIN f] ==
19+
LET elt == CHOOSE e \in S : TRUE
20+
IN IF S = {} THEN 0
21+
ELSE f[elt] + DSum[S \ {elt}]
22+
IN DSum[DOMAIN f]
23+
24+
(***************************************************************************)
25+
(* D is number of disks and N number of towers *)
26+
(***************************************************************************)
27+
CONSTANT D, N
28+
29+
(***************************************************************************)
30+
(* Towers of Hanoi with N towers *)
31+
(***************************************************************************)
32+
VARIABLES towers
33+
vars == <<towers>>
34+
35+
(***************************************************************************)
36+
(* The total sum of all towers must amount to the disks in the system *)
37+
(***************************************************************************)
38+
Inv == Sum(towers) = 2^D - 1
39+
40+
(* Towers are naturals in the interval (0, 2^D] *)
41+
TypeOK == /\ \A i \in DOMAIN towers : /\ towers[i] \in Nat \* Towers are represented by natural numbers
42+
/\ towers[i] < 2^D
43+
44+
(***************************************************************************)
45+
(* Now we define of the initial predicate, that specifies the initial *)
46+
(* values of the variables. *)
47+
(***************************************************************************)
48+
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
49+
50+
(***************************************************************************)
51+
(* TRUE iff the tower is empty *)
52+
(***************************************************************************)
53+
IsEmptyTower(tower) == tower = 0
54+
55+
(***************************************************************************)
56+
(* TRUE iff the disk is located on the given tower *)
57+
(***************************************************************************)
58+
IsOnTower(tower, disk) == /\ tower & disk = disk
59+
60+
(***************************************************************************)
61+
(* TRUE iff disk is the smallest disk on tower *)
62+
(***************************************************************************)
63+
IsSmallestDisk(tower, disk) == /\ IsOnTower(tower, disk)
64+
/\ tower & (disk - 1) = 0 \* All less significant bits are 0
65+
66+
(***************************************************************************)
67+
(* TRUE iff disk can be moved off of tower *)
68+
(***************************************************************************)
69+
CanMoveOff(tower, disk) == /\ IsOnTower(tower, disk)
70+
/\ IsSmallestDisk(tower, disk)
71+
72+
(***************************************************************************)
73+
(* TRUE iff disk can be moved to the tower *)
74+
(***************************************************************************)
75+
CanMoveTo(tower, disk) == \/ tower & (disk - 1) = 0
76+
\/ IsEmptyTower(tower)
77+
78+
(***************************************************************************)
79+
(* *)
80+
(***************************************************************************)
81+
Move(from, to, disk) == /\ CanMoveOff(towers[from], disk)
82+
/\ CanMoveTo(towers[to], disk)
83+
/\ towers' = [towers EXCEPT ![from] = towers[from] - disk, \* Remaining tower does not change
84+
![to] = towers[to] + disk]
85+
86+
(***************************************************************************)
87+
(* Define all possible actions that disks can perform. *)
88+
(***************************************************************************)
89+
Next == \E d \in SetOfPowerOfTwo(D): \E idx1, idx2 \in DOMAIN towers:
90+
/\ idx1 # idx2 \* No need to try to move onto the same tower (Move(...) prevents it too)
91+
/\ Move(idx1, idx2, d)
92+
93+
(***************************************************************************)
94+
(* We define the formula Spec to be the complete specification, asserting *)
95+
(* of a behavior that it begins in a state satisfying Init, and that every *)
96+
(* step either satisfies Next or else leaves the pair <<big, small>> *)
97+
(* unchanged. *)
98+
(***************************************************************************)
99+
Spec == Init /\ [][Next]_vars
100+
-----------------------------------------------------------------------------
101+
102+
(***************************************************************************)
103+
(* The final configuration has all disks on the right tower. If TLC is set *)
104+
(* to run with an invariant rightTower # 2^N-1, it will search for *)
105+
(* configurations in which this invariant is violated. If violation can be *)
106+
(* found, the stack trace shows the steps to solve the Hanoi problem. *)
107+
(***************************************************************************)
108+
NotSolved == towers[N] # 2^D - 1
109+
110+
(***************************************************************************)
111+
(* We find a solution by having TLC check if NotSolved is an invariant, *)
112+
(* which will cause it to print out an "error trace" consisting of a *)
113+
(* behavior ending in a state where NotSolved is false. With three disks, *)
114+
(* and three towers the puzzle can be solved in seven moves. *)
115+
(* The minimum number of moves required to solve a Tower of Hanoi puzzle *)
116+
(* generally is 2n - 1, where n is the number of disks. Thus, the counter- *)
117+
(* examples shown by TLC will be of length 2n-1 *)
118+
(***************************************************************************)
119+
=============================================================================
120+
\* Modification History
121+
\* Last modified Tue May 17 14:55:33 CEST 2016 by markus
122+
\* Created Sun Jul 17 10:20:57 CEST 2011 by markus

‎specifications/tower_of_hanoi/README.md

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Tower of Hanoi
2+
A specification of the ["Tower of Hanoi" problem](https://en.wikipedia.org/wiki/Tower_of_Hanoi)
3+
with the number of disk and towers defined by the model.

0 commit comments

Comments
 (0)