The moving cat puzzle

README.md

@@ -42,6 +42,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [Stone Scale Puzzle](specifications/Stones)                                                         | Leslie Lamport                                      |    ✔     |             |         |     ✔     |          |
 | [The Coffee Can Bean Problem](specifications/CoffeeCan)                                             | Andrew Helwer                                       |    ✔     |             |         |     ✔     |          |
 | [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a)                | Stephan Merz, Leslie Lamport, Markus Kuppe          |    ✔     |             |   (✔)   |     ✔     |          |
+| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle)                                           | Florian Schanda                                     |    ✔     |             |         |     ✔     |          |
 | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie)                                      | Leslie Lamport, Stephan Merz                        |          |      ✔      |    ✔    |     ✔     |          |
 | [Misra Reachability Algorithm](specifications/MisraReachability)                                    | Leslie Lamport                                      |          |      ✔      |    ✔    |     ✔     |          |
 | [Byzantizing Paxos by Refinement](specifications/byzpaxos)                                          | Leslie Lamport                                      |          |      ✔      |    ✔    |     ✔     |          |

manifest.json

@@ -1330,6 +1330,40 @@
         }
       ]
     },
+    {
+      "path": "specifications/Moving_Cat_Puzzle",
+      "title": "The Moving Cat Puzzle",
+      "description": "Demonstrating the solution for the moving cat puzzle is correct.",
+      "sources": [],
+      "authors": ["Florian Schanda"],
+      "tags": ["beginner"],
+      "modules": [
+        {
+          "path": "specifications/Moving_Cat_Puzzle/Cat.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/Moving_Cat_Puzzle/OddBoxes.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": ["liveness"],
+              "result": "success"
+            },
+            {
+              "path": "specifications/Moving_Cat_Puzzle/EvenBoxes.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": ["liveness"],
+              "result": "success"
+            }
+          ]
+	}
+      ]
+    },
     {
       "path": "specifications/MultiCarElevator",
       "title": "Multi-Car Elevator System",

specifications/Moving_Cat_Puzzle/Cat.tla

@@ -0,0 +1,106 @@
+You have N boxes numbered 1 to N, arranged on a line. A cat is hiding
+in one of the boxes. Every night, she moves to an adjacent box, and
+every morning, you have one chance to inspect a box to find her. How
+do you find the cat?
+
+Solution: You start at box 2 and move one by one to N - 1. Then you
+observe N - 1 again and start moving back to box 2. Repeat and
+eventually you will find the cat. E.g with 5 boxes you check 2, 3, 4,
+4, 3, 2; with 4 boxes you check 2, 3, 3, 2.
+
+There is a simpler solution if the number of boxes is odd. The
+solution here works in both even and odd cases.
+
+The puzzle is trivial / impossible for a single box, since the cat
+cannot move.
+
+---- MODULE Cat ----
+
+EXTENDS Naturals
+
+CONSTANTS
+  Number_Of_Boxes
+
+ASSUME Number_Of_Boxes >= 2
+
+VARIABLES
+  \* The box the cat is currently hiding in
+  cat_box,
+
+  \* The box that is observed
+  observed_box,
+
+  \* The direction in which our search is progressing
+  direction
+
+vars == <<cat_box, observed_box, direction>>
+
+----------------------------------------------------------------------
+
+Directions == {"left", "right"}
+
+Boxes == 1 .. Number_Of_Boxes
+
+Observed_Boxes == 2 .. Number_Of_Boxes - 1
+
+----------------------------------------------------------------------
+
+\* Initially the cat is in an arbitrary box. We start our search
+\* anywhere in the pattern described by the solution.
+Init ==
+  /\ cat_box \in Boxes
+  /\ observed_box \in Observed_Boxes
+  /\ direction \in Directions
+
+\* The action performed by the cat: she either moves left or
+\* right. There is no wrap-around.
+Move_Cat ==
+  /\ \/ cat_box' = cat_box + 1
+     \/ cat_box' = cat_box - 1
+  /\ cat_box' \in Boxes
+
+\* The action performed by us: we observe boxes one by one. If we hit
+\* the end of our search we reverse direction. For N boxes, we
+\* alternate between 2 and N - 1.
+Observe_Box ==
+  LET next_box == IF direction = "right"
+                  THEN observed_box + 1
+                  ELSE observed_box - 1
+  IN \/ /\ next_box \in Observed_Boxes
+        /\ observed_box' = next_box
+        /\ UNCHANGED direction
+     \/ /\ next_box \notin Observed_Boxes
+        /\ direction' = CHOOSE d \in Directions: d /= direction
+        /\ UNCHANGED observed_box
+
+\* Each step both the cat moves, and we make a choice on where to
+\* look. Note that while in the puzzle description these things happen
+\* one after the other, in the spec here there is no need. We can do
+\* both at the same time.
+Next ==
+  /\ Move_Cat
+  /\ Observe_Box
+
+Spec ==
+  /\ Init
+  /\ [][Next]_vars
+
+  \* The cat must always make a move, it is not allowed to sit
+  \* still. Note that we could also apply weak fairness directly to
+  \* Next, but this seems more precise to me.
+  /\ WF_cat_box(Move_Cat)
+
+----------------------------------------------------------------------
+
+\* The game ends if the cat is in the observed box. With the above
+\* algorithm, this will eventually happen.
+Victory == <>(observed_box = cat_box)
+
+----------------------------------------------------------------------
+
+TypeOK ==
+  /\ cat_box \in Boxes
+  /\ observed_box \in Observed_Boxes
+  /\ direction \in Directions
+
+====

specifications/Moving_Cat_Puzzle/EvenBoxes.cfg

@@ -0,0 +1,8 @@
+CONSTANTS
+  Number_Of_Boxes = 6
+
+SPECIFICATION Spec
+
+INVARIANT TypeOK
+
+PROPERTY Victory

specifications/Moving_Cat_Puzzle/OddBoxes.cfg

@@ -0,0 +1,8 @@
+CONSTANTS
+  Number_Of_Boxes = 5
+
+SPECIFICATION Spec
+
+INVARIANT TypeOK
+
+PROPERTY Victory