Skip to content

Commit d666ad2

Browse files
florianschandaflorianschanda
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 <fschanda@nvidia.com>
1 parent e22d145 commit d666ad2

5 files changed

Lines changed: 150 additions & 0 deletions

File tree

‎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: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
You have N boxes numbered 1 to N, in one of which a cat is
2+
hiding. Every night, she moves to an adjacent box, and every morning,
3+
you have one chance to inspect a box to find her. How do you find the
4+
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+
\* Initially the cat is in an arbitrary box. We start our search at
41+
\* box 2, moving to the right. It doesn't actually matter where you
42+
\* start as long as you eventually fall into the pattern described by
43+
\* the solution.
44+
Init ==
45+
/\ cat_box \in 1 .. Number_Of_Boxes
46+
/\ observed_box = 2
47+
/\ direction = "right"
48+
49+
\* The action performed by the cat: we either move left or
50+
\* right. There is no wrap-around.
51+
Move_Cat ==
52+
\/ cat_box < Number_Of_Boxes /\ cat_box' = cat_box + 1
53+
\/ cat_box > 1 /\ cat_box' = cat_box - 1
54+
55+
\* The action performed by us: we observe boxes one by one. If we hit
56+
\* the end of our search we reverse direction. For N boxes, we
57+
\* alternate between 2 and N - 1.
58+
Observe_Box ==
59+
/\ IF direction = "right"
60+
THEN \/ /\ observed_box < Number_Of_Boxes - 1
61+
/\ observed_box' = observed_box + 1
62+
/\ UNCHANGED direction
63+
\/ /\ observed_box = Number_Of_Boxes - 1
64+
/\ direction' = "left"
65+
/\ UNCHANGED observed_box
66+
ELSE \/ /\ observed_box > 2
67+
/\ observed_box' = observed_box - 1
68+
/\ UNCHANGED direction
69+
\/ /\ observed_box = 2
70+
/\ direction' = "right"
71+
/\ UNCHANGED observed_box
72+
73+
\* Each step both the cat moves, and we make a choice on where to
74+
\* look.
75+
Next ==
76+
/\ Move_Cat
77+
/\ Observe_Box
78+
79+
Spec ==
80+
/\ Init
81+
/\ [][Next]_vars
82+
83+
\* The cat must always make a move, it is not allowed to sit still.
84+
/\ WF_cat_box(Move_Cat)
85+
86+
----------------------------------------------------------------------
87+
88+
\* The game ends if the cat is in the observed box. With the above
89+
\* algorithm, this will eventually happen.
90+
Victory == <>(observed_box = cat_box)
91+
92+
----------------------------------------------------------------------
93+
94+
TypeOK ==
95+
/\ cat_box \in 1 .. Number_Of_Boxes
96+
/\ observed_box \in 2 .. Number_Of_Boxes - 1
97+
/\ direction \in {"left", "right"}
98+
99+
====

‎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)