lemmy · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026
diff --git a/.github/workflows/run.sh b/.github/workflows/run.sh
@@ -39,8 +39,8 @@ echo Check MCDieHarder
 $TLC_COMMAND specifications/DieHard/MCDieHarder || (($? == 12))  ## Expect a safety violation
 echo Check DieHard
 $TLC_COMMAND specifications/DieHard/DieHard || (($? == 12))  ## Expect a safety violation
-echo Check DiningPhilosophers
-$TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophers
+echo Check DiningPhilosophersPCal
+$TLC_COMMAND specifications/DiningPhilosophers/DiningPhilosophersPCal
 echo Check TransitiveClosure
 $TLC_COMMAND specifications/TransitiveClosure/TransitiveClosure
 echo Check MCEcho

diff --git a/README.md b/README.md
@@ -33,7 +33,7 @@ Here is a list of specs included in this repository which are validated by the C
 | [Boyer-Moore Majority Vote](specifications/Majority)                                                | Stephan Merz                                        |    ✔     |      ✔      |         |     ✔     |          |
 | [Proof x+x is Even](specifications/sums_even)                                                       | Martin Riener                                       |    ✔     |      ✔      |         |     ✔     |          |
 | [The N-Queens Puzzle](specifications/N-Queens)                                                      | Stephan Merz                                        |    ✔     |             |    ✔    |     ✔     |          |
-| [The Dining Philosophers Problem](specifications/DiningPhilosophers)                                | Jeff Hemphill                                       |    ✔     |             |    ✔    |     ✔     |    ✔     |
+| [The Dining Philosophers Problem](specifications/DiningPhilosophers)                                | Jeff Hemphill, Markus Kuppe                         |    ✔     |      ✔      |   (✔)   |     ✔     |    ✔     |
 | [The Car Talk Puzzle](specifications/CarTalkPuzzle)                                                 | Leslie Lamport                                      |    ✔     |             |         |     ✔     |          |
 | [The Die Hard Problem](specifications/DieHard)                                                      | Leslie Lamport                                      |    ✔     |      ✔      |         |     ✔     |    ✔     |
 | [The Prisoners & Switches Puzzle](specifications/Prisoners)                                         | Leslie Lamport                                      |    ✔     |             |         |     ✔     |          |

diff --git a/specifications/DiningPhilosophers/APDiningPhilosophers.tla b/specifications/DiningPhilosophers/APDiningPhilosophers.tla
@@ -1,5 +1,5 @@
 ---- MODULE APDiningPhilosophers ----
-(* Apalache type annotations for DiningPhilosophers.tla, applied via
+(* Apalache type annotations for DiningPhilosophersPCal.tla, applied via
    INSTANCE so the original spec remains free of tool-specific
    idiosyncrasies. *)
 
@@ -17,6 +17,6 @@ VARIABLES
   \* @type: Int -> Bool;
   hungry
 
-INSTANCE DiningPhilosophers
+INSTANCE DiningPhilosophersPCal
 
 ====
diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.cfg b/specifications/DiningPhilosophers/DiningPhilosophers.cfg
@@ -1,9 +1,4 @@
-\* Add statements after this line.
+CONSTANTS N = 5
 SPECIFICATION Spec
-CONSTANT
-    NP = 5
-INVARIANT
-    TypeOK
-    ExclusiveAccess
-PROPERTY
-    NobodyStarves
+INVARIANT TypeOK NoDeadlock
+PROPERTY NoLivelock NoStarvation
diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.tla b/specifications/DiningPhilosophers/DiningPhilosophers.tla
@@ -1,232 +1,95 @@
----- MODULE DiningPhilosophers ----
+---------------------------- MODULE DiningPhilosophers ----------------------------
 
-(*
-TLA+ / PlusCal implementation of the Dining Philosophers problem.
-Based on the exercise given in https://learntla.com/temporal-logic/operators/
+EXTENDS Naturals, FiniteSets
 
-This is an implementation of the Chandy-Misra solution.
-https://en.wikipedia.org/wiki/Dining_philosophers_problem#Chandy/Misra_solution
+CONSTANT N \* Number of philosophers
+ASSUME NIsPosNat == N \in Nat \ {0}
 
-In Dijkstra's original formulation of the problem, philosophers may not speak
-to each other and cannot hand forks to each other.
+P == 1..N
 
-In the Chandy-Misra formulation, philosophers may hand forks directly to each
-other.
-
-I ran this with alygin's TLA+ extension for VSCode:
-  https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus
-"> TLA+: Parse module" updates the translated TLA+ to match the PlusCal
-  'algorithm' above.
-"> TLA+: Check model with TLC" checks the model's correctness.
-
-You can also use TLA+ Toolbox. You may need to "create a model" and
-use the UI to add the invariants and properties at the bottom of this file.
-*)
-
-EXTENDS Integers, TLC
-
-CONSTANTS
-    \* Number of philosophers
-    NP
-
-ASSUME
-    /\ NP \in Nat \ {0}
+LeftFork(p) == p
+RightFork(p) == (p % N) + 1
 
-(* --algorithm DiningPhilosophers
+ASSUME ForksDistinct == \A p \in P : RightFork(p) \in P /\ RightFork(p) # LeftFork(p)
+ASSUME ForksCovered == {RightFork(p) : p \in P} = P
 
-variables
-    forks = [
-        fork \in 1..NP |-> [
-            \* We start with each fork held by the lowest-number philosopher
-            \* adjacent to the fork.
-            holder |-> IF fork = 2 THEN 1 ELSE fork,
-            \* Each fork starts out "dirty". Eating causes a fork to become
-            \* dirty, after which the philosopher must clean the fork and hand
-            \* it to their neighbor.
-            clean |-> FALSE
-        ]
-    ]
+VARIABLES philosophers, forks
+vars == <<philosophers, forks>>
 
-define
-    LeftFork(p) == p
-    RightFork(p) == IF p = NP THEN 1 ELSE p + 1
-
-    LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1
-    RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1
-
-    IsHoldingBothForks(p) ==
-        forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p
-    BothForksAreClean(p) ==
-        forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean
-
-    CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p)
-end define;
-
-\* This spawns 'NP' parallel Philosopher processes.
-\* 
-\* A process looks kind of like an object oriented class, but '\in 1..NP' means
-\* it's really just an integer between 1 and NP. Use 'self' to access that
-\* integer.
-\* 
-\* If you remove the 'fair' in 'fair process', each process can stop at any
-\* time and will never run again. Dining philosophers don't randomly die while
-\* clenching forks in the original problem, so let's keep the processes fair.
-fair process Philosopher \in 1..NP
-\* This acts like a member variable and you can access it like one. But we're
-\* actually creating an array with one element per process, and the "member
-\* variable" we access is just the corresponding bucket in that array.
-variables hungry = TRUE;
-begin
-Loop:
-    while TRUE do
-        \* Check if we're holding dirty forks that other philosophers might
-        \* want.
-        if
-            /\ forks[LeftFork(self)].holder = self
-            /\ ~forks[LeftFork(self)].clean
-        then
-            forks[LeftFork(self)] := [
-                holder |-> LeftPhilosopher(self),
-                clean |-> TRUE
-            ];
-        elsif
-            /\ forks[RightFork(self)].holder = self
-            /\ ~forks[RightFork(self)].clean
-        then
-            forks[RightFork(self)] := [
-                holder |-> RightPhilosopher(self),
-                clean |-> TRUE
-            ];
-        end if;
-        if hungry then
-            if CanEat(self) then
-Eat:
-                hungry := FALSE;
-                forks[LeftFork(self)].clean := FALSE ||
-                forks[RightFork(self)].clean := FALSE;
-            end if;
-        else
-Think:
-            hungry := TRUE;
-        end if;
-    end while;
-end process;
-
-end algorithm; *)
-\* BEGIN TRANSLATION (chksum(pcal) = "ea877089" /\ chksum(tla) = "16352822")
-VARIABLES forks, pc
-
-(* define statement *)
-LeftFork(p) == p
-RightFork(p) == IF p = NP THEN 1 ELSE p + 1
-
-LeftPhilosopher(p) == IF p = 1 THEN NP ELSE p - 1
-RightPhilosopher(p) == IF p = NP THEN 1 ELSE p + 1
-
-IsHoldingBothForks(p) ==
-    forks[LeftFork(p)].holder = p /\ forks[RightFork(p)].holder = p
-BothForksAreClean(p) ==
-    forks[LeftFork(p)].clean /\ forks[RightFork(p)].clean
-
-CanEat(p) == IsHoldingBothForks(p) /\ BothForksAreClean(p)
-
-VARIABLE hungry
-
-vars == << forks, pc, hungry >>
-
-ProcSet == (1..NP)
-
-Init == (* Global variables *)
-        /\ forks =         [
-                       fork \in 1..NP |-> [
-
-
-                           holder |-> IF fork = 2 THEN 1 ELSE fork,
-
-
-
-                           clean |-> FALSE
-                       ]
-                   ]
-        (* Process Philosopher *)
-        /\ hungry = [self \in 1..NP |-> TRUE]
-        /\ pc = [self \in ProcSet |-> "Loop"]
-
-Loop(self) == /\ pc[self] = "Loop"
-              /\ IF /\ forks[LeftFork(self)].holder = self
-                    /\ ~forks[LeftFork(self)].clean
-                    THEN /\ forks' = [forks EXCEPT ![LeftFork(self)] =                          [
-                                                                           holder |-> LeftPhilosopher(self),
-                                                                           clean |-> TRUE
-                                                                       ]]
-                    ELSE /\ IF /\ forks[RightFork(self)].holder = self
-                               /\ ~forks[RightFork(self)].clean
-                               THEN /\ forks' = [forks EXCEPT ![RightFork(self)] =                           [
-                                                                                       holder |-> RightPhilosopher(self),
-                                                                                       clean |-> TRUE
-                                                                                   ]]
-                               ELSE /\ TRUE
-                                    /\ forks' = forks
-              /\ IF hungry[self]
-                    THEN /\ IF CanEat(self)
-                               THEN /\ pc' = [pc EXCEPT ![self] = "Eat"]
-                               ELSE /\ pc' = [pc EXCEPT ![self] = "Loop"]
-                    ELSE /\ pc' = [pc EXCEPT ![self] = "Think"]
-              /\ UNCHANGED hungry
-
-Think(self) == /\ pc[self] = "Think"
-               /\ hungry' = [hungry EXCEPT ![self] = TRUE]
-               /\ pc' = [pc EXCEPT ![self] = "Loop"]
-               /\ forks' = forks
-
-Eat(self) == /\ pc[self] = "Eat"
-             /\ hungry' = [hungry EXCEPT ![self] = FALSE]
-             /\ forks' = [forks EXCEPT ![LeftFork(self)].clean = FALSE,
-                                       ![RightFork(self)].clean = FALSE]
-             /\ pc' = [pc EXCEPT ![self] = "Loop"]
-
-Philosopher(self) == Loop(self) \/ Think(self) \/ Eat(self)
-
-Next == (\E self \in 1..NP: Philosopher(self))
-
-Spec == /\ Init /\ [][Next]_vars
-        /\ \A self \in 1..NP : WF_vars(Philosopher(self))
-
-\* END TRANSLATION
-
-----
-(* Invariant helpers *)
-----
-
-(* TRUE iff philosophers p and q share a fork between them. *)
-ShareFork(p, q) ==
-    {LeftFork(p), RightFork(p)} \cap {LeftFork(q), RightFork(q)} /= {}
-
-----
-(* Invariants *)
-----
-
-(*
-TLA+ and PlusCal are dynamically-typed, but we can roll our own typechecking
-with an invariant.
-*)
 TypeOK ==
-    /\ forks \in [1..NP -> [holder: 1..NP, clean: BOOLEAN]]
-    /\ hungry \in [1..NP -> BOOLEAN]
-    /\ pc \in [1..NP -> {"Loop", "Eat", "Think"}]
-
-(* If two philosophers share a fork, they cannot eat at the same time. *)
-ExclusiveAccess ==
-    \A p,q \in 1..NP:
-        p /= q /\ ShareFork(p, q) => ~(pc[p] = "Eat" /\ pc[q] = "Eat")
+    /\ philosophers \in [P -> SUBSET P]
+    /\ forks \in SUBSET P
+
+Init ==
+    \* each philosopher starts with no forks
+    /\ philosophers = [ p \in P |-> {} ]
+    \* all forks are available
+    /\ forks = 1..N
+
+TakeLeft(p) ==
+    \* Philosopher N grabs the right fork first.
+    /\ p = N => philosophers[p] = {RightFork(p)}
+    /\ LeftFork(p) \in forks
+    /\ forks' = forks \ {LeftFork(p)}
+    /\ philosophers' = 
+        [philosophers EXCEPT ![p] = philosophers[p] \cup {LeftFork(p)}]
+
+TakeRight(p) ==
+    \* All other philosophers grab the left fork first.
+    /\ p # N => philosophers[p] = {LeftFork(p)}
+    /\ RightFork(p) \in forks 
+    /\ forks' = forks \ {RightFork(p)}
+    /\ philosophers' = 
+        [philosophers EXCEPT ![p] = philosophers[p] \cup {RightFork(p)}]
+
+Release(p) ==
+    /\ philosophers[p] = {LeftFork(p), RightFork(p)}
+    /\ forks' = forks \cup {LeftFork(p), RightFork(p)}
+    /\ philosophers' = [philosophers EXCEPT ![p] = {}]
+
+Next ==
+    \E p \in P:
+        \/ TakeLeft(p)
+        \/ TakeRight(p)
+        \/ Release(p)
+
+Spec ==
+    /\ Init
+    /\ [][Next]_vars
+    /\ \A p \in P :
+        SF_vars(TakeLeft(p) \/ TakeRight(p) \/ Release(p))
+
+IsEating(p) ==
+    Cardinality(philosophers[p]) = 2
+
+NoDeadlock ==
+    ENABLED Next
+
+NoLivelock ==
+    []<>(\E p \in P: IsEating(p))
+
+NoStarvation ==
+    \A p \in P: []<>IsEating(p)
+
+\* Proved in DiningPhilosophers_proof.
+THEOREM DeadlockFreedom == Spec => []NoDeadlock
+THEOREM LivelockFreedom == Spec => NoLivelock
+THEOREM StarvationFreedom == Spec => NoStarvation
+
+-----
+
+Alias ==
+    LET ThinkHungryEat(p) ==
+        IF IsEating(p) THEN "eating"
+        ELSE IF Cardinality(philosophers[p]) = 1 THEN "hungry"
+        ELSE "thinking" IN
+    [
+        philosophers |-> philosophers,
+        forks |-> forks,
+        eating |-> [ p \in DOMAIN philosophers |-> ThinkHungryEat(p) ]
+    ]
 
-----
-(* Properties *)
-----
+-----------------------------------------------------------------------------
 
-(*
-Every philosopher will eventually get to eat again.
-*)
-NobodyStarves == \A p \in 1..NP: []<>(~hungry[p])
 
-====
+=====
diff --git a/specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg b/specifications/DiningPhilosophers/DiningPhilosophersPCal.cfg
@@ -0,0 +1,9 @@
+\* Add statements after this line.
+SPECIFICATION Spec
+CONSTANT
+    NP = 5
+INVARIANT
+    TypeOK
+    ExclusiveAccess
+PROPERTY
+    NobodyStarves