50 Gefangene

(Quelle: Bulletin EATCS, Puzzle Corner, 200?)

• Ein Zimmer mit Lampe + Schalter.
• Der faire Wärter führt Gefangene einzeln in das Zimmer.
• Wenn jemand STOP ruft, und zu dem Zeitpunkt alle ≥1 mal im Zimmer waren, dann werden alle freigelassen.

Spezifikation: I_k : ist-drin, W_k : war-drin

(¬W_k$\mathsf {U}$ I_k)∧$\Box$(I_k⇒$\Box$W_k)

Fairness: $\bigwedge_{k}^{}$ : $\Box$$\Diamond$I_k.          impliziert Ziel: $\Diamond$$\bigwedge_{k}^{}$W_k

Aufgabe: 1. formale Semantik von $\mathsf {U}$ (until)?

2. Lösung? (2a Lampe ist anfangs aus, 2b ...unbekannt)