muenchnerkindl
commented
3 years ago Thank you very much for the changes. A few more comments:
- The PlusCal algorithm and the TLA+ are not in sync. In particular, there is an assignment to the variable `requesting' that is not declared in the algorithm but does appear in the TLA+ spec. However, since its value is never tested, it appears that it is unnecessary. Indeed, I removed it and the properties (see below) still hold.
- The liveness property should be strengthened to \A p \in 1..NP: []<>(~hungry[p]), ensuring that philosophers will eat repeatedly (and it holds).
- I suggest adding one or two invariants to check as well, for example type correctness and exclusive access between neighbors (even if it's pretty obvious from the protocol), as follows:
TypeOK == /\ forks \in [ 1..NP -> [holder : 1..NP, clean : BOOLEAN] ] /\ hungry \in [ 1..NP -> BOOLEAN ] /\ pc \in [ 1..NP -> {"Loop", "Eat", "Think"}]
ShareFork(p,q) == {LeftFork(p), RightFork(p)} \cap {LeftFork(q), RightFork(q)} # {} ExclusiveAccess == \A p,q \in 1..NP : p # q /\ ShareFork(p,q) => ~(pc[p] = "Eat" /\ pc[q] = "Eat")
If you agree, please make this changes and I'll merge the PR.
Best regards, Stephan
I've been trying to learn TLA+ to suss out a rare bug in my code. On https://learntla.com/temporal-logic/operators/ , I came across a toy Dining Philosophers problem. It took me several hours to make everything work and build something free of deadlocks, livelocks, or starvation, so I'd like to add my knowledge to the bank.
This model solves the problem via Dijkstra's resource hierarchy solution. You should be able to run it with no changes via VSCode or the command-line, or with minimal changes via TLA toolbox.