Conjunction Capers: A TLA+ Truffle

on YouTube ↗27m

" summary

Shows two concrete uses of composing canonical TLA+ state‑machines and how to run them in TLC by rewriting Next into a single boxed action (putting UNCHANGED conjuncts first). First, it composes rule‑threads to model Behavioral Programming and implements Tic‑Tac‑Toe with seven tactic rules that model‑checks in about seven seconds. Second, it uses composition for model‑based trace‑checking: embedding 20‑record traces (or many logs) into TLA+, letting TLC fill hidden variables to validate traces against the spec.

AI-written summary · about

" chapters (10)

1. 0:00Introduction to talk
2. 1:25TLA+ Truffles concept
3. 2:31Conjunction in TLA formulas
4. 5:05Transforming to canonical form
5. 9:09Behavioral programming example
6. 13:33Possibility properties check
7. 16:46Model-based trace checking
8. 21:30Checking multiple traces
9. 22:35Hidden variables in traces
10. 27:06Conclusion and resources