smv-model-extractor
Installation
SKILL.md
SMV Model Extractor
SMV is for small, finite, synchronous systems — think hardware controllers, protocol handshakes, embedded state machines. Compared to → program-to-tlaplus-spec-generator: SMV is synchronous (all transitions fire together) and finite by construction; TLA+ is asynchronous and handles unbounded state.
When SMV over TLA+
| Characteristic | SMV fits | TLA+ fits |
|---|---|---|
| State space | Naturally finite (< 10⁸ states ideally) | Can be unbounded (abstracted) |
| Execution model | Synchronous — all modules step together | Asynchronous interleaving |
| Property language | CTL (branching) + LTL | TLA (linear, actions) |
| Source domain | Hardware, embedded, protocol handshakes | Distributed systems, concurrency |