BlockingQueue
BlockingQueue copied to clipboard
lemmy
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
### Polish * `Starvation` -> `NoStarvation` * `Invariant` -> `NoDeadlock` or `DeadlockFree` (proof has theorem `DeadlockFreedom`) * Java `take` vs. TLA `get` action names * Align bound variable `x` in...
https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing https://github.com/lemmy/BlockingQueue/blob/0761ecfdb0e3aef3db1aa78df6f4aa0b60e5736d/.devcontainer/devcontainer.json#L10-L13 https://github.com/tlaplus/Examples/blob/f49468c12a3236ff1b39447f531378b85889e38e/.devcontainer/devcontainer.json#L14-L16
https://github.com/tlaplus/tlapm/issues/15 makes it necessary to update [TLAPS.tla](https://github.com/lemmy/BlockingQueue/blob/master/TLAPS.tla) in this repository to the newest version in TLAPM.
https://github.com/lemmy/BlockingQueue/blob/a064863fd482e2cb15389db48d1a7297a6c30851/BlockingQueuePoisonApple.tla#L103 I think that this is because of an (unstated?) presumption that producers are unwilling to block forever, so with a bounded queue you would need a PutFail action that...
