Repository navigation

DiningPhilosophers: add a pure TLA+ spec that walks from broken solutions to a proved one - #237

Merged

lemmy merged 8 commits into

Oct 20, 2026

Merged

DiningPhilosophers: add a pure TLA+ spec that walks from broken solutions to a proved one#237
lemmy merged 8 commits into
masterfrom
mku-dining

Commits on Oct 20, 2026
- DiningPhilosophers: rename the PlusCal spec to DiningPhilosophersPCal
  
  lemmy
  and
  claude
  committed
  e1e2d5f
- DiningPhilosophers: point to the current VS Code extension
  lemmy
  committed
  ee7a6e3
- DiningPhilosophers: add a pure TLA+ spec with an animation
  
  lemmy
  and
  claude
  committed
  b9d1c96
- DiningPhilosophers: take the left fork before the right fork
  
  lemmy
  and
  claude
  committed
  ced77d1
- DiningPhilosophers: put the left fork back when the right fork is taken
  
  lemmy
  and
  claude
  committed
  91c897a
- DiningPhilosophers: take both forks at once
  
  lemmy
  and
  claude
  committed
  939135f
- DiningPhilosophers: let philosopher N take its right fork first
  
  lemmy
  and
  claude
  committed
  99a39d0
- DiningPhilosophers: prove starvation freedom with TLAPS
  
  lemmy
  and
  claude
  committed
  925e668