TLA+ / PlusCal implementation of the Dining Philosophers problem. Based on the exercise given in https://learntla.com/temporal-logic/operators/
This is an implementation of the Chandy-Misra solution. https://en.wikipedia.org/wiki/Dining_philosophers_problem#Chandy/Misra_solution
In Dijkstra's original formulation of the problem, philosophers may not speak to each other and cannot hand forks to each other.
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.