Skip to content

Add a variant of the Prisoner's puzzle #172

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ahelwer merged 1 commit into from
Jun 5, 2025
Merged

Add a variant of the Prisoner's puzzle #172

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 | ✔ | | | ✔ | |
Expand Down
62 changes: 62 additions & 0 deletions manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1855,6 +1855,68 @@
}
]
},
{
"path": "specifications/Prisoners_Single_Switch",
"title": "The Prisoners & Switch Puzzle",
Copy link
Copy Markdown
Member

@lemmy lemmy Jun 2, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ahelwer Looking at the json, I’m once more left wondering why fields like title, description, authors, and tags can’t simply be included as plain text in the preamble or postamble of the spec itself (as shown below). Similarly, mode and result could be represented as comments within the MC.cfg or MC.tla files. The remaining values can be extracted automatically using SANY or a Tree-sitter parser on the spec and config files. => Contributors only have to touch their .tla and .cfg.

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.
author: Florian Schanda
tags: beginner
---- MODULE Prisoner ----

...

====

author should ideally be extracted from the git history, or from the footer that the Toolbox adds to specs.

Related: #171

Copy link
Copy Markdown
Contributor Author

@florianschanda florianschanda Jun 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would caution against taking author from the git history - e.g. you might want to add an example that somebody else wrote with their permission. Similarly maintainer commits that e.g. remove end-of-line whitespace or renamings would further muddy the history.

Copy link
Copy Markdown
Member

@lemmy lemmy Jun 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree that the footer is preferable, but unfortunately, our VSCode extension no longer encourages it. Could be another check for a TLA+ linter.

"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",
Expand Down
9 changes: 9 additions & 0 deletions specifications/Prisoners_Single_Switch/Prisoner.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CONSTANTS
Prisoner = {"Alice", "Bob", "Eve"}
Light_Unknown = FALSE

SPECIFICATION Spec
PROPERTY Terminating

INVARIANT TypeOK
INVARIANT VictoryOK
184 changes: 184 additions & 0 deletions specifications/Prisoners_Single_Switch/Prisoner.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 == <<count, announced, signalled, light, has_visited>>

------------------------------------------------------------------------------

\* 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"
Copy link
Copy Markdown
Member

@lemmy lemmy Jun 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a difference not only in syntax but also in semantics here: the ITE causes ENABLED CounterAction to hold (StandardAction too), whereas ENABLED CounterAction would not hold without the ITE. This can lead to subtle differences when it comes to fairness.

Copy link
Copy Markdown
Contributor Author

@florianschanda florianschanda Jun 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It also makes sense when considering a real possibility in the puzzle: the counter is selected and placed into the cell if the light is not on.

I understand that for actually solving this puzzle it's not interesting (you just do nothing) but the prisoner in their world has to actively decide to not do anything and that's what I wanted to model.

THEN
/\ light' = "off"
/\ count' = count + 1
ELSE
UNCHANGED <<light, count>>
/\ announced' = (count' >= VictoryThreshold)
/\ UNCHANGED <<signalled>>

\* 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 <<light, signalled>>
/\ UNCHANGED <<count, announced>>

\* The action performed by the warden: place a prisoner in the cell
Copy link
Copy Markdown
Member

@lemmy lemmy Jun 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Processes are in the eye of the beholder: If we change the operational into an more axiomatic description of the prisoner puzzle, the warden disappears.

Entities and Sets

  • Let $P = {p_1, p_2, \dots, p_N}$ be the finite set of $N$ prisoners.
  • Let $L \in {\text{ON}, \text{OFF}}$ represent the state of a single light in a special room.
  • Let $C \in P$ be the designated counter prisoner.
  • Let $V: P \rightarrow \mathbb{N}$ be a function mapping each prisoner to the number of times they have visited the special room.
  • Let $A: P \rightarrow {0, 1, 2}$ represent whether each prisoner (except the counter) has performed the action of turning the light ON (0 = never, 1 = once, 2 = twice), with upper bound depending on the variant.

Initial Conditions

  • Each prisoner is in solitary confinement.
  • The function $V$ is initialized with $V(p) = 0$ for all $p \in P$.
  • The light state $L$ is either known (e.g., OFF) or unknown.
  • The counter $C$ is fixed and known to all prisoners.

Game Dynamics

At each discrete time step:

For Non-Counter Prisoners ($p \in P \setminus {C}$)

  • Iff $L = \text{OFF}$ and $A(p) &lt; k$, then $p$ may set $L := \text{ON}$ and increment $A(p) := A(p) + 1$, where:

    • $k = 1$ for known initial light state.
    • $k = 2$ for unknown initial light state.
For the Counter Prisoner ($p = C$)

  • If $L = \text{ON}$, then:

    • Set $L := \text{OFF}$
    • Let $count := count + 1$

  • If $count = N - 1$ (or $2N - 2$ in the unknown-initial-state variant), then the counter announces that all prisoners have visited the room.

Victory Condition

  • The game ends successfully if the counter makes the announcement when each prisoner $p \in P$ has visited the room at least once (i.e., $V(p) &gt; 0$ for all $p \in P$).

  • The game ends in failure (permanent imprisonment) if the counter makes the announcement prematurely (i.e., there exists $p \in P$ with $V(p) = 0$).

\* and maintain our own view of who's been selected (so we can judge
\* if a victory announcement is correct)
WardenAction(p) ==
Copy link
Copy Markdown
Member

@lemmy lemmy Jun 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One technical reason for inlining WardenAction into StandardAction and CounterAction is that it allows TLC to produce more descriptive counterexamples, explicitly naming StandardAction and CounterAction. However, specifications should not be written solely to accommodate TLC.

\* 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)

====
9 changes: 9 additions & 0 deletions specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CONSTANTS
Prisoner = {"Alice", "Bob", "Eve"}
Light_Unknown = TRUE

SPECIFICATION Spec
PROPERTY Terminating

INVARIANT TypeOK
INVARIANT VictoryOK
71 changes: 71 additions & 0 deletions specifications/Prisoners_Single_Switch/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 <<count, announced>>

CounterAction(p) ==
/\ p = Designated_Counter
/\ light = "on"
/\ light' = "off"
/\ count' = count + 1
/\ announced' = (count' >= VictoryThreshold)
/\ UNCHANGED <<signalled>>
```

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
Comment thread
florianschanda marked this conversation as resolved.
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).
9 changes: 9 additions & 0 deletions specifications/Prisoners_Single_Switch/SoloPrisoner.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CONSTANTS
Prisoner = {"Alice"}
Light_Unknown = FALSE

SPECIFICATION Spec
PROPERTY Terminating

INVARIANT TypeOK
INVARIANT VictoryOK
9 changes: 9 additions & 0 deletions specifications/Prisoners_Single_Switch/SoloPrisonerLightUnknown.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CONSTANTS
Prisoner = {"Alice"}
Light_Unknown = TRUE

SPECIFICATION Spec
PROPERTY Terminating

INVARIANT TypeOK
INVARIANT VictoryOK