Skip to content

Commit c993823

Browse files
florianschandaahelwer
florianschanda
authored and
ahelwer
committed
Another puzzle example
You have N boxes and a cat moves from one to another. Each day you can check a single box. Can you find the cat? Signed-off-by: Florian Schanda <[email protected]>
1 parent e22d145 commit c993823

File tree

5 files changed

+157
-0
lines changed

5 files changed

+157
-0
lines changed

‎README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ Here is a list of specs included in this repository, with links to the relevant
4242
| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | |
4343
| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | |
4444
| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | | (✔) | ✔ | |
45+
| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | |
4546
| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | |
4647
| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | |
4748
| [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | |

‎manifest.json

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1330,6 +1330,40 @@
13301330
}
13311331
]
13321332
},
1333+
{
1334+
"path": "specifications/Moving_Cat_Puzzle",
1335+
"title": "The Moving Cat Puzzle",
1336+
"description": "Demonstrating the solution for the moving cat puzzle is correct.",
1337+
"sources": [],
1338+
"authors": ["Florian Schanda"],
1339+
"tags": ["beginner"],
1340+
"modules": [
1341+
{
1342+
"path": "specifications/Moving_Cat_Puzzle/Cat.tla",
1343+
"communityDependencies": [],
1344+
"tlaLanguageVersion": 2,
1345+
"features": [],
1346+
"models": [
1347+
{
1348+
"path": "specifications/Moving_Cat_Puzzle/OddBoxes.cfg",
1349+
"runtime": "00:00:01",
1350+
"size": "small",
1351+
"mode": "exhaustive search",
1352+
"features": ["liveness"],
1353+
"result": "success"
1354+
},
1355+
{
1356+
"path": "specifications/Moving_Cat_Puzzle/EvenBoxes.cfg",
1357+
"runtime": "00:00:01",
1358+
"size": "small",
1359+
"mode": "exhaustive search",
1360+
"features": ["liveness"],
1361+
"result": "success"
1362+
}
1363+
]
1364+
}
1365+
]
1366+
},
13331367
{
13341368
"path": "specifications/MultiCarElevator",
13351369
"title": "Multi-Car Elevator System",

‎specifications/Moving_Cat_Puzzle/Cat.tla

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
You have N boxes numbered 1 to N, arranged on a line. A cat is hiding
2+
in one of the boxes. Every night, she moves to an adjacent box, and
3+
every morning, you have one chance to inspect a box to find her. How
4+
do you find the cat?
5+
6+
Solution: You start at box 2 and move one by one to N - 1. Then you
7+
observe N - 1 again and start moving back to box 2. Repeat and
8+
eventually you will find the cat. E.g with 5 boxes you check 2, 3, 4,
9+
4, 3, 2; with 4 boxes you check 2, 3, 3, 2.
10+
11+
There is a simpler solution if the number of boxes is odd. The
12+
solution here works in both even and odd cases.
13+
14+
The puzzle is trivial / impossible for a single box, since the cat
15+
cannot move.
16+
17+
---- MODULE Cat ----
18+
19+
EXTENDS Naturals
20+
21+
CONSTANTS
22+
Number_Of_Boxes
23+
24+
ASSUME Number_Of_Boxes >= 2
25+
26+
VARIABLES
27+
\* The box the cat is currently hiding in
28+
cat_box,
29+
30+
\* The box that is observed
31+
observed_box,
32+
33+
\* The direction in which our search is progressing
34+
direction
35+
36+
vars == <<cat_box, observed_box, direction>>
37+
38+
----------------------------------------------------------------------
39+
40+
Directions == {"left", "right"}
41+
42+
Boxes == 1 .. Number_Of_Boxes
43+
44+
Observed_Boxes == 2 .. Number_Of_Boxes - 1
45+
46+
----------------------------------------------------------------------
47+
48+
\* Initially the cat is in an arbitrary box. We start our search
49+
\* anywhere in the pattern described by the solution.
50+
Init ==
51+
/\ cat_box \in Boxes
52+
/\ observed_box \in Observed_Boxes
53+
/\ direction \in Directions
54+
55+
\* The action performed by the cat: she either moves left or
56+
\* right. There is no wrap-around.
57+
Move_Cat ==
58+
/\ \/ cat_box' = cat_box + 1
59+
\/ cat_box' = cat_box - 1
60+
/\ cat_box' \in Boxes
61+
62+
\* The action performed by us: we observe boxes one by one. If we hit
63+
\* the end of our search we reverse direction. For N boxes, we
64+
\* alternate between 2 and N - 1.
65+
Observe_Box ==
66+
LET next_box == IF direction = "right"
67+
THEN observed_box + 1
68+
ELSE observed_box - 1
69+
IN \/ /\ next_box \in Observed_Boxes
70+
/\ observed_box' = next_box
71+
/\ UNCHANGED direction
72+
\/ /\ next_box \notin Observed_Boxes
73+
/\ direction' = CHOOSE d \in Directions: d /= direction
74+
/\ UNCHANGED observed_box
75+
76+
\* Each step both the cat moves, and we make a choice on where to
77+
\* look. Note that while in the puzzle description these things happen
78+
\* one after the other, in the spec here there is no need. We can do
79+
\* both at the same time.
80+
Next ==
81+
/\ Move_Cat
82+
/\ Observe_Box
83+
84+
Spec ==
85+
/\ Init
86+
/\ [][Next]_vars
87+
88+
\* The cat must always make a move, it is not allowed to sit
89+
\* still. Note that we could also apply weak fairness directly to
90+
\* Next, but this seems more precise to me.
91+
/\ WF_cat_box(Move_Cat)
92+
93+
----------------------------------------------------------------------
94+
95+
\* The game ends if the cat is in the observed box. With the above
96+
\* algorithm, this will eventually happen.
97+
Victory == <>(observed_box = cat_box)
98+
99+
----------------------------------------------------------------------
100+
101+
TypeOK ==
102+
/\ cat_box \in Boxes
103+
/\ observed_box \in Observed_Boxes
104+
/\ direction \in Directions
105+
106+
====

‎specifications/Moving_Cat_Puzzle/EvenBoxes.cfg

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CONSTANTS
2+
Number_Of_Boxes = 6
3+
4+
SPECIFICATION Spec
5+
6+
INVARIANT TypeOK
7+
8+
PROPERTY Victory

‎specifications/Moving_Cat_Puzzle/OddBoxes.cfg

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CONSTANTS
2+
Number_Of_Boxes = 5
3+
4+
SPECIFICATION Spec
5+
6+
INVARIANT TypeOK
7+
8+
PROPERTY Victory

0 commit comments

Comments
 (0)