Skip to content

Commit c5024e0

Browse files
florianschandaflorianschanda
committed
Add a variant of the Prisoner's puzzle
This version has a single switch. There are two variants, one where the initial position of the light switch is known, and another one where it is not. Signed-off-by: Florian Schanda <fschanda@nvidia.com>
1 parent ad3d3e4 commit c5024e0

6 files changed

Lines changed: 313 additions & 0 deletions

File tree

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ Here is a list of specs included in this repository, with links to the relevant
3535
| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | |
3636
| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | |
3737
| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | |
38+
| [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | |
3839
| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | |
3940
| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | |
4041
| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | |

‎manifest.json‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1855,6 +1855,50 @@
18551855
}
18561856
]
18571857
},
1858+
{
1859+
"path": "specifications/Prisoners_Single_Switch",
1860+
"title": "The Prisoners & Switch Puzzle",
1861+
"description": "Given a room containing a single light switch prisoners enter one by one, they must develop a strategy to free themselves.",
1862+
"sources": [],
1863+
"authors": [
1864+
"Florian Schanda"
1865+
],
1866+
"tags": [
1867+
"beginner"
1868+
],
1869+
"modules": [
1870+
{
1871+
"path": "specifications/Prisoners_Single_Switch/Prisoner.tla",
1872+
"communityDependencies": [],
1873+
"tlaLanguageVersion": 2,
1874+
"features": [],
1875+
"models": [
1876+
{
1877+
"path": "specifications/Prisoners_Single_Switch/Prisoner.cfg",
1878+
"runtime": "00:00:01",
1879+
"size": "small",
1880+
"mode": "exhaustive search",
1881+
"features": [
1882+
"ignore deadlock",
1883+
"liveness"
1884+
],
1885+
"result": "success"
1886+
},
1887+
{
1888+
"path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg",
1889+
"runtime": "00:00:01",
1890+
"size": "small",
1891+
"mode": "exhaustive search",
1892+
"features": [
1893+
"ignore deadlock",
1894+
"liveness"
1895+
],
1896+
"result": "success"
1897+
}
1898+
]
1899+
}
1900+
]
1901+
},
18581902
{
18591903
"path": "specifications/ReadersWriters",
18601904
"title": "The Readers-Writers Problem",

‎specifications/Prisoners_Single_Switch/Prisoner.cfg‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CONSTANTS
2+
Prisoner = {"Alice", "Bob", "Eve"}
3+
Designated_Counter = "Alice"
4+
Light_Unknown = FALSE
5+
6+
SPECIFICATION Spec
7+
PROPERTY Terminating
8+
9+
INVARIANT TypeOK
10+
INVARIANT VictoryOK
11+
12+
CHECK_DEADLOCK FALSE

‎specifications/Prisoners_Single_Switch/Prisoner.tla‎

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
The prisoner puzzle. A set of N prisoners, all in solitary cells, is
2+
offered a game. One of them is randomly selected and placed in a
3+
special cell. This cell has a lamp and prisoners can turn it off or
4+
on. Afterwards the prisoner is returned back to their cell.
5+
6+
At any point a prisoner can announce to the warden that they have all
7+
been in the cell at least once. If they are right everyone is
8+
released. If they are wrong the game ends and they remain in prison
9+
forever.
10+
11+
The prisoners are allowed to communicate and design a strategy before
12+
the game starts. Afterwards they can no longer communicate.
13+
14+
There is a variant of the puzzle where the initial state of the light
15+
in the cell is not known.
16+
17+
In either case the strategy is:
18+
19+
* One prisoner is designated as the counter.
20+
21+
* Other prisoners, when they enter the cell turn the light on if its
22+
off. They do this at most once (or twice in the variant).
23+
24+
* If the designated counter sees the light, they turn it off and
25+
increment their count. Once they count to N (or 2N - 1 for the
26+
variant), they know that everyone (including themselves) must have
27+
entered the cell and can announce victory.
28+
29+
Note: This puzzle is a variant of other prisoner puzzle here that I
30+
was not aware of when I wrote this model.
31+
https://github.com/tlaplus/Examples/tree/master/specifications/Prisoners
32+
33+
The setup is different: here there is only one switch, and the initial
34+
status of it might be known, and the prisoners are not required to do
35+
anything if they enter the room.
36+
37+
The solution is the same however (except we don't have the busy-work
38+
switch), and our models are very similar.
39+
40+
---- MODULE Prisoner ----
41+
42+
EXTENDS FiniteSets, Naturals
43+
44+
CONSTANTS
45+
Prisoner,
46+
\* The set of prisoners playing the game. Has to be at least one.
47+
48+
Designated_Counter,
49+
\* The designated counter could also be picked non-deterministically
50+
\* during Init, but it doesn't really add any value.
51+
52+
Light_Unknown
53+
\* Configuration if the initial state of the light is "off" or
54+
\* unknown. The puzzle is harder (takes more steps) if we don't know
55+
\* the initial state.
56+
57+
ASSUME Light_Unknown \in BOOLEAN
58+
ASSUME Designated_Counter \in Prisoner
59+
60+
VARIABLES
61+
count, \* The counter's current count
62+
announced, \* If the announcement has been made
63+
64+
signalled, \* How often other prisoners have signalled
65+
66+
light, \* Current status of the light
67+
68+
has_visited \* The warden's view on who has actually been to the cell
69+
70+
vars == <<count, announced, signalled, light, has_visited>>
71+
72+
------------------------------------------------------------------------------
73+
74+
\* The strategy differs slightly if the initial state of the light is
75+
\* known or not. If it's "off" then a simple count to N is
76+
\* sufficient. If the state is unknown we count to 2N - 1, and each
77+
\* prisoner will signal up to two times.
78+
79+
SignalLimit == IF Light_Unknown THEN 2 ELSE 1
80+
81+
VictoryThreshold ==
82+
IF Light_Unknown
83+
THEN Cardinality(Prisoner) * 2 - 1
84+
ELSE Cardinality(Prisoner)
85+
86+
------------------------------------------------------------------------------
87+
88+
NormalPrisoner == Prisoner \ {Designated_Counter}
89+
90+
\* The only thing to note here is that the count starts at one. Since
91+
\* only the counter will make an announcement if they are in the cell,
92+
\* this 1 means they have already counted themselves. We could also
93+
\* model this with a separate variable to note when the counter has
94+
\* visited the cell for the very first time, but this is not
95+
\* necessary.
96+
97+
Init ==
98+
/\ count = 1
99+
/\ announced = FALSE
100+
/\ signalled = [ p \in NormalPrisoner |-> 0 ]
101+
/\ \/ Light_Unknown /\ light \in { "off", "on" }
102+
\/ ~Light_Unknown /\ light = "off"
103+
/\ has_visited = {}
104+
105+
\* The action taken by the designated counter, if they are placed in
106+
\* the cell
107+
\*
108+
\* Note: we could simplify this change the IF to just be a
109+
\* precondition to the action, and while that would be a more elegant
110+
\* spec, I think this better models the decision procedure of the
111+
\* prisoner.
112+
CounterAction(p) ==
113+
/\ p = Designated_Counter
114+
/\ IF light = "on"
115+
THEN
116+
/\ light' = "off"
117+
/\ count' = count + 1
118+
ELSE
119+
UNCHANGED <<light, count>>
120+
/\ announced' = (count' >= VictoryThreshold)
121+
/\ UNCHANGED <<signalled>>
122+
123+
\* The action taken by the other prisoners, if they are placed in the
124+
\* cell
125+
\*
126+
\* Same note on the IF applies here.
127+
StandardAction(p) ==
128+
/\ p \in NormalPrisoner
129+
/\ IF light = "off" /\ signalled[p] < SignalLimit
130+
THEN
131+
/\ light' = "on"
132+
/\ signalled' = [signalled EXCEPT ![p] = @ + 1]
133+
ELSE
134+
UNCHANGED <<light, signalled>>
135+
/\ UNCHANGED <<count, announced>>
136+
137+
\* The action performed by the warden: place a prisoner in the cell
138+
\* and maintain our own view of who's been selected (so we can judge
139+
\* if a victory announcement is correct)
140+
WardenAction(p) ==
141+
\* Put one of the prisoners in the cell
142+
/\ \/ CounterAction(p)
143+
\/ StandardAction(p)
144+
145+
\* Maintain the warden's view
146+
/\ has_visited' = has_visited \union {p}
147+
148+
Next == \E p \in Prisoner: WardenAction(p)
149+
150+
Spec ==
151+
/\ Init
152+
/\ [][Next]_vars
153+
154+
\* Base assumption in the game: the warden eventually has to choose
155+
\* everyone in a way progress is possible
156+
/\ \A p \in Prisoner: WF_vars(WardenAction(p))
157+
158+
------------------------------------------------------------------------------
159+
160+
\* Goal of the game: eventually the prisoners will win
161+
Terminating == <>announced
162+
163+
------------------------------------------------------------------------------
164+
165+
\* Type invariant. Note it's possible to over-count in the lights
166+
\* unknown version, if the initial state of the light is "on". Hence
167+
\* the slightly more relaxed upper bound on count.
168+
TypeOK ==
169+
/\ count \in 1 .. VictoryThreshold + 1
170+
/\ announced \in BOOLEAN
171+
/\ signalled \in [ NormalPrisoner -> 0 .. 2 ]
172+
/\ light \in {"off", "on"}
173+
/\ has_visited \subseteq Prisoner
174+
175+
\* Invariant to make sure victory is never declared in error
176+
VictoryOK == announced => (has_visited = Prisoner)
177+
178+
====

‎specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CONSTANTS
2+
Prisoner = {"Alice", "Bob", "Eve"}
3+
Designated_Counter = "Alice"
4+
Light_Unknown = TRUE
5+
6+
SPECIFICATION Spec
7+
PROPERTY Terminating
8+
9+
INVARIANT TypeOK
10+
INVARIANT VictoryOK
11+
12+
CHECK_DEADLOCK FALSE

‎specifications/Prisoners_Single_Switch/README.md‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# The Prisoners & Switch Puzzle
2+
3+
A set of N prisoners, all in solitary cells, is offered a game. One of
4+
them is randomly selected and placed in a special cell. This cell has
5+
a lamp and prisoners can turn it off or on. Afterwards the prisoner is
6+
returned back to their cell.
7+
8+
At any point a prisoner can announce to the warden that they have all
9+
been in the cell at least once. If they are right everyone is
10+
released. If they are wrong the game ends and they remain in prison
11+
forever.
12+
13+
The prisoners are allowed to communicate and design a strategy before
14+
the game starts. Afterwards they can no longer communicate.
15+
16+
The default version where the initial state of the light is off is
17+
checked in [Prisoner.cfg](Prisoner.cfg).
18+
19+
There is a variant of the puzzle where the initial state of the light
20+
in the cell is not known. This is checked in
21+
[PrisonerLightUnknown.cfg](PrisonerLightUnknown.cfg).
22+
23+
## Note on the spec
24+
25+
The spec could be more compact by replacing the do nothing ELSE clause
26+
in the actions with stutter steps, like so:
27+
28+
```TLA+
29+
StandardAction(p) ==
30+
/\ p \in NormalPrisoner
31+
/\ light = "off"
32+
/\ signalled[p] < SignalLimit
33+
/\ light' = "on"
34+
/\ signalled' = [signalled EXCEPT ![p] = @ + 1]
35+
/\ UNCHANGED <<count, announced>>
36+
37+
CounterAction(p) ==
38+
/\ p = Designated_Counter
39+
/\ light = "on"
40+
/\ light' = "off"
41+
/\ count' = count + 1
42+
/\ announced' = (count' >= VictoryThreshold)
43+
/\ UNCHANGED <<signalled>>
44+
```
45+
46+
In the end I decided against this as I wanted to model the individual
47+
decision procedure of a prisoner as closely as possible.
48+
49+
I also did not want to remove the `p` from the `CounterAction` for a
50+
similar reason - it's the counter's job to know what they are doing,
51+
not the warden's.
52+
53+
## Note on the other prisoner puzzle
54+
55+
The light unknown variant is very similar to the other [prisoner
56+
puzzle](../Prisoners) in this repository. I was not aware of this when
57+
I created my version. This puzzle has a slightly different setup, but
58+
at their core they are identical.
59+
60+
This puzzle has one light switch and prisoners are not forced to use
61+
it.
62+
63+
The other puzzle has two switches, and prisoners are forced to use
64+
exactly one. The puzzles are identical since you treat one switch as
65+
the signal switch, and the other one is used if you want to "do
66+
nothing".

0 commit comments

Comments
 (0)