TLA+ Modeling Tips
3 days ago
- #TLA+
- #Modeling
- #Specification
- Model minimalistically by starting with a tiny core and extending only when necessary.
- Write declaratively, focusing on what must hold rather than how it is achieved.
- Avoid illegal knowledge by ensuring processes only access observable state.
- Use fine-grained atomic actions to expose real interleavings.
- Think in guarded commands rather than procedural steps.
- Regularly review the model to ensure all relevant aspects are included.
- Write TypeOK invariants early to document types explicitly.
- Define as many invariants as possible to ensure properties are explicit.
- Include progress properties to ensure eventual completion of actions.
- Be suspicious of successful model runs to avoid over-constrained models.
- Optimize model checking efficiency only after the model is robust.