tlaplus-model-reduction
Installation
SKILL.md
TLA+ Model Reduction
TLC is explicit-state: it literally visits every reachable state. State count is roughly product of each variable's domain size, raised to how many variables you have, times fanout. When that product hits billions, you're done — unless you shrink something.
Diagnose first — where's the blowup?
Run TLC with -coverage 1. Look at:
- Distinct states vs states generated — high ratio of generated/distinct means lots of redundant exploration (symmetry helps).
- States per action — one action dominates? That's your bottleneck.
- Queue size — growing unboundedly? You have an infinite state space.
| Symptom | Likely cause | Fix |
|---|---|---|
| Runs forever, queue keeps growing | Unbounded domain (Nat, Seq) | State constraint |
| Huge distinct-states count, slow | Too many processes/nodes | Shrink CONSTANTS |
| generated/distinct ratio very high | Symmetric processes | SYMMETRY set |
| One variable has huge domain | Over-precise data modeling | Abstract the data |