statechart

Checks a TLA+ model of something that moves between states (a checkout, an upload, a protocol, a job with retries) with the TLC model checker and draws it as a Mermaid statechart in the reader's words, marking each state that breaks a rule and the shortest path to it. Use when asked to 'draw the states', 'chart how this flow works', 'statechart', 'can this ever happen', 'check this flow keeps the rule', 'model the lifecycle', or to show a bug about order, duplicates, retries or late events as a path through states. Declines work with no states, such as a pure function. Not for architecture or sequence diagrams (vd:archify, vd:diagram-design).