Workshop: TLA+ in action (Part 4)
summary
Workshop models EWD998 termination detection in TLA+, writes a low‑level spec that replaces counters with inboxes and a recursive sum, and checks safety and liveness. Using the TLC simulator a bad choose vs existential change moves state counts 17,000→70,000→200,000, showing nondeterminism cost; choose shrinks state space. Uses community modules and fold, verifies an inductive invariant with Apalache + Z3 in ~9s on a symbolic encoding, exports JSON traces to Shivas for SVG animation and compares TLC vs TLC simulator vs symbolic model checking tradeoffs.
AI-written summary · about
chapters (10)
- 0:00Start
- 9:34Recursive Functions
- 21:52The Community Modules
- 26:25Sum Operator
- 35:14Type Annotations
- 46:53The Tla plus Proof
- 1:00:03The Vector Clock Algorithm
- 1:00:39Tlc Trace
- 1:01:33Interactive Communication Graphs
- 1:09:19Tlc Simulator
related talks
01h 13mDesigning distributed systems with TLA+
15mTLC: Temporal Logic of Distributed Components
41mDesigning software with complex configurations
32mTLA + specification of PCR parallel programming pattern
43mWeeks of Debugging Can Save You Hours of TLA+
31mTurning an Incident Report into a Design Issue with TLA+
18mSmart Casual Verification of the Confidential Consortium Framework
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)