Skip to content

Commit f5c7f9e

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 f5c7f9e

8 files changed

Lines changed: 357 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: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1855,6 +1855,68 @@
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+
"liveness"
1883+
],
1884+
"result": "success"
1885+
},
1886+
{
1887+
"path": "specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg",
1888+
"runtime": "00:00:01",
1889+
"size": "small",
1890+
"mode": "exhaustive search",
1891+
"features": [
1892+
"liveness"
1893+
],
1894+
"result": "success"
1895+
},
1896+
{
1897+
"path": "specifications/Prisoners_Single_Switch/SoloPrisoner.cfg",
1898+
"runtime": "00:00:01",
1899+
"size": "small",
1900+
"mode": "exhaustive search",
1901+
"features": [
1902+
"liveness"
1903+
],
1904+
"result": "success"
1905+
},
1906+
{
1907+
"path": "specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg",
1908+
"runtime": "00:00:01",
1909+
"size": "small",
1910+
"mode": "exhaustive search",
1911+
"features": [
1912+
"liveness"
1913+
],
1914+
"result": "success"
1915+
}
1916+
]
1917+
}
1918+
]
1919+
},
18581920
{
18591921
"path": "specifications/ReadersWriters",
18601922
"title": "The Readers-Writers Problem",

‎specifications/Prisoners_Single_Switch/Prisoner.cfg‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
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

‎specifications/Prisoners_Single_Switch/Prisoner.tla‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
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+
\* The set of prisoners playing the game. Has to be at least one.
46+
Prisoner,
47+
48+
\* The designated counter could also be picked non-deterministically
49+
\* during Init, but it doesn't really add any value.
50+
Designated_Counter,
51+
52+
\* Configuration if the initial state of the light is "off" or
53+
\* unknown. The puzzle is harder (takes more steps) if we don't know
54+
\* the initial state.
55+
Light_Unknown
56+
57+
ASSUME Light_Unknown \in BOOLEAN
58+
ASSUME Designated_Counter \in Prisoner
59+
60+
VARIABLES
61+
\* The counter's current count
62+
count,
63+
64+
\* If the announcement has been made
65+
announced,
66+
67+
\* How often other prisoners have signalled
68+
signalled,
69+
70+
\* Current status of the light
71+
light,
72+
73+
\* The warden's view on who has actually been to the cell
74+
has_visited
75+
76+
vars == <<count, announced, signalled, light, has_visited>>
77+
78+
------------------------------------------------------------------------------
79+
80+
\* The strategy differs slightly if the initial state of the light is
81+
\* known or not. If it's "off" then a simple count to N is
82+
\* sufficient. If the state is unknown we count to 2N - 1, and each
83+
\* prisoner will signal up to two times.
84+
85+
SignalLimit == IF Light_Unknown THEN 2 ELSE 1
86+
87+
VictoryThreshold ==
88+
IF Light_Unknown
89+
THEN Cardinality(Prisoner) * 2 - 1
90+
ELSE Cardinality(Prisoner)
91+
92+
------------------------------------------------------------------------------
93+
94+
NormalPrisoner == Prisoner \ {Designated_Counter}
95+
96+
\* The only thing to note here is that the count starts at one. Since
97+
\* only the counter will make an announcement if they are in the cell,
98+
\* this 1 means they have already counted themselves. We could also
99+
\* model this with a separate variable to note when the counter has
100+
\* visited the cell for the very first time, but this is not
101+
\* necessary.
102+
Init ==
103+
/\ count = 1
104+
/\ announced = FALSE
105+
/\ signalled = [ p \in NormalPrisoner |-> 0 ]
106+
/\ \/ Light_Unknown /\ light \in { "off", "on" }
107+
\/ ~Light_Unknown /\ light = "off"
108+
/\ has_visited = {}
109+
110+
\* The action taken by the designated counter, if they are placed in
111+
\* the cell
112+
\*
113+
\* Note: we could simplify this change the IF to just be a
114+
\* precondition to the action, and while that would be a more elegant
115+
\* spec, I think this better models the decision procedure of the
116+
\* prisoner.
117+
CounterAction(p) ==
118+
/\ p = Designated_Counter
119+
/\ IF light = "on"
120+
THEN
121+
/\ light' = "off"
122+
/\ count' = count + 1
123+
ELSE
124+
UNCHANGED <<light, count>>
125+
/\ announced' = (count' >= VictoryThreshold)
126+
/\ UNCHANGED <<signalled>>
127+
128+
\* The action taken by the other prisoners, if they are placed in the
129+
\* cell
130+
\*
131+
\* Same note on the IF applies here.
132+
StandardAction(p) ==
133+
/\ p \in NormalPrisoner
134+
/\ IF light = "off" /\ signalled[p] < SignalLimit
135+
THEN
136+
/\ light' = "on"
137+
/\ signalled' = [signalled EXCEPT ![p] = @ + 1]
138+
ELSE
139+
UNCHANGED <<light, signalled>>
140+
/\ UNCHANGED <<count, announced>>
141+
142+
\* The action performed by the warden: place a prisoner in the cell
143+
\* and maintain our own view of who's been selected (so we can judge
144+
\* if a victory announcement is correct)
145+
WardenAction(p) ==
146+
\* Put one of the prisoners in the cell
147+
/\ \/ CounterAction(p)
148+
\/ StandardAction(p)
149+
150+
\* Maintain the warden's view
151+
/\ has_visited' = has_visited \union {p}
152+
153+
Next == \E p \in Prisoner: WardenAction(p)
154+
155+
Spec ==
156+
/\ Init
157+
/\ [][Next]_vars
158+
159+
\* Base assumption in the game: the warden eventually has to choose
160+
\* everyone in a way progress is possible
161+
/\ \A p \in Prisoner: WF_vars(WardenAction(p))
162+
163+
------------------------------------------------------------------------------
164+
165+
\* Goal of the game: eventually the prisoners will win
166+
Terminating == <>announced
167+
168+
------------------------------------------------------------------------------
169+
170+
\* Type invariant. Note it's possible to over-count in the lights
171+
\* unknown version, if the initial state of the light is "on". Hence
172+
\* the slightly more relaxed upper bound on count.
173+
TypeOK ==
174+
/\ count \in 1 .. VictoryThreshold + 1
175+
/\ announced \in BOOLEAN
176+
/\ signalled \in [ NormalPrisoner -> 0 .. 2 ]
177+
/\ light \in {"off", "on"}
178+
/\ has_visited \subseteq Prisoner
179+
180+
\* Invariant to make sure victory is never declared in error
181+
VictoryOK == announced => (has_visited = Prisoner)
182+
183+
====

‎specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
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

‎specifications/Prisoners_Single_Switch/README.md‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
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".
67+
68+
One final difference is that this spec also works for a single
69+
prisoner, which is of course trivial but still an interesting
70+
corner-case. These are checked in [SoloPrisoner.cfg](SoloPrisoner.cfg)
71+
and [SoloPrisonerLightUnknown.cfg](SoloPrisonerLightUnknown.cfg).

‎specifications/Prisoners_Single_Switch/SoloPrisoner.cfg‎

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

‎specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg‎

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

0 commit comments

Comments
 (0)