From 2a6804f8c96db83db15e003d707469c71d6cbec6 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 29 Oct 2026 08:38:59 -0700 Subject: [PATCH] DP: name the backend that proves each slow step. CI killed tlapm on DiningPhilosophers_proof.tla at its three-minute limit on macOS. The proof needed 2m55s to 2m58s there in earlier runs. tlapm tries SMT, then Zenon, then Isabelle, and CI runs it with --stretch 5. On 23 steps SMT failed, and on 12 of them Zenon failed too, each only after its stretched time limit of 25 or 50 seconds. Naming Zenon or Isa on these steps skips the attempts that fail. Locally, with --stretch 5, the proof now takes 29 seconds and no backend fails. The new limit of five minutes, the most that CI allows, leaves room for slow runners. https://github.com/tlaplus/Examples/actions/runs/40815991190 Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- .../DiningPhilosophers_proof.tla | 46 +++++++++---------- .../DiningPhilosophers/manifest.json | 2 +- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla b/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla index 2856ec3e..41fcac38 100644 --- a/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla +++ b/specifications/DiningPhilosophers/DiningPhilosophers_proof.tla @@ -116,18 +116,18 @@ LEMMA TakeAgree == <2>2. philosophers[p] = {} BY <2>1, <1>1 DEF Phases, Idle, Hungry, Eating <2>. QED - BY <1>1, <2>2 DEF TakeLeft, TakeLow + BY <1>1, <2>2, Zenon DEF TakeLeft, TakeLow <1>2. CASE TakeLeft(p) /\ p % 2 = 0 - BY <1>2 DEF TakeLeft, TakeHigh + BY <1>2, Zenon DEF TakeLeft, TakeHigh <1>3. CASE TakeRight(p) /\ p % 2 = 1 - BY <1>3 DEF TakeRight, TakeHigh + BY <1>3, Isa DEF TakeRight, TakeHigh <1>4. CASE TakeRight(p) /\ p % 2 = 0 <2>1. RightFork(p) \in P /\ RightFork(p) \notin philosophers[p] BY <1>4, ForksDistinct DEF TakeRight, OnTable <2>2. philosophers[p] = {} BY <2>1, <1>4 DEF Phases, Idle, Hungry, Eating <2>. QED - BY <1>4, <2>2 DEF TakeRight, TakeLow + BY <1>4, <2>2, Zenon DEF TakeRight, TakeLow <1>. QED BY <1>1, <1>2, <1>3, <1>4, Parity @@ -222,7 +222,7 @@ THEOREM OnTableNext == Inv /\ [Next]_vars => OnTable' <1>3. ASSUME NEW p \in P, Release(p) PROVE g \in forks' <=> \A r \in P : g \notin philosophers'[r] <2>1. CASE g \in {LowFork(p), HighFork(p)} - BY <1>3, <2>1, ReleaseFrame DEF Exclusive + BY <1>3, <2>1, ReleaseFrame, Zenon DEF Exclusive <2>2. CASE g \notin {LowFork(p), HighFork(p)} <3>1. \A r \in P : g \in philosophers'[r] <=> g \in philosophers[r] BY <1>3, <2>2, ReleaseFrame @@ -285,10 +285,10 @@ BY InvInit, InvNext, PTL DEF Spec Act(p) == TakeLeft(p) \/ TakeRight(p) \/ Release(p) LEMMA SpecNext == Spec => [][Next]_vars -BY DEF Spec +BY Isa DEF Spec LEMMA SpecFair == \A q \in P : Spec => SF_vars(Act(q)) -BY DEF Spec, Act +BY Isa DEF Spec, Act \* A step either is a step of q or leaves q's forks alone. LEMMA NextSplit == @@ -340,9 +340,9 @@ LEMMA IdleEnabled == forks \ {LeftFork(q)}>> # <> BY <1>1 <2>3. ENABLED <>_vars - BY <1>1, <1>2, <2>1, <2>2, ExpandENABLED DEF TakeLeft, vars + BY <1>1, <1>2, <2>1, <2>2, ExpandENABLED, Isa DEF TakeLeft, vars <2>. QED - BY <2>3, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + BY <2>3, ExpandENABLED, Zenon DEF Act, TakeLeft, TakeRight, Release, vars <1>3. CASE q % 2 = 0 <2>1. RightFork(q) \in forks BY <1>3 DEF LowFork @@ -350,9 +350,9 @@ LEMMA IdleEnabled == forks \ {RightFork(q)}>> # <> BY <1>1 <2>3. ENABLED <>_vars - BY <1>1, <1>3, <2>1, <2>2, ExpandENABLED DEF TakeRight, vars + BY <1>1, <1>3, <2>1, <2>2, ExpandENABLED, Isa DEF TakeRight, vars <2>. QED - BY <2>3, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + BY <2>3, ExpandENABLED, Zenon DEF Act, TakeLeft, TakeRight, Release, vars <1>. QED BY <1>2, <1>3, Parity @@ -375,9 +375,9 @@ LEMMA HungryEnabled == <2>3. (q % 2 = 1 => philosophers[q] = {LeftFork(q)}) /\ RightFork(q) \in forks BY <2>1 <2>4. ENABLED <>_vars - BY <2>2, <2>3, ExpandENABLED DEF TakeRight, vars + BY <2>2, <2>3, ExpandENABLED, Isa DEF TakeRight, vars <2>. QED - BY <2>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + BY <2>4, ExpandENABLED, Zenon DEF Act, TakeLeft, TakeRight, Release, vars <1>4. CASE q % 2 = 0 <2>1. philosophers[q] = {RightFork(q)} /\ LeftFork(q) \in forks BY <1>1, <1>4 DEF LowFork, HighFork @@ -387,9 +387,9 @@ LEMMA HungryEnabled == <2>3. (q % 2 = 0 => philosophers[q] = {RightFork(q)}) /\ LeftFork(q) \in forks BY <2>1 <2>4. ENABLED <>_vars - BY <2>2, <2>3, ExpandENABLED DEF TakeLeft, vars + BY <2>2, <2>3, ExpandENABLED, Isa DEF TakeLeft, vars <2>. QED - BY <2>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + BY <2>4, ExpandENABLED, Zenon DEF Act, TakeLeft, TakeRight, Release, vars <1>. QED BY <1>3, <1>4, Parity @@ -408,9 +408,9 @@ LEMMA EatingEnabled == # <> BY <1>1, <1>2 <1>4. ENABLED <>_vars - BY <1>1, <1>3, ExpandENABLED DEF Release, vars + BY <1>1, <1>3, ExpandENABLED, Isa DEF Release, vars <1>. QED - BY <1>4, ExpandENABLED DEF Act, TakeLeft, TakeRight, Release, vars + BY <1>4, ExpandENABLED, Zenon DEF Act, TakeLeft, TakeRight, Release, vars ----------------------------------------------------------------------------- (***************************************************************************) @@ -445,7 +445,7 @@ LEMMA IdleHungry == <1>3. Inv /\ Idle(q) /\ LowFork(q) \in forks => ENABLED <>_vars BY IdleEnabled <1>4. Spec => SF_vars(Act(q)) - BY SpecFair + BY SpecFair, Isa <1>. QED BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF FreeIO, IdleToHungry @@ -466,7 +466,7 @@ LEMMA HungryEat == <1>3. Inv /\ Hungry(q) /\ HighFork(q) \in forks => ENABLED <>_vars BY HungryEnabled <1>4. Spec => SF_vars(Act(q)) - BY SpecFair + BY SpecFair, Isa <1>. QED BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF FreeIO, HungryToEating @@ -488,7 +488,7 @@ LEMMA EatRelease == <1>3. Inv /\ HeldEat(f, q) => ENABLED <>_vars BY EatingEnabled DEF HeldEat <1>4. Spec => SF_vars(Act(q)) - BY SpecFair + BY SpecFair, Isa <1>. QED BY <1>1, <1>2, <1>3, <1>4, InvSpec, SpecNext, PTL DEF EatingFrees @@ -595,7 +595,7 @@ THEOREM AllFree == \A f \in P : Spec => FreeIO(f) BY <2>1 <1>. HIDE DEF Q <1>3. \A m \in Nat : Q(m) - BY <1>1, <1>2, NatInduction + BY <1>1, <1>2, NatInduction, Isa <1>4. Q(3) BY <1>3 <1>. QED @@ -616,7 +616,7 @@ LEMMA EatingIsEating == \A p \in P : Eating(p) => IsEating(p) <1>3. Cardinality({LowFork(p)} \cup {HighFork(p)}) = 2 BY <1>1, <1>2, FS_AddElement <1>. QED - BY <1>3 DEF Eating, IsEating + BY <1>3, Zenon DEF Eating, IsEating THEOREM StarvationFreedom <1>. SUFFICES ASSUME NEW p \in P PROVE Spec => []<>IsEating(p) @@ -666,7 +666,7 @@ BY StarvationFreedom, StarvationImpliesNoLivelock LEMMA ActEnabledNext == ASSUME NEW q \in P PROVE (ENABLED <>_vars) => ENABLED Next -BY ExpandENABLED DEF Act, Next, TakeLeft, TakeRight, Release, vars +BY ExpandENABLED, Zenon DEF Act, Next, TakeLeft, TakeRight, Release, vars LEMMA EvenFree == ASSUME Inv, \A q \in P : ~Eating(q), NEW f \in P, Rank(f) = 2 diff --git a/specifications/DiningPhilosophers/manifest.json b/specifications/DiningPhilosophers/manifest.json index 46546f4b..c25c8966 100644 --- a/specifications/DiningPhilosophers/manifest.json +++ b/specifications/DiningPhilosophers/manifest.json @@ -85,7 +85,7 @@ "features": [], "models": [], "proof": { - "maxRuntimeMinutes": 3 + "maxRuntimeMinutes": 5 } } ]