statechart
Model-check a TLA+ spec with TLC and turn the result into a reader-labeled Mermaid state diagram plus a report of the shortest path to every violated rule. Use on /statechart, to explain a bug as a walk through states, or to read any TLA+ result (formal verify skills route here).
Pinned to revision 4d2771eba39f, so it is the text this page describes rather than whatever the author pushed since.
Files
- skills/statechart/SKILL.md
- skills/statechart/references/render.md
- skills/statechart/scripts/README.md
- skills/statechart/scripts/lib/chart.mjs
- skills/statechart/scripts/lib/config.mjs
- skills/statechart/scripts/lib/dot.mjs
- skills/statechart/scripts/lib/files.mjs
- skills/statechart/scripts/lib/graph.mjs
- skills/statechart/scripts/lib/mermaid.mjs
- skills/statechart/scripts/lib/pipeline.mjs
- skills/statechart/scripts/lib/release.mjs
- skills/statechart/scripts/lib/replay.mjs
- skills/statechart/scripts/lib/report.mjs
- skills/statechart/scripts/lib/sany.mjs
- skills/statechart/scripts/lib/tlc-output.mjs
- skills/statechart/scripts/lib/toolchain.mjs
- skills/statechart/scripts/lib/values.mjs
- skills/statechart/scripts/lib/verdicts.mjs
- skills/statechart/scripts/lib/view.mjs
- skills/statechart/scripts/package.json
- skills/statechart/scripts/statechart
- skills/statechart/scripts/statechart.mjs
- skills/statechart/scripts/test/chart.test.mjs
- skills/statechart/scripts/test/cli.test.mjs
- skills/statechart/scripts/test/config.test.mjs
- skills/statechart/scripts/test/corpus.test.mjs
- skills/statechart/scripts/test/corpus/big/Grid.cfg
- skills/statechart/scripts/test/corpus/big/Grid.tla
- skills/statechart/scripts/test/corpus/big/expected/chart.mmd
- skills/statechart/scripts/test/corpus/big/expected/exit.txt
- skills/statechart/scripts/test/corpus/big/expected/report.md
- skills/statechart/scripts/test/corpus/big/expected/tlc.out
- skills/statechart/scripts/test/corpus/big/recordings/sany.json
- skills/statechart/scripts/test/corpus/big/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/big/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/commit/Commit.cfg
- skills/statechart/scripts/test/corpus/commit/Commit.tla
- skills/statechart/scripts/test/corpus/commit/expected/chart.mmd
- skills/statechart/scripts/test/corpus/commit/expected/exit.txt
- skills/statechart/scripts/test/corpus/commit/expected/report.md
- skills/statechart/scripts/test/corpus/commit/expected/tlc.out
- skills/statechart/scripts/test/corpus/commit/recordings/draw.json
- skills/statechart/scripts/test/corpus/commit/recordings/sany.json
- skills/statechart/scripts/test/corpus/commit/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/commit/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/commit/view.mjs
- skills/statechart/scripts/test/corpus/counter/Counter.cfg
- skills/statechart/scripts/test/corpus/counter/Counter.tla
- skills/statechart/scripts/test/corpus/counter/expected/chart.mmd
- skills/statechart/scripts/test/corpus/counter/expected/exit.txt
- skills/statechart/scripts/test/corpus/counter/expected/report.md
- skills/statechart/scripts/test/corpus/counter/expected/tlc.out
- skills/statechart/scripts/test/corpus/counter/recordings/draw.json
- skills/statechart/scripts/test/corpus/counter/recordings/sany.json
- skills/statechart/scripts/test/corpus/counter/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/counter/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/cut/Wide.cfg
- skills/statechart/scripts/test/corpus/cut/Wide.tla
- skills/statechart/scripts/test/corpus/cut/expected/chart.mmd
- skills/statechart/scripts/test/corpus/cut/expected/exit.txt
- skills/statechart/scripts/test/corpus/cut/expected/report.md
- skills/statechart/scripts/test/corpus/cut/expected/tlc.out
- skills/statechart/scripts/test/corpus/cut/recordings/sany.json
- skills/statechart/scripts/test/corpus/cut/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/cut/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/deadlock-constraint/Stack.cfg
- skills/statechart/scripts/test/corpus/deadlock-constraint/Stack.tla
- skills/statechart/scripts/test/corpus/deadlock-constraint/expected/chart.mmd
- skills/statechart/scripts/test/corpus/deadlock-constraint/expected/exit.txt
- skills/statechart/scripts/test/corpus/deadlock-constraint/expected/report.md
- skills/statechart/scripts/test/corpus/deadlock-constraint/expected/tlc.out
- skills/statechart/scripts/test/corpus/deadlock-constraint/recordings/draw.json
- skills/statechart/scripts/test/corpus/deadlock-constraint/recordings/sany.json
- skills/statechart/scripts/test/corpus/deadlock-constraint/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/deadlock-constraint/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/depths/Depths.cfg
- skills/statechart/scripts/test/corpus/depths/Depths.tla
- skills/statechart/scripts/test/corpus/depths/expected/chart.mmd
- skills/statechart/scripts/test/corpus/depths/expected/exit.txt
- skills/statechart/scripts/test/corpus/depths/expected/report.md
- skills/statechart/scripts/test/corpus/depths/expected/tlc.out
- skills/statechart/scripts/test/corpus/depths/recordings/draw.json
- skills/statechart/scripts/test/corpus/depths/recordings/sany.json
- skills/statechart/scripts/test/corpus/depths/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/depths/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/depths/recordings/verdict-3.json
- skills/statechart/scripts/test/corpus/depths/recordings/verdict-4.json
- skills/statechart/scripts/test/corpus/excluded/Gate.cfg
- skills/statechart/scripts/test/corpus/excluded/Gate.tla
- skills/statechart/scripts/test/corpus/excluded/expected/chart.mmd
- skills/statechart/scripts/test/corpus/excluded/expected/exit.txt
- skills/statechart/scripts/test/corpus/excluded/expected/report.md
- skills/statechart/scripts/test/corpus/excluded/expected/tlc.out
- skills/statechart/scripts/test/corpus/excluded/recordings/draw.json
- skills/statechart/scripts/test/corpus/excluded/recordings/sany.json
- skills/statechart/scripts/test/corpus/excluded/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/first-fails/Typo.cfg
- skills/statechart/scripts/test/corpus/first-fails/Typo.tla
- skills/statechart/scripts/test/corpus/first-fails/expected/error.txt
- skills/statechart/scripts/test/corpus/first-fails/expected/exit.txt
- skills/statechart/scripts/test/corpus/first-fails/recordings/sany.json
- skills/statechart/scripts/test/corpus/first-fails/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/halt/Halt.cfg
- skills/statechart/scripts/test/corpus/halt/Halt.tla
- skills/statechart/scripts/test/corpus/halt/expected/chart.mmd
- skills/statechart/scripts/test/corpus/halt/expected/exit.txt
- skills/statechart/scripts/test/corpus/halt/expected/report.md
- skills/statechart/scripts/test/corpus/halt/expected/tlc-ReachesFive.out
- skills/statechart/scripts/test/corpus/halt/expected/tlc.out
- skills/statechart/scripts/test/corpus/halt/recordings/draw.json
- skills/statechart/scripts/test/corpus/halt/recordings/sany.json
- skills/statechart/scripts/test/corpus/halt/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/hidden-clock/Clock.cfg
- skills/statechart/scripts/test/corpus/hidden-clock/Clock.tla
- skills/statechart/scripts/test/corpus/hidden-clock/expected/chart.mmd
- skills/statechart/scripts/test/corpus/hidden-clock/expected/exit.txt
- skills/statechart/scripts/test/corpus/hidden-clock/expected/report.md
- skills/statechart/scripts/test/corpus/hidden-clock/expected/tlc.out
- skills/statechart/scripts/test/corpus/hidden-clock/recordings/draw.json
- skills/statechart/scripts/test/corpus/hidden-clock/recordings/sany.json
- skills/statechart/scripts/test/corpus/hidden-clock/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/initial/Depths.cfg
- skills/statechart/scripts/test/corpus/initial/Depths.tla
- skills/statechart/scripts/test/corpus/initial/expected/chart.mmd
- skills/statechart/scripts/test/corpus/initial/expected/exit.txt
- skills/statechart/scripts/test/corpus/initial/expected/report.md
- skills/statechart/scripts/test/corpus/initial/expected/tlc.out
- skills/statechart/scripts/test/corpus/initial/recordings/draw.json
- skills/statechart/scripts/test/corpus/initial/recordings/sany.json
- skills/statechart/scripts/test/corpus/initial/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/initial/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/instance/Light.tla
- skills/statechart/scripts/test/corpus/instance/Wrapped.cfg
- skills/statechart/scripts/test/corpus/instance/Wrapped.tla
- skills/statechart/scripts/test/corpus/instance/expected/chart.mmd
- skills/statechart/scripts/test/corpus/instance/expected/exit.txt
- skills/statechart/scripts/test/corpus/instance/expected/report.md
- skills/statechart/scripts/test/corpus/instance/expected/tlc-ReachesBlue.out
- skills/statechart/scripts/test/corpus/instance/expected/tlc.out
- skills/statechart/scripts/test/corpus/instance/recordings/draw.json
- skills/statechart/scripts/test/corpus/instance/recordings/sany.json
- skills/statechart/scripts/test/corpus/instance/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/jugs/Jugs.cfg
- skills/statechart/scripts/test/corpus/jugs/Jugs.tla
- skills/statechart/scripts/test/corpus/jugs/expected/chart.mmd
- skills/statechart/scripts/test/corpus/jugs/expected/exit.txt
- skills/statechart/scripts/test/corpus/jugs/expected/report.md
- skills/statechart/scripts/test/corpus/jugs/expected/tlc.out
- skills/statechart/scripts/test/corpus/jugs/recordings/draw.json
- skills/statechart/scripts/test/corpus/jugs/recordings/sany.json
- skills/statechart/scripts/test/corpus/jugs/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/jugs/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/later-fails/Later.cfg
- skills/statechart/scripts/test/corpus/later-fails/Later.tla
- skills/statechart/scripts/test/corpus/later-fails/expected/chart.mmd
- skills/statechart/scripts/test/corpus/later-fails/expected/exit.txt
- skills/statechart/scripts/test/corpus/later-fails/expected/report.md
- skills/statechart/scripts/test/corpus/later-fails/expected/tlc.out
- skills/statechart/scripts/test/corpus/later-fails/recordings/draw.json
- skills/statechart/scripts/test/corpus/later-fails/recordings/sany.json
- skills/statechart/scripts/test/corpus/later-fails/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/later-fails/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/light/Light.cfg
- skills/statechart/scripts/test/corpus/light/Light.tla
- skills/statechart/scripts/test/corpus/light/expected/chart.mmd
- skills/statechart/scripts/test/corpus/light/expected/exit.txt
- skills/statechart/scripts/test/corpus/light/expected/report.md
- skills/statechart/scripts/test/corpus/light/expected/tlc-EventuallyBlue.out
- skills/statechart/scripts/test/corpus/light/expected/tlc.out
- skills/statechart/scripts/test/corpus/light/recordings/draw.json
- skills/statechart/scripts/test/corpus/light/recordings/sany.json
- skills/statechart/scripts/test/corpus/light/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/light/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/light/recordings/verdict-3.json
- skills/statechart/scripts/test/corpus/light/recordings/verdict-4.json
- skills/statechart/scripts/test/corpus/login-regions/Session.cfg
- skills/statechart/scripts/test/corpus/login-regions/Session.tla
- skills/statechart/scripts/test/corpus/login-regions/expected/chart.mmd
- skills/statechart/scripts/test/corpus/login-regions/expected/exit.txt
- skills/statechart/scripts/test/corpus/login-regions/expected/report.md
- skills/statechart/scripts/test/corpus/login-regions/expected/tlc.out
- skills/statechart/scripts/test/corpus/login-regions/recordings/draw.json
- skills/statechart/scripts/test/corpus/login-regions/recordings/sany.json
- skills/statechart/scripts/test/corpus/login-regions/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/login-regions/view.mjs
- skills/statechart/scripts/test/corpus/login/Login.cfg
- skills/statechart/scripts/test/corpus/login/Login.tla
- skills/statechart/scripts/test/corpus/login/expected/chart.mmd
- skills/statechart/scripts/test/corpus/login/expected/exit.txt
- skills/statechart/scripts/test/corpus/login/expected/report.md
- skills/statechart/scripts/test/corpus/login/expected/tlc.out
- skills/statechart/scripts/test/corpus/login/recordings/draw.json
- skills/statechart/scripts/test/corpus/login/recordings/sany.json
- skills/statechart/scripts/test/corpus/login/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/login/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/login/view.mjs
- skills/statechart/scripts/test/corpus/merge/Count.cfg
- skills/statechart/scripts/test/corpus/merge/Count.tla
- skills/statechart/scripts/test/corpus/merge/expected/chart.mmd
- skills/statechart/scripts/test/corpus/merge/expected/exit.txt
- skills/statechart/scripts/test/corpus/merge/expected/report.md
- skills/statechart/scripts/test/corpus/merge/expected/tlc.out
- skills/statechart/scripts/test/corpus/merge/recordings/draw.json
- skills/statechart/scripts/test/corpus/merge/recordings/sany.json
- skills/statechart/scripts/test/corpus/merge/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/merge/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/merge/view.mjs
- skills/statechart/scripts/test/corpus/no-init/Empty.cfg
- skills/statechart/scripts/test/corpus/no-init/Empty.tla
- skills/statechart/scripts/test/corpus/no-init/expected/exit.txt
- skills/statechart/scripts/test/corpus/no-init/expected/report.md
- skills/statechart/scripts/test/corpus/no-init/expected/tlc.out
- skills/statechart/scripts/test/corpus/no-init/recordings/draw.json
- skills/statechart/scripts/test/corpus/no-init/recordings/sany.json
- skills/statechart/scripts/test/corpus/no-init/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/nodeadlock-name/Finish.cfg
- skills/statechart/scripts/test/corpus/nodeadlock-name/Finish.tla
- skills/statechart/scripts/test/corpus/nodeadlock-name/expected/chart.mmd
- skills/statechart/scripts/test/corpus/nodeadlock-name/expected/exit.txt
- skills/statechart/scripts/test/corpus/nodeadlock-name/expected/report.md
- skills/statechart/scripts/test/corpus/nodeadlock-name/expected/tlc.out
- skills/statechart/scripts/test/corpus/nodeadlock-name/recordings/draw.json
- skills/statechart/scripts/test/corpus/nodeadlock-name/recordings/sany.json
- skills/statechart/scripts/test/corpus/nodeadlock-name/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/nodeadlock-name/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/odd-names/Odd.cfg
- skills/statechart/scripts/test/corpus/odd-names/Odd.tla
- skills/statechart/scripts/test/corpus/odd-names/expected/chart.mmd
- skills/statechart/scripts/test/corpus/odd-names/expected/exit.txt
- skills/statechart/scripts/test/corpus/odd-names/expected/report.md
- skills/statechart/scripts/test/corpus/odd-names/expected/tlc.out
- skills/statechart/scripts/test/corpus/odd-names/recordings/draw.json
- skills/statechart/scripts/test/corpus/odd-names/recordings/sany.json
- skills/statechart/scripts/test/corpus/odd-names/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/odd-names/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/partial/Guard.cfg
- skills/statechart/scripts/test/corpus/partial/Guard.tla
- skills/statechart/scripts/test/corpus/partial/expected/chart.mmd
- skills/statechart/scripts/test/corpus/partial/expected/exit.txt
- skills/statechart/scripts/test/corpus/partial/expected/report.md
- skills/statechart/scripts/test/corpus/partial/expected/tlc.out
- skills/statechart/scripts/test/corpus/partial/recordings/draw.json
- skills/statechart/scripts/test/corpus/partial/recordings/sany.json
- skills/statechart/scripts/test/corpus/partial/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/past/Tank.cfg
- skills/statechart/scripts/test/corpus/past/Tank.tla
- skills/statechart/scripts/test/corpus/past/expected/chart.mmd
- skills/statechart/scripts/test/corpus/past/expected/exit.txt
- skills/statechart/scripts/test/corpus/past/expected/report.md
- skills/statechart/scripts/test/corpus/past/expected/tlc.out
- skills/statechart/scripts/test/corpus/past/recordings/draw.json
- skills/statechart/scripts/test/corpus/past/recordings/sany.json
- skills/statechart/scripts/test/corpus/past/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/past/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/player/Player.cfg
- skills/statechart/scripts/test/corpus/player/Player.tla
- skills/statechart/scripts/test/corpus/player/expected/chart.mmd
- skills/statechart/scripts/test/corpus/player/expected/exit.txt
- skills/statechart/scripts/test/corpus/player/expected/report.md
- skills/statechart/scripts/test/corpus/player/expected/tlc-StopsForever.out
- skills/statechart/scripts/test/corpus/player/expected/tlc.out
- skills/statechart/scripts/test/corpus/player/recordings/draw.json
- skills/statechart/scripts/test/corpus/player/recordings/sany.json
- skills/statechart/scripts/test/corpus/player/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/player/recordings/verdict-2.json
- skills/statechart/scripts/test/corpus/player/recordings/verdict-3.json
- skills/statechart/scripts/test/corpus/player/recordings/verdict-4.json
- skills/statechart/scripts/test/corpus/player/recordings/verdict-5.json
- skills/statechart/scripts/test/corpus/player/view.mjs
- skills/statechart/scripts/test/corpus/sany-error/Broken.cfg
- skills/statechart/scripts/test/corpus/sany-error/Broken.tla
- skills/statechart/scripts/test/corpus/sany-error/expected/error.txt
- skills/statechart/scripts/test/corpus/sany-error/expected/exit.txt
- skills/statechart/scripts/test/corpus/sany-error/recordings/sany.json
- skills/statechart/scripts/test/corpus/symmetry/Pool.cfg
- skills/statechart/scripts/test/corpus/symmetry/Pool.tla
- skills/statechart/scripts/test/corpus/symmetry/expected/chart.mmd
- skills/statechart/scripts/test/corpus/symmetry/expected/exit.txt
- skills/statechart/scripts/test/corpus/symmetry/expected/report.md
- skills/statechart/scripts/test/corpus/symmetry/expected/tlc.out
- skills/statechart/scripts/test/corpus/symmetry/recordings/draw.json
- skills/statechart/scripts/test/corpus/symmetry/recordings/sany.json
- skills/statechart/scripts/test/corpus/symmetry/recordings/verdict-1.json
- skills/statechart/scripts/test/corpus/symmetry/recordings/verdict-2.json
- skills/statechart/scripts/test/graph.test.mjs
- skills/statechart/scripts/test/index.js
- skills/statechart/scripts/test/live.test.mjs
- skills/statechart/scripts/test/package.json
- skills/statechart/scripts/test/support/corpus.mjs
- skills/statechart/scripts/test/support/record.mjs
- skills/statechart/scripts/test/tlc-output.test.mjs
- skills/statechart/scripts/test/values.test.mjs
- skills/statechart/scripts/test/view.test.mjs
Every link opens the file at its source, pinned to the revision this page describes.