diff --git a/README.md b/README.md index 059cf44a..5a60810d 100644 --- a/README.md +++ b/README.md @@ -35,6 +35,7 @@ Here is a list of specs included in this repository, with links to the relevant | [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | | | [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | | | [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | +| [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | | | [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | | | [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | | | [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | | diff --git a/manifest.json b/manifest.json index 67263c38..bc9eb837 100644 --- a/manifest.json +++ b/manifest.json @@ -1855,6 +1855,68 @@ } ] }, + { + "path": "specifications/Prisoners_Single_Switch", + "title": "The Prisoners & Switch Puzzle", + "description": "Given a room containing a single light switch prisoners enter one by one, they must develop a strategy to free themselves.", + "sources": [], + "authors": [ + "Florian Schanda" + ], + "tags": [ + "beginner" + ], + "modules": [ + { + "path": "specifications/Prisoners_Single_Switch/Prisoner.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/Prisoners_Single_Switch/Prisoner.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/Prisoners_Single_Switch/SoloPrisoner.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + }, + { + "path": "specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg", + "runtime": "00:00:01", + "size": "small", + "mode": "exhaustive search", + "features": [ + "liveness" + ], + "result": "success" + } + ] + } + ] + }, { "path": "specifications/ReadersWriters", "title": "The Readers-Writers Problem", diff --git a/specifications/Prisoners_Single_Switch/Prisoner.cfg b/specifications/Prisoners_Single_Switch/Prisoner.cfg new file mode 100644 index 00000000..9f349d0d --- /dev/null +++ b/specifications/Prisoners_Single_Switch/Prisoner.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Prisoner = {"Alice", "Bob", "Eve"} + Light_Unknown = FALSE + +SPECIFICATION Spec +PROPERTY Terminating + +INVARIANT TypeOK +INVARIANT VictoryOK diff --git a/specifications/Prisoners_Single_Switch/Prisoner.tla b/specifications/Prisoners_Single_Switch/Prisoner.tla new file mode 100644 index 00000000..09ac8c2c --- /dev/null +++ b/specifications/Prisoners_Single_Switch/Prisoner.tla @@ -0,0 +1,184 @@ +The prisoner puzzle. A set of N prisoners, all in solitary cells, is +offered a game. One of them is randomly selected and placed in a +special cell. This cell has a lamp and prisoners can turn it off or +on. Afterwards the prisoner is returned back to their cell. + +At any point a prisoner can announce to the warden that they have all +been in the cell at least once. If they are right everyone is +released. If they are wrong the game ends and they remain in prison +forever. + +The prisoners are allowed to communicate and design a strategy before +the game starts. Afterwards they can no longer communicate. + +There is a variant of the puzzle where the initial state of the light +in the cell is not known. + +In either case the strategy is: + + * One prisoner is designated as the counter. + + * Other prisoners, when they enter the cell turn the light on if its + off. They do this at most once (or twice in the variant). + + * If the designated counter sees the light, they turn it off and + increment their count. Once they count to N (or 2N - 1 for the + variant), they know that everyone (including themselves) must have + entered the cell and can announce victory. + +Note: This puzzle is a variant of other prisoner puzzle here that I +was not aware of when I wrote this model. +https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners + +The setup is different: here there is only one switch, and the initial +status of it might be known, and the prisoners are not required to do +anything if they enter the room. + +The solution is the same however (except we don't have the busy-work +switch), and our models are very similar. + +---- MODULE Prisoner ---- + +EXTENDS FiniteSets, Naturals + +CONSTANTS + \* The set of prisoners playing the game. Has to be at least one. + Prisoner, + + \* Configuration if the initial state of the light is "off" or + \* unknown. The puzzle is harder (takes more steps) if we don't know + \* the initial state. + Light_Unknown + +ASSUME Light_Unknown \in BOOLEAN + +VARIABLES + \* The counter's current count + count, + + \* If the announcement has been made + announced, + + \* How often other prisoners have signalled + signalled, + + \* Current status of the light + light, + + \* The warden's view on who has actually been to the cell + has_visited + +vars == <> + +------------------------------------------------------------------------------ + +\* The strategy differs slightly if the initial state of the light is +\* known or not. If it's "off" then a simple count to N is +\* sufficient. If the state is unknown we count to 2N - 1, and each +\* prisoner will signal up to two times. + +SignalLimit == IF Light_Unknown THEN 2 ELSE 1 + +VictoryThreshold == + IF Light_Unknown + THEN Cardinality(Prisoner) * 2 - 1 + ELSE Cardinality(Prisoner) + +------------------------------------------------------------------------------ + +\* We pick somebody at random to be the counter +DesignatedCounter == CHOOSE p \in Prisoner: TRUE + +\* The other prisoners +NormalPrisoner == Prisoner \ {DesignatedCounter} + +\* The only thing to note here is that the count starts at one. Since +\* only the counter will make an announcement if they are in the cell, +\* this 1 means they have already counted themselves. We could also +\* model this with a separate variable to note when the counter has +\* visited the cell for the very first time, but this is not +\* necessary. +Init == + /\ count = 1 + /\ announced = FALSE + /\ signalled = [ p \in NormalPrisoner |-> 0 ] + /\ \/ Light_Unknown /\ light \in { "off", "on" } + \/ ~Light_Unknown /\ light = "off" + /\ has_visited = {} + +------------------------------------------------------------------------------ + +\* The action taken by the designated counter, if they are placed in +\* the cell +\* +\* Note: we could simplify this change the IF to just be a +\* precondition to the action, and while that would be a more elegant +\* spec, I think this better models the decision procedure of the +\* prisoner. +CounterAction(p) == + /\ p = DesignatedCounter + /\ IF light = "on" + THEN + /\ light' = "off" + /\ count' = count + 1 + ELSE + UNCHANGED <> + /\ announced' = (count' >= VictoryThreshold) + /\ UNCHANGED <> + +\* The action taken by the other prisoners, if they are placed in the +\* cell +\* +\* Same note on the IF applies here. +StandardAction(p) == + /\ p \in NormalPrisoner + /\ IF light = "off" /\ signalled[p] < SignalLimit + THEN + /\ light' = "on" + /\ signalled' = [signalled EXCEPT ![p] = @ + 1] + ELSE + UNCHANGED <> + /\ UNCHANGED <> + +\* The action performed by the warden: place a prisoner in the cell +\* and maintain our own view of who's been selected (so we can judge +\* if a victory announcement is correct) +WardenAction(p) == + \* Put one of the prisoners in the cell + /\ \/ CounterAction(p) + \/ StandardAction(p) + + \* Maintain the warden's view + /\ has_visited' = has_visited \union {p} + +Next == \E p \in Prisoner: WardenAction(p) + +Spec == + /\ Init + /\ [][Next]_vars + + \* Base assumption in the game: the warden eventually has to choose + \* everyone in a way progress is possible + /\ \A p \in Prisoner: WF_vars(WardenAction(p)) + +------------------------------------------------------------------------------ + +\* Goal of the game: eventually the prisoners will win +Terminating == <>announced + +------------------------------------------------------------------------------ + +\* Type invariant. Note it's possible to over-count in the lights +\* unknown version, if the initial state of the light is "on". Hence +\* the slightly more relaxed upper bound on count. +TypeOK == + /\ count \in 1 .. VictoryThreshold + 1 + /\ announced \in BOOLEAN + /\ signalled \in [ NormalPrisoner -> 0 .. 2 ] + /\ light \in {"off", "on"} + /\ has_visited \subseteq Prisoner + +\* Invariant to make sure victory is never declared in error +VictoryOK == announced => (has_visited = Prisoner) + +==== diff --git a/specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg b/specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg new file mode 100644 index 00000000..86e4b9bf --- /dev/null +++ b/specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Prisoner = {"Alice", "Bob", "Eve"} + Light_Unknown = TRUE + +SPECIFICATION Spec +PROPERTY Terminating + +INVARIANT TypeOK +INVARIANT VictoryOK diff --git a/specifications/Prisoners_Single_Switch/README.md b/specifications/Prisoners_Single_Switch/README.md new file mode 100644 index 00000000..96dfd6cd --- /dev/null +++ b/specifications/Prisoners_Single_Switch/README.md @@ -0,0 +1,71 @@ +# The Prisoners & Switch Puzzle + +A set of N prisoners, all in solitary cells, is offered a game. One of +them is randomly selected and placed in a special cell. This cell has +a lamp and prisoners can turn it off or on. Afterwards the prisoner is +returned back to their cell. + +At any point a prisoner can announce to the warden that they have all +been in the cell at least once. If they are right everyone is +released. If they are wrong the game ends and they remain in prison +forever. + +The prisoners are allowed to communicate and design a strategy before +the game starts. Afterwards they can no longer communicate. + +The default version where the initial state of the light is off is +checked in [Prisoner.cfg](Prisoner.cfg). + +There is a variant of the puzzle where the initial state of the light +in the cell is not known. This is checked in +[PrisonerLightUnknown.cfg](PrisonerLightUnknown.cfg). + +## Note on the spec + +The spec could be more compact by replacing the do nothing ELSE clause +in the actions with stutter steps, like so: + +```TLA+ +StandardAction(p) == + /\ p \in NormalPrisoner + /\ light = "off" + /\ signalled[p] < SignalLimit + /\ light' = "on" + /\ signalled' = [signalled EXCEPT ![p] = @ + 1] + /\ UNCHANGED <> + +CounterAction(p) == + /\ p = Designated_Counter + /\ light = "on" + /\ light' = "off" + /\ count' = count + 1 + /\ announced' = (count' >= VictoryThreshold) + /\ UNCHANGED <> +``` + +In the end I decided against this as I wanted to model the individual +decision procedure of a prisoner as closely as possible. + +I also did not want to remove the `p` from the `CounterAction` for a +similar reason - it's the counter's job to know what they are doing, +not the warden's. + +## Note on the other prisoner puzzle + +The light unknown variant is very similar to the other [prisoner +puzzle](../Prisoners) in this repository. I was not aware of this when +I created my version. This puzzle has a slightly different setup, but +at their core they are identical. + +This puzzle has one light switch and prisoners are not forced to use +it. + +The other puzzle has two switches, and prisoners are forced to use +exactly one. The puzzles are identical since you treat one switch as +the signal switch, and the other one is used if you want to "do +nothing". + +One final difference is that this spec also works for a single +prisoner, which is of course trivial but still an interesting +corner-case. These are checked in [SoloPrisoner.cfg](SoloPrisoner.cfg) +and [SoloPrisonerLightUnknown.cfg](SoloPrisonerLightUnknown.cfg). diff --git a/specifications/Prisoners_Single_Switch/SoloPrisoner.cfg b/specifications/Prisoners_Single_Switch/SoloPrisoner.cfg new file mode 100644 index 00000000..28ad3318 --- /dev/null +++ b/specifications/Prisoners_Single_Switch/SoloPrisoner.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Prisoner = {"Alice"} + Light_Unknown = FALSE + +SPECIFICATION Spec +PROPERTY Terminating + +INVARIANT TypeOK +INVARIANT VictoryOK diff --git a/specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg b/specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg new file mode 100644 index 00000000..369c2ed4 --- /dev/null +++ b/specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg @@ -0,0 +1,9 @@ +CONSTANTS + Prisoner = {"Alice"} + Light_Unknown = TRUE + +SPECIFICATION Spec +PROPERTY Terminating + +INVARIANT TypeOK +INVARIANT VictoryOK