Individual skill
statechart
Check a TLA+ model of a system that moves between states, such as a product flow, a protocol, or a service, and draw it as a Mermaid statechart. The report gives the shortest path to each state that breaks a rule. Use for /statechart, or to show a bug as a path through states.
skills/statechart/SKILL.md
Source commit 91251ca92b107de606d3958e86454441910f1179
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- Yes
- Repository scan complete
- No
- Skill scan complete
- No
- Observed behavior
- Network or broad shell
- Last checked
- Nov 5, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 18
- Repository last updated
- Nov 4, 2026
- License
- MIT
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
- agent-skills Repository topic
- ai-agents Repository topic
- claude-code Repository topic
- code-review Repository topic
- codex Repository topic
- developer-tools Repository topic
- multi-agent Repository topic
- pstack Repository topic
- skills Repository topic
- t3-code Repository topic
- engineering Derived category
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Browse files
SKILL.mdcore · 9,250 bytesreferences/render.mddoc · 3,716 bytesscripts/backends/cfg.tsruns · 1,230 bytesscripts/backends/mermaid.tsruns · 7,437 bytesscripts/backends/plain-text.tsruns · 2,343 bytesscripts/backends/report.tsruns · 7,060 bytesscripts/frontends/config.tsruns · 10,698 bytesscripts/frontends/dot.tsruns · 2,484 bytesscripts/frontends/marks.tsruns · 3,257 bytesscripts/frontends/messages.tsruns · 1,842 bytesscripts/frontends/spec.tsruns · 4,198 bytesscripts/frontends/trace.tsruns · 988 bytesscripts/frontends/value.tsruns · 4,757 bytesscripts/frontends/verdict.tsruns · 1,756 bytesscripts/frontends/view.tsruns · 4,354 bytesscripts/ir.tsruns · 15,141 bytesscripts/package.jsonruns · 233 bytesscripts/passes/annotate.tsruns · 3,738 bytesscripts/passes/label.tsruns · 8,555 bytesscripts/passes/lift.tsruns · 2,888 bytesscripts/passes/loop-check.tsruns · 2,149 bytesscripts/passes/paths.tsruns · 1,900 bytesscripts/passes/reach.tsruns · 4,063 bytesscripts/passes/region-check.tsruns · 3,525 bytesscripts/passes/regions.tsruns · 9,475 bytesscripts/pipeline.tsruns · 2,931 bytesscripts/run.tsruns · 17,319 bytesscripts/statechartruns · 991 bytesscripts/statechart.tsruns · 6,044 bytesscripts/test/ConfigOracle.javaasset · 2,717 bytesscripts/test/chart.test.tsruns · 39,702 bytesscripts/test/charts/Braces.mmdasset · 312 bytesscripts/test/charts/Escapes.mmdasset · 244 bytesscripts/test/charts/Phases.mmdasset · 584 bytesscripts/test/cli.test.tsruns · 50,337 bytesscripts/test/config-fuzz.test.tsruns · 8,719 bytesscripts/test/corpus.test.tsruns · 12,763 bytesscripts/test/corpus/Counter/ChartRun.outasset · 2,658 bytesscripts/test/corpus/Counter/Counter.cfgasset · 64 bytesscripts/test/corpus/Counter/Counter.tlaasset · 185 bytesscripts/test/corpus/Counter/chart.mmdasset · 112 bytesscripts/test/corpus/Counter/graph.dotasset · 633 bytesscripts/test/corpus/Counter/report.mddoc · 243 bytesscripts/test/corpus/Counter/sany.outasset · 38,148 bytesscripts/test/corpus/Counter/verdict-1.outasset · 2,199 bytesscripts/test/corpus/CounterAction/ChartRun.outasset · 2,780 bytesscripts/test/corpus/CounterAction/CounterAction.cfgasset · 89 bytesscripts/test/corpus/CounterAction/CounterAction.tlaasset · 255 bytesscripts/test/corpus/CounterAction/chart.mmdasset · 518 bytesscripts/test/corpus/CounterAction/graph.dotasset · 798 bytesscripts/test/corpus/CounterAction/report.mddoc · 436 bytesscripts/test/corpus/CounterAction/sany.outasset · 43,961 bytesscripts/test/corpus/CounterAction/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterAction/verdict-1.outasset · 2,152 bytesscripts/test/corpus/CounterAction/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterAction/verdict-2.outasset · 3,148 bytesscripts/test/corpus/CounterAction/verdict-3.outasset · 2,690 bytesscripts/test/corpus/CounterDeadlock/ChartRun.outasset · 2,752 bytesscripts/test/corpus/CounterDeadlock/CounterDeadlock.cfgasset · 63 bytesscripts/test/corpus/CounterDeadlock/CounterDeadlock.tlaasset · 225 bytesscripts/test/corpus/CounterDeadlock/chart.mmdasset · 462 bytesscripts/test/corpus/CounterDeadlock/graph.dotasset · 633 bytesscripts/test/corpus/CounterDeadlock/report.mddoc · 624 bytesscripts/test/corpus/CounterDeadlock/sany.outasset · 42,836 bytesscripts/test/corpus/CounterDeadlock/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterDeadlock/verdict-1.outasset · 2,160 bytesscripts/test/corpus/CounterDeadlock/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterDeadlock/verdict-2.outasset · 3,024 bytesscripts/test/corpus/CounterFan/ChartRun.outasset · 3,140 bytesscripts/test/corpus/CounterFan/CounterFan.cfgasset · 37 bytesscripts/test/corpus/CounterFan/CounterFan.tlaasset · 338 bytesscripts/test/corpus/CounterFan/chart.mmdasset · 1,771 bytesscripts/test/corpus/CounterFan/graph.dotasset · 5,433 bytesscripts/test/corpus/CounterFan/report.mddoc · 239 bytesscripts/test/corpus/CounterFan/sany.outasset · 49,584 bytesscripts/test/corpus/CounterFan/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterFan/verdict-1.outasset · 2,497 bytesscripts/test/corpus/CounterFan/verdict-2.outasset · 2,688 bytesscripts/test/corpus/CounterGuard/ChartRun.exitasset · 3 bytesscripts/test/corpus/CounterGuard/ChartRun.outasset · 3,415 bytesscripts/test/corpus/CounterGuard/CounterGuard.cfgasset · 66 bytesscripts/test/corpus/CounterGuard/CounterGuard.tlaasset · 192 bytesscripts/test/corpus/CounterGuard/chart.mmdasset · 63 bytesscripts/test/corpus/CounterGuard/graph.dotasset · 302 bytesscripts/test/corpus/CounterGuard/report.mddoc · 954 bytesscripts/test/corpus/CounterGuard/sany.outasset · 36,948 bytesscripts/test/corpus/CounterGuard/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterGuard/verdict-1.outasset · 2,433 bytesscripts/test/corpus/CounterGuard/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterGuard/verdict-2.outasset · 2,985 bytesscripts/test/corpus/CounterInitPast/ChartRun.outasset · 2,564 bytesscripts/test/corpus/CounterInitPast/CounterInitPast.cfgasset · 54 bytesscripts/test/corpus/CounterInitPast/CounterInitPast.tlaasset · 169 bytesscripts/test/corpus/CounterInitPast/chart.mmdasset · 282 bytesscripts/test/corpus/CounterInitPast/graph.dotasset · 84 bytesscripts/test/corpus/CounterInitPast/report.mddoc · 425 bytesscripts/test/corpus/CounterInitPast/sany.outasset · 36,125 bytesscripts/test/corpus/CounterInitPast/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterInitPast/verdict-1.outasset · 1,362 bytesscripts/test/corpus/CounterInitPast/verdict-2.outasset · 2,540 bytesscripts/test/corpus/CounterInitPastHolds/ChartRun.outasset · 2,547 bytesscripts/test/corpus/CounterInitPastHolds/CounterInitPastHolds.cfgasset · 50 bytesscripts/test/corpus/CounterInitPastHolds/CounterInitPastHolds.tlaasset · 171 bytesscripts/test/corpus/CounterInitPastHolds/chart.mmdasset · 16 bytesscripts/test/corpus/CounterInitPastHolds/graph.dotasset · 84 bytesscripts/test/corpus/CounterInitPastHolds/report.mddoc · 211 bytesscripts/test/corpus/CounterInitPastHolds/sany.outasset · 35,616 bytesscripts/test/corpus/CounterInitPastHolds/verdict-1.outasset · 2,089 bytesscripts/test/corpus/CounterInstance/ChartRun.outasset · 2,833 bytesscripts/test/corpus/CounterInstance/CounterInstance.cfgasset · 41 bytesscripts/test/corpus/CounterInstance/CounterInstance.tlaasset · 217 bytesscripts/test/corpus/CounterInstance/CounterSteps.tlaasset · 113 bytesscripts/test/corpus/CounterInstance/chart.mmdasset · 326 bytesscripts/test/corpus/CounterInstance/graph.dotasset · 599 bytesscripts/test/corpus/CounterInstance/report.mddoc · 295 bytesscripts/test/corpus/CounterInstance/sany.outasset · 75,094 bytesscripts/test/corpus/CounterInstance/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterInstance/verdict-1.outasset · 3,043 bytesscripts/test/corpus/CounterJump/ChartRun.outasset · 2,752 bytesscripts/test/corpus/CounterJump/CounterJump.cfgasset · 57 bytesscripts/test/corpus/CounterJump/CounterJump.tlaasset · 303 bytesscripts/test/corpus/CounterJump/chart.mmdasset · 547 bytesscripts/test/corpus/CounterJump/graph.dotasset · 1,075 bytesscripts/test/corpus/CounterJump/report.mddoc · 374 bytesscripts/test/corpus/CounterJump/sany.outasset · 46,017 bytesscripts/test/corpus/CounterJump/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterJump/verdict-1.outasset · 2,178 bytesscripts/test/corpus/CounterJump/verdict-2.outasset · 2,687 bytesscripts/test/corpus/CounterLoop/ChartRun.outasset · 2,674 bytesscripts/test/corpus/CounterLoop/CounterLoop.cfgasset · 41 bytesscripts/test/corpus/CounterLoop/CounterLoop.tlaasset · 232 bytesscripts/test/corpus/CounterLoop/chart.mmdasset · 320 bytesscripts/test/corpus/CounterLoop/graph.dotasset · 593 bytesscripts/test/corpus/CounterLoop/report.mddoc · 285 bytesscripts/test/corpus/CounterLoop/sany.outasset · 42,493 bytesscripts/test/corpus/CounterLoop/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterLoop/verdict-1.outasset · 2,866 bytesscripts/test/corpus/CounterOrder/ChartRun.outasset · 2,734 bytesscripts/test/corpus/CounterOrder/CounterOrder.cfgasset · 51 bytesscripts/test/corpus/CounterOrder/CounterOrder.tlaasset · 194 bytesscripts/test/corpus/CounterOrder/chart.mmdasset · 406 bytesscripts/test/corpus/CounterOrder/graph.dotasset · 299 bytesscripts/test/corpus/CounterOrder/report.mddoc · 606 bytesscripts/test/corpus/CounterOrder/sany.outasset · 39,895 bytesscripts/test/corpus/CounterOrder/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterOrder/verdict-1.outasset · 2,141 bytesscripts/test/corpus/CounterOrder/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterOrder/verdict-2.outasset · 2,762 bytesscripts/test/corpus/CounterRules/ChartRun.outasset · 2,927 bytesscripts/test/corpus/CounterRules/CounterRules.cfgasset · 79 bytesscripts/test/corpus/CounterRules/CounterRules.tlaasset · 265 bytesscripts/test/corpus/CounterRules/Moves.tlaasset · 70 bytesscripts/test/corpus/CounterRules/chart.mmdasset · 485 bytesscripts/test/corpus/CounterRules/graph.dotasset · 302 bytesscripts/test/corpus/CounterRules/report.mddoc · 509 bytesscripts/test/corpus/CounterRules/sany.outasset · 62,215 bytesscripts/test/corpus/CounterRules/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterRules/verdict-1.outasset · 2,290 bytesscripts/test/corpus/CounterRules/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterRules/verdict-2.outasset · 2,758 bytesscripts/test/corpus/CounterRules/verdict-3.exitasset · 3 bytesscripts/test/corpus/CounterRules/verdict-3.outasset · 3,041 bytesscripts/test/corpus/CounterRules/verdict-4.outasset · 2,824 bytesscripts/test/corpus/CounterStart/ChartRun.outasset · 2,725 bytesscripts/test/corpus/CounterStart/CounterStart.cfgasset · 53 bytesscripts/test/corpus/CounterStart/CounterStart.tlaasset · 180 bytesscripts/test/corpus/CounterStart/chart.mmdasset · 351 bytesscripts/test/corpus/CounterStart/graph.dotasset · 466 bytesscripts/test/corpus/CounterStart/report.mddoc · 343 bytesscripts/test/corpus/CounterStart/sany.outasset · 37,436 bytesscripts/test/corpus/CounterStart/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterStart/verdict-1.outasset · 1,353 bytesscripts/test/corpus/CounterStart/verdict-2.outasset · 2,702 bytesscripts/test/corpus/CounterStop/ChartRun.outasset · 2,674 bytesscripts/test/corpus/CounterStop/CounterStop.cfgasset · 53 bytesscripts/test/corpus/CounterStop/CounterStop.tlaasset · 172 bytesscripts/test/corpus/CounterStop/chart.mmdasset · 87 bytesscripts/test/corpus/CounterStop/graph.dotasset · 466 bytesscripts/test/corpus/CounterStop/report.mddoc · 127 bytesscripts/test/corpus/CounterStop/sany.outasset · 36,919 bytesscripts/test/corpus/CounterStop/verdict-1.outasset · 2,217 bytesscripts/test/corpus/CounterTie/ChartRun.outasset · 2,833 bytesscripts/test/corpus/CounterTie/CounterTie.cfgasset · 96 bytesscripts/test/corpus/CounterTie/CounterTie.tlaasset · 263 bytesscripts/test/corpus/CounterTie/chart.mmdasset · 600 bytesscripts/test/corpus/CounterTie/graph.dotasset · 798 bytesscripts/test/corpus/CounterTie/report.mddoc · 675 bytesscripts/test/corpus/CounterTie/sany.outasset · 45,338 bytesscripts/test/corpus/CounterTie/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterTie/verdict-1.outasset · 2,137 bytesscripts/test/corpus/CounterTie/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterTie/verdict-2.outasset · 2,606 bytesscripts/test/corpus/CounterTie/verdict-3.exitasset · 3 bytesscripts/test/corpus/CounterTie/verdict-3.outasset · 3,248 bytesscripts/test/corpus/CounterTie/verdict-4.outasset · 2,682 bytesscripts/test/corpus/CounterTieInGraph/ChartRun.outasset · 2,798 bytesscripts/test/corpus/CounterTieInGraph/CounterTieInGraph.cfgasset · 72 bytesscripts/test/corpus/CounterTieInGraph/CounterTieInGraph.tlaasset · 283 bytesscripts/test/corpus/CounterTieInGraph/chart.mmdasset · 455 bytesscripts/test/corpus/CounterTieInGraph/graph.dotasset · 933 bytesscripts/test/corpus/CounterTieInGraph/report.mddoc · 192 bytesscripts/test/corpus/CounterTieInGraph/sany.outasset · 47,544 bytesscripts/test/corpus/CounterTieInGraph/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterTieInGraph/verdict-1.outasset · 2,168 bytesscripts/test/corpus/CounterTieInGraph/verdict-2.outasset · 2,702 bytesscripts/test/corpus/CounterView/ChartRun.outasset · 2,836 bytesscripts/test/corpus/CounterView/CounterView.cfgasset · 96 bytesscripts/test/corpus/CounterView/CounterView.tlaasset · 264 bytesscripts/test/corpus/CounterView/chart.mmdasset · 502 bytesscripts/test/corpus/CounterView/graph.dotasset · 798 bytesscripts/test/corpus/CounterView/report.mddoc · 686 bytesscripts/test/corpus/CounterView/sany.outasset · 45,402 bytesscripts/test/corpus/CounterView/verdict-1.exitasset · 3 bytesscripts/test/corpus/CounterView/verdict-1.outasset · 2,141 bytesscripts/test/corpus/CounterView/verdict-2.exitasset · 3 bytesscripts/test/corpus/CounterView/verdict-2.outasset · 2,610 bytesscripts/test/corpus/CounterView/verdict-3.exitasset · 3 bytesscripts/test/corpus/CounterView/verdict-3.outasset · 3,256 bytesscripts/test/corpus/CounterView/verdict-4.outasset · 2,683 bytesscripts/test/corpus/CounterView/view.mjsruns · 67 bytesscripts/test/corpus/DieHard/ChartRun.outasset · 2,746 bytesscripts/test/corpus/DieHard/DieHard.cfgasset · 51 bytesscripts/test/corpus/DieHard/DieHard.tlaasset · 900 bytesscripts/test/corpus/DieHard/chart.mmdasset · 2,098 bytesscripts/test/corpus/DieHard/graph.dotasset · 10,782 bytesscripts/test/corpus/DieHard/report.mddoc · 427 bytesscripts/test/corpus/DieHard/sany.outasset · 67,417 bytesscripts/test/corpus/DieHard/verdict-1.exitasset · 3 bytesscripts/test/corpus/DieHard/verdict-1.outasset · 3,059 bytesscripts/test/corpus/DieHard/verdict-2.outasset · 2,679 bytesscripts/test/corpus/FirstRule/ChartRun.outasset · 2,773 bytesscripts/test/corpus/FirstRule/FirstRule.cfgasset · 69 bytesscripts/test/corpus/FirstRule/FirstRule.tlaasset · 173 bytesscripts/test/corpus/FirstRule/chart.mmdasset · 523 bytesscripts/test/corpus/FirstRule/graph.dotasset · 636 bytesscripts/test/corpus/FirstRule/report.mddoc · 380 bytesscripts/test/corpus/FirstRule/sany.outasset · 35,468 bytesscripts/test/corpus/FirstRule/verdict-1.exitasset · 3 bytesscripts/test/corpus/FirstRule/verdict-1.outasset · 2,134 bytesscripts/test/corpus/FirstRule/verdict-2.exitasset · 3 bytesscripts/test/corpus/FirstRule/verdict-2.outasset · 2,607 bytesscripts/test/corpus/FirstRule/verdict-3.exitasset · 3 bytesscripts/test/corpus/FirstRule/verdict-3.outasset · 2,604 bytesscripts/test/corpus/FirstRule/verdict-4.exitasset · 3 bytesscripts/test/corpus/FirstRule/verdict-4.outasset · 2,991 bytesscripts/test/corpus/HiddenClock/ChartRun.outasset · 2,675 bytesscripts/test/corpus/HiddenClock/HiddenClock.cfgasset · 71 bytesscripts/test/corpus/HiddenClock/HiddenClock.tlaasset · 290 bytesscripts/test/corpus/HiddenClock/chart.mmdasset · 277 bytesscripts/test/corpus/HiddenClock/graph.dotasset · 467 bytesscripts/test/corpus/HiddenClock/report.mddoc · 491 bytesscripts/test/corpus/HiddenClock/sany.outasset · 44,753 bytesscripts/test/corpus/HiddenClock/verdict-1.exitasset · 3 bytesscripts/test/corpus/HiddenClock/verdict-1.outasset · 2,716 bytesscripts/test/corpus/Login/ChartRun.outasset · 2,662 bytesscripts/test/corpus/Login/Login.cfgasset · 46 bytesscripts/test/corpus/Login/Login.tlaasset · 2,804 bytesscripts/test/corpus/Login/chart.mmdasset · 735 bytesscripts/test/corpus/Login/graph.dotasset · 2,946 bytesscripts/test/corpus/Login/report.mddoc · 304 bytesscripts/test/corpus/Login/sany.outasset · 61,094 bytesscripts/test/corpus/Login/verdict-1.outasset · 2,084 bytesscripts/test/corpus/Login/view.mjsruns · 47 bytesscripts/test/corpus/LoginGuarded/ChartRun.outasset · 2,683 bytesscripts/test/corpus/LoginGuarded/LoginGuarded.cfgasset · 56 bytesscripts/test/corpus/LoginGuarded/LoginGuarded.tlaasset · 3,297 bytesscripts/test/corpus/LoginGuarded/chart.mmdasset · 856 bytesscripts/test/corpus/LoginGuarded/graph.dotasset · 2,836 bytesscripts/test/corpus/LoginGuarded/report.mddoc · 295 bytesscripts/test/corpus/LoginGuarded/sany.outasset · 86,678 bytesscripts/test/corpus/LoginGuarded/verdict-1.outasset · 2,105 bytesscripts/test/corpus/LoginGuarded/view.mjsruns · 75 bytesscripts/test/corpus/LoginParallel/ChartRun.outasset · 2,765 bytesscripts/test/corpus/LoginParallel/LoginParallel.cfgasset · 76 bytesscripts/test/corpus/LoginParallel/LoginParallel.tlaasset · 2,619 bytesscripts/test/corpus/LoginParallel/chart.mmdasset · 1,114 bytesscripts/test/corpus/LoginParallel/graph.dotasset · 5,138 bytesscripts/test/corpus/LoginParallel/report.mddoc · 696 bytesscripts/test/corpus/LoginParallel/sany.outasset · 65,596 bytesscripts/test/corpus/LoginParallel/verdict-1.exitasset · 3 bytesscripts/test/corpus/LoginParallel/verdict-1.outasset · 3,109 bytesscripts/test/corpus/LoginParallel/verdict-2.outasset · 2,697 bytesscripts/test/corpus/LoginParallel/view.mjsruns · 75 bytesscripts/test/corpus/MediaPlayer/ChartRun.outasset · 2,747 bytesscripts/test/corpus/MediaPlayer/MediaPlayer.cfgasset · 77 bytesscripts/test/corpus/MediaPlayer/MediaPlayer.tlaasset · 3,514 bytesscripts/test/corpus/MediaPlayer/chart.mmdasset · 1,202 bytesscripts/test/corpus/MediaPlayer/graph.dotasset · 8,433 bytesscripts/test/corpus/MediaPlayer/report.mddoc · 506 bytesscripts/test/corpus/MediaPlayer/sany.outasset · 106,159 bytesscripts/test/corpus/MediaPlayer/verdict-1.exitasset · 3 bytesscripts/test/corpus/MediaPlayer/verdict-1.outasset · 2,239 bytesscripts/test/corpus/MediaPlayer/verdict-2.outasset · 3,573 bytesscripts/test/corpus/MediaPlayer/view.mjsruns · 195 bytesscripts/test/corpus/MediaPlayerFixed/ChartRun.outasset · 2,698 bytesscripts/test/corpus/MediaPlayerFixed/MediaPlayerFixed.cfgasset · 52 bytesscripts/test/corpus/MediaPlayerFixed/MediaPlayerFixed.tlaasset · 3,472 bytesscripts/test/corpus/MediaPlayerFixed/chart.mmdasset · 880 bytesscripts/test/corpus/MediaPlayerFixed/graph.dotasset · 7,629 bytesscripts/test/corpus/MediaPlayerFixed/report.mddoc · 363 bytesscripts/test/corpus/MediaPlayerFixed/sany.outasset · 107,448 bytesscripts/test/corpus/MediaPlayerFixed/verdict-1.outasset · 2,120 bytesscripts/test/corpus/MediaPlayerFixed/view.mjsruns · 195 bytesscripts/test/corpus/MediaPlayerProps/ChartRun.outasset · 2,853 bytesscripts/test/corpus/MediaPlayerProps/MediaPlayer.tlaasset · 3,514 bytesscripts/test/corpus/MediaPlayerProps/MediaPlayerProps.cfgasset · 107 bytesscripts/test/corpus/MediaPlayerProps/MediaPlayerProps.tlaasset · 164 bytesscripts/test/corpus/MediaPlayerProps/chart.mmdasset · 1,125 bytesscripts/test/corpus/MediaPlayerProps/graph.dotasset · 8,433 bytesscripts/test/corpus/MediaPlayerProps/report.mddoc · 766 bytesscripts/test/corpus/MediaPlayerProps/sany.outasset · 110,999 bytesscripts/test/corpus/MediaPlayerProps/verdict-1.exitasset · 3 bytesscripts/test/corpus/MediaPlayerProps/verdict-1.outasset · 2,408 bytesscripts/test/corpus/MediaPlayerProps/verdict-2.outasset · 2,861 bytesscripts/test/corpus/MediaPlayerProps/verdict-3.outasset · 2,828 bytesscripts/test/corpus/MediaPlayerProps/verdict-4.exitasset · 3 bytesscripts/test/corpus/MediaPlayerProps/verdict-4.outasset · 2,669 bytesscripts/test/corpus/MediaPlayerProps/verdict-5.exitasset · 3 bytesscripts/test/corpus/MediaPlayerProps/verdict-5.outasset · 2,292 bytesscripts/test/corpus/MediaPlayerProps/verdict-6.outasset · 2,274 bytesscripts/test/corpus/MediaPlayerProps/view.mjsruns · 195 bytesscripts/test/corpus/PickWorker/ChartRun.outasset · 2,672 bytesscripts/test/corpus/PickWorker/PickWorker.cfgasset · 125 bytesscripts/test/corpus/PickWorker/PickWorker.tlaasset · 298 bytesscripts/test/corpus/PickWorker/chart.mmdasset · 67 bytesscripts/test/corpus/PickWorker/graph.dotasset · 403 bytesscripts/test/corpus/PickWorker/report.mddoc · 303 bytesscripts/test/corpus/PickWorker/sany.outasset · 262,944 bytesscripts/test/corpus/PickWorker/verdict-1.outasset · 3,349 bytesscripts/test/corpus/Shadow/ChartRun.outasset · 2,935 bytesscripts/test/corpus/Shadow/Shadow.cfgasset · 88 bytesscripts/test/corpus/Shadow/Shadow.tlaasset · 225 bytesscripts/test/corpus/Shadow/ShadowLib.tlaasset · 146 bytesscripts/test/corpus/Shadow/ShadowSub.tlaasset · 43 bytesscripts/test/corpus/Shadow/chart.mmdasset · 115 bytesscripts/test/corpus/Shadow/graph.dotasset · 636 bytesscripts/test/corpus/Shadow/report.mddoc · 372 bytesscripts/test/corpus/Shadow/sany.outasset · 44,875 bytesscripts/test/corpus/Shadow/verdict-1.outasset · 3,026 bytesscripts/test/corpus/SpacedNames/ChartRun.outasset · 2,745 bytesscripts/test/corpus/SpacedNames/SpacedNames.cfgasset · 35 bytesscripts/test/corpus/SpacedNames/SpacedNames.tlaasset · 268 bytesscripts/test/corpus/SpacedNames/chart.mmdasset · 513 bytesscripts/test/corpus/SpacedNames/graph.dotasset · 855 bytesscripts/test/corpus/SpacedNames/report.mddoc · 297 bytesscripts/test/corpus/SpacedNames/sany.outasset · 24,142 bytesscripts/test/corpus/SpacedNames/verdict-1.exitasset · 3 bytesscripts/test/corpus/SpacedNames/verdict-1.outasset · 2,353 bytesscripts/test/corpus/SpacedNames/verdict-2.exitasset · 3 bytesscripts/test/corpus/SpacedNames/verdict-2.outasset · 2,928 bytesscripts/test/corpus/TwoPhase/ChartRun.outasset · 3,023 bytesscripts/test/corpus/TwoPhase/TwoPhase.cfgasset · 76 bytesscripts/test/corpus/TwoPhase/TwoPhase.tlaasset · 2,140 bytesscripts/test/corpus/TwoPhase/chart.mmdasset · 1,878 bytesscripts/test/corpus/TwoPhase/graph.dotasset · 38,927 bytesscripts/test/corpus/TwoPhase/report.mddoc · 818 bytesscripts/test/corpus/TwoPhase/sany.outasset · 89,545 bytesscripts/test/corpus/TwoPhase/verdict-1.exitasset · 3 bytesscripts/test/corpus/TwoPhase/verdict-1.outasset · 3,529 bytesscripts/test/corpus/TwoPhase/verdict-2.outasset · 2,685 bytesscripts/test/corpus/TwoPhase/view.mjsruns · 90 bytesscripts/test/corpus/TwoPhaseFixed/ChartRun.outasset · 2,692 bytesscripts/test/corpus/TwoPhaseFixed/TwoPhaseFixed.cfgasset · 76 bytesscripts/test/corpus/TwoPhaseFixed/TwoPhaseFixed.tlaasset · 2,108 bytesscripts/test/corpus/TwoPhaseFixed/chart.mmdasset · 1,068 bytesscripts/test/corpus/TwoPhaseFixed/graph.dotasset · 28,548 bytesscripts/test/corpus/TwoPhaseFixed/report.mddoc · 468 bytesscripts/test/corpus/TwoPhaseFixed/sany.outasset · 90,332 bytesscripts/test/corpus/TwoPhaseFixed/verdict-1.outasset · 2,113 bytesscripts/test/corpus/TwoPhaseFixed/view.mjsruns · 90 bytesscripts/test/corpus/TypeGuard/ChartRun.exitasset · 3 bytesscripts/test/corpus/TypeGuard/ChartRun.outasset · 2,966 bytesscripts/test/corpus/TypeGuard/TypeGuard.cfgasset · 54 bytesscripts/test/corpus/TypeGuard/TypeGuard.tlaasset · 187 bytesscripts/test/corpus/TypeGuard/chart.mmdasset · 370 bytesscripts/test/corpus/TypeGuard/graph.dotasset · 560 bytesscripts/test/corpus/TypeGuard/report.mddoc · 738 bytesscripts/test/corpus/TypeGuard/sany.outasset · 37,427 bytesscripts/test/corpus/TypeGuard/verdict-1.exitasset · 3 bytesscripts/test/corpus/TypeGuard/verdict-1.outasset · 2,419 bytesscripts/test/corpus/TypeGuard/verdict-2.exitasset · 3 bytesscripts/test/corpus/TypeGuard/verdict-2.outasset · 2,975 bytesscripts/test/corpus/UserNoDeadlock/ChartRun.outasset · 2,713 bytesscripts/test/corpus/UserNoDeadlock/UserNoDeadlock.cfgasset · 40 bytesscripts/test/corpus/UserNoDeadlock/UserNoDeadlock.tlaasset · 154 bytesscripts/test/corpus/UserNoDeadlock/chart.mmdasset · 477 bytesscripts/test/corpus/UserNoDeadlock/graph.dotasset · 636 bytesscripts/test/corpus/UserNoDeadlock/report.mddoc · 254 bytesscripts/test/corpus/UserNoDeadlock/sany.outasset · 35,387 bytesscripts/test/corpus/UserNoDeadlock/verdict-1.exitasset · 3 bytesscripts/test/corpus/UserNoDeadlock/verdict-1.outasset · 2,158 bytesscripts/test/corpus/UserNoDeadlock/verdict-2.exitasset · 3 bytesscripts/test/corpus/UserNoDeadlock/verdict-2.outasset · 3,022 bytesscripts/test/differential.test.tsruns · 18,644 bytesscripts/test/grid/Grid.cfgasset · 40 bytesscripts/test/grid/Grid.tlaasset · 205 bytesscripts/test/grid/sany.outasset · 40,105 bytesscripts/test/java.tsruns · 2,639 bytesscripts/test/labels.tsruns · 19,769 bytesscripts/test/messages.test.tsruns · 7,763 bytesscripts/test/pipeline.test.tsruns · 9,720 bytesscripts/test/plain-tlc.test.tsruns · 7,180 bytesscripts/test/render.test.tsruns · 3,257 bytesscripts/test/tlc-out.test.tsruns · 3,630 bytesscripts/test/tlc.tsruns · 5,743 bytesscripts/tsconfig.jsonasset · 225 bytesscripts/worker.tsruns · 1,095 bytes
Read excerpt
# Statechart
Read [the pstack-t3 runtime](../pstack-runtime/SKILL.md) before spawning workers, choosing models, scheduling, or isolating work. It maps those steps onto T3's orchestrator tools.
The chart shows how a system moves between states, in the words of the person who reads it. That person, the reader, decides whether the behavior is right.
## Run
Work in a scratch folder outside the repo. Write a TLA+ spec and its config. Then run:
```sh
<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR]
```