ewd998

ewd998 copied to clipboard

### EWD998 https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF https://lynshi.github.io/posts/understanding-ewd998/ ### Recordings Hydra Conf 2021 https://www.youtube.com/watch?v=rBVhDKfg9fQ https://www.youtube.com/watch?v=N0WOXFWBnhc https://www.youtube.com/watch?v=Im63Kl3tB2g https://www.youtube.com/watch?v=FBEviGMuOK8 ### Teaching TLA+ with EWD998 https://link.springer.com/chapter/10.1007/978-3-031-27534-0_5 ### Verifying EWD998 with Apalache, TLC, and TLAPS https://arxiv.org/abs/2211.07216

lemmy

[Accessibility] Handwriting in EWD998 is difficult to read

1

The handwriting in EWD998 is difficult to read and has zero accessibility. https://twitter.com/lemmster/status/1580294056105893889 /cc @alzarei

lemmy

# Part A 1. Basics 2. Actions 3. Invariants 4. Implication 5. Implied Init & Box/Always 6. `[A]_v` 7. Temporal Formual: `Spec` 8. ENABLED 9. `_v` 10. Diamond/Eventually (liveness) 11....

lemmy

Interesting mistakes

4

The bug below only causes a safety violation on Dijkstra's invariant `Inv` with `N >= 4` and *not* with `N=3`, unless `Init` defines `token.pos \in Node`. It is also caught...

lemmy

Incremental cheat sheet showing the ASCII syntax. Prior Work: - https://github.com/tlaplus-workshops/ewd998/blob/main/docs/TLA+CheatSheet.pdf - Standard Modules chapter in Specifying Systems - https://github.com/tlaplus/PlusCalCheatSheet/blob/main/pluscal.pdf - https://github.com/OCamlPro/cheat-sheets/blob/master/tla-cheat-sheet/tla-cheat-sheet-v1.pdf - https://mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html

lemmy

- Set theory refresher - https://github.com/tlaplus-workshops/ewd998/blob/main/F.tla

lemmy

New VSCode Dev Container for TLA+

3

I have a vague memory of you asking for help to produce a VSCode dev container for TLA+. I've created one, borrowing the basic set-up (but not your commit history)...

kevinsullivan

Primarily closely read the paper's description of the algorithm and made changes to match the spec to the text description. One of the biggest changes was that nodes get marked...

xkrogen

1. msgSentNotTainted initialization `msgSentNotTainted = [ n \in Node |-> IF n=0 THEN TRUE ELSE FALSE ]` 2. bring back the safety and liveness check to the EWD998 file as...

jasperjiaguo

* Rename `InitiateProbe` to something that conveys that multiple rounds get initiated * Rename `Terminate` actions to `GoIdle` to convey that nodes do *not* shut down * Remove superfluous `pending...

lemmy