Workshop: TLA+ in action (Part 2)
summary
Workshop models Safra’s EWD998 termination detector in TLA+ using TLC model checking and Lamport’s tutorial style, exercises include reducing Naturals to a finite range and swapping an infinite init for an MC_init to get a finite model. The session finds a type bug, adds a global terminationDetected flag, checks invariants and temporal properties (box/diamond), probes liveness with simulate 10,000 behaviors, uses WF_vars fairness, inspects a counterexample loop in a 513 states model and a 17-state graph; design works after fixing implication and action constraints.
AI-written summary · about
chapters (8)
- 0:00Start
- 9:41Termination Detection
- 15:58Executive Summary
- 20:21The Box Operator
- 22:41Error Trace
- 28:12Simulation Mode
- 30:10Action Constraints
- 52:51Mental Model
related talks
01h 13mDesigning distributed systems with TLA+
15mTLC: Temporal Logic of Distributed Components
41mDesigning software with complex configurations
43mWeeks of Debugging Can Save You Hours of TLA+
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)
32mTLA + specification of PCR parallel programming pattern
31mTurning an Incident Report into a Design Issue with TLA+
34mTLA+ at Microsoft to build planetary-scale systems