TLA+ Formal Modeling Boot Camp
From naive set theory to model-checked specifications.
Continue: Sets — What They Are, What You Can Do With Them →
Foundations
Sets — What They Are, What You Can Do With Them
Set Basics
Logic — Propositions, Predicates, and Quantifiers
Logic Basics
Functions and Relations
Functions Basics
Sequences
Sequence Basics
Tla Plus Basics
Modules, State, and Variables
Traffic Light State
Actions and Next
Traffic Light Cycle
Specifications and Stuttering
Traffic Light Spec
Invariants & Running TLC
Hour Clock
Concurrency And Time
Processes & Interleaving
Two Counters
"Temporal Operators: Always and Eventually"
Always in Bounds
Fairness
Fair Counter
Weak vs. Strong Fairness
Flaky Signal