diff --git a/README.md b/README.md index 5a60810d..3e9983b0 100644 --- a/README.md +++ b/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 | | ✔ | ✔ | ✔ | | diff --git a/manifest.json b/manifest.json index bc9eb837..3c0ab7e6 100644 --- a/manifest.json +++ b/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", diff --git a/specifications/Moving_Cat_Puzzle/Cat.tla b/specifications/Moving_Cat_Puzzle/Cat.tla new file mode 100644 index 00000000..f41d4d96 --- /dev/null +++ b/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 == <> + +---------------------------------------------------------------------- + +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 + +==== diff --git a/specifications/Moving_Cat_Puzzle/EvenBoxes.cfg b/specifications/Moving_Cat_Puzzle/EvenBoxes.cfg new file mode 100644 index 00000000..5e55b569 --- /dev/null +++ b/specifications/Moving_Cat_Puzzle/EvenBoxes.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Number_Of_Boxes = 6 + +SPECIFICATION Spec + +INVARIANT TypeOK + +PROPERTY Victory diff --git a/specifications/Moving_Cat_Puzzle/OddBoxes.cfg b/specifications/Moving_Cat_Puzzle/OddBoxes.cfg new file mode 100644 index 00000000..11495b42 --- /dev/null +++ b/specifications/Moving_Cat_Puzzle/OddBoxes.cfg @@ -0,0 +1,8 @@ +CONSTANTS + Number_Of_Boxes = 5 + +SPECIFICATION Spec + +INVARIANT TypeOK + +PROPERTY Victory