Add a variant of the Prisoner's puzzle

[florianschanda]

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.

[ahelwer]

Thanks! CI failing due to error message:

Spec specifications/Prisoners_Single_Switch has name The prisoners & light switch puzzle in manifest and The Prisoners & Switch Puzzle in README

[florianschanda]

I have fixed the name mismatch. I suppose the generate_manifest.py script could also add a blank row with the correct name in the top-level README.md, that would be quite convenient.

[Copilot]

Pull Request Overview

This PR adds a variant of the Prisoner’s puzzle that uses a single light switch, with two modes based on whether the initial state of the light is known.

• Adds documentation and configuration files for the single switch puzzle, including variants for known and unknown light states.
• Implements a TLA+ specification for the puzzle logic and updates the repository manifest and README accordingly.

Reviewed Changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
specifications/Prisoners_Single_Switch/README.md	Introduces documentation for the single switch puzzle with a minor spelling error.
specifications/Prisoners_Single_Switch/PrisonerLightUnknown.cfg	Adds configuration for the variant where the light initial state is unknown.
specifications/Prisoners_Single_Switch/Prisoner.tla	Contains the TLA+ specification for the prisoner puzzle with comments referencing the initial state.
specifications/Prisoners_Single_Switch/Prisoner.cfg	Provides configuration with the known initial light state.
manifest.json	Updates the manifest to include the new puzzle specification.
README.md	Updates the repository index to list the new single switch puzzle.

[florianschanda]

Typos fixed

[florianschanda]

Comments from @lemmy addressed.

[lemmy]

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) < 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) > 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$).

[lemmy]

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.

[ahelwer]

@florianschanda good to know you used generate_manifest.py. I agree automatically creating an entry in the spec table would be a good feature; this was also requested by others.

[lemmy]

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.

[florianschanda]

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.

[lemmy]

LGTM, though the spec could be written in a more idiomatic TLA+ style.

[lemmy]

@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

[florianschanda]

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.

[lemmy]

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

[lemmy]

Will merge unless reviews from @ahelwer or @muenchnerkindl are pending.

[muenchnerkindl]

I had a look at the specification yesterday and it looked good to me.