From b5a5df0aee92b559dad593d3eb8d3ddb9f7a97dc Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Fri, 6 Nov 2026 05:58:49 -0500 Subject: [PATCH 1/8] sync: import statechart and ketchup-video Statechart takes upstream's final compiler, launcher, Pele renderer instructions and test corpus (eb4db2b through 519d36a). Ketchup-video comes from 3c0fdb4. Both stay typed-only. poteto-help gets both rows, and create-formal-verification-skill tells the next agent to read and follow the typed-only statechart skill (00d5dec). Root test and typecheck now run statechart's suite. Statechart gets a lockfile, pinned typescript and @types/node, and fixes for three type errors and one macOS tmpdir symlink failure in upstream's code. Refs #262 Co-Authored-By: Claude Opus 5.5 --- .gitignore | 2 + package.json | 4 +- .../create-formal-verification-skill/SKILL.md | 2 + plugins/pstack/skills/ketchup-video/SKILL.md | 29 + plugins/pstack/skills/poteto-help/SKILL.md | 2 + plugins/pstack/skills/statechart/SKILL.md | 82 + .../skills/statechart/references/render.md | 93 ++ .../skills/statechart/scripts/backends/cfg.ts | 33 + .../statechart/scripts/backends/mermaid.ts | 201 +++ .../statechart/scripts/backends/plain-text.ts | 72 + .../statechart/scripts/backends/report.ts | 177 +++ .../pstack/skills/statechart/scripts/bun.lock | 65 + .../statechart/scripts/frontends/config.ts | 276 ++++ .../statechart/scripts/frontends/dot.ts | 74 + .../statechart/scripts/frontends/marks.ts | 93 ++ .../statechart/scripts/frontends/messages.ts | 52 + .../statechart/scripts/frontends/spec.ts | 114 ++ .../statechart/scripts/frontends/trace.ts | 24 + .../statechart/scripts/frontends/value.ts | 166 +++ .../statechart/scripts/frontends/verdict.ts | 40 + .../statechart/scripts/frontends/view.ts | 119 ++ .../pstack/skills/statechart/scripts/ir.ts | 547 +++++++ .../skills/statechart/scripts/package.json | 14 + .../statechart/scripts/passes/annotate.ts | 128 ++ .../skills/statechart/scripts/passes/label.ts | 269 ++++ .../skills/statechart/scripts/passes/lift.ts | 85 ++ .../statechart/scripts/passes/loop-check.ts | 68 + .../skills/statechart/scripts/passes/paths.ts | 60 + .../skills/statechart/scripts/passes/reach.ts | 135 ++ .../statechart/scripts/passes/region-check.ts | 97 ++ .../statechart/scripts/passes/regions.ts | 295 ++++ .../skills/statechart/scripts/pipeline.ts | 76 + .../pstack/skills/statechart/scripts/run.ts | 481 ++++++ .../skills/statechart/scripts/statechart | 29 + .../skills/statechart/scripts/statechart.ts | 164 ++ .../statechart/scripts/test/ConfigOracle.java | 63 + .../statechart/scripts/test/chart.test.ts | 1210 +++++++++++++++ .../statechart/scripts/test/charts/Braces.mmd | 7 + .../scripts/test/charts/Escapes.mmd | 11 + .../statechart/scripts/test/charts/Phases.mmd | 29 + .../statechart/scripts/test/cli.test.ts | 1316 +++++++++++++++++ .../scripts/test/config-fuzz.test.ts | 263 ++++ .../statechart/scripts/test/corpus.test.ts | 403 +++++ .../scripts/test/corpus/Counter/ChartRun.out | 57 + .../scripts/test/corpus/Counter/Counter.cfg | 3 + .../scripts/test/corpus/Counter/Counter.tla | 10 + .../scripts/test/corpus/Counter/chart.mmd | 9 + .../scripts/test/corpus/Counter/graph.dot | 16 + .../scripts/test/corpus/Counter/report.md | 7 + .../scripts/test/corpus/Counter/sany.out | 2 + .../scripts/test/corpus/Counter/verdict-1.out | 49 + .../test/corpus/CounterAction/ChartRun.out | 60 + .../corpus/CounterAction/CounterAction.cfg | 4 + .../corpus/CounterAction/CounterAction.tla | 22 + .../test/corpus/CounterAction/chart.mmd | 26 + .../test/corpus/CounterAction/graph.dot | 19 + .../test/corpus/CounterAction/report.md | 20 + .../test/corpus/CounterAction/sany.out | 2 + .../test/corpus/CounterAction/verdict-1.exit | 1 + .../test/corpus/CounterAction/verdict-1.out | 56 + .../test/corpus/CounterAction/verdict-2.exit | 1 + .../test/corpus/CounterAction/verdict-2.out | 82 + .../test/corpus/CounterAction/verdict-3.out | 57 + .../test/corpus/CounterDeadlock/ChartRun.out | 59 + .../CounterDeadlock/CounterDeadlock.cfg | 3 + .../CounterDeadlock/CounterDeadlock.tla | 11 + .../test/corpus/CounterDeadlock/chart.mmd | 22 + .../test/corpus/CounterDeadlock/graph.dot | 16 + .../test/corpus/CounterDeadlock/report.md | 17 + .../test/corpus/CounterDeadlock/sany.out | 2 + .../corpus/CounterDeadlock/verdict-1.exit | 1 + .../test/corpus/CounterDeadlock/verdict-1.out | 56 + .../corpus/CounterDeadlock/verdict-2.exit | 1 + .../test/corpus/CounterDeadlock/verdict-2.out | 77 + .../test/corpus/CounterFan/ChartRun.out | 69 + .../test/corpus/CounterFan/CounterFan.cfg | 2 + .../test/corpus/CounterFan/CounterFan.tla | 11 + .../scripts/test/corpus/CounterFan/chart.mmd | 85 ++ .../scripts/test/corpus/CounterFan/graph.dot | 70 + .../scripts/test/corpus/CounterFan/report.md | 12 + .../scripts/test/corpus/CounterFan/sany.out | 2 + .../test/corpus/CounterFan/verdict-1.exit | 1 + .../test/corpus/CounterFan/verdict-1.out | 67 + .../test/corpus/CounterFan/verdict-2.out | 57 + .../test/corpus/CounterGuard/ChartRun.exit | 1 + .../test/corpus/CounterGuard/ChartRun.out | 85 ++ .../test/corpus/CounterGuard/CounterGuard.cfg | 6 + .../test/corpus/CounterGuard/CounterGuard.tla | 13 + .../test/corpus/CounterGuard/chart.mmd | 5 + .../test/corpus/CounterGuard/graph.dot | 10 + .../test/corpus/CounterGuard/report.md | 31 + .../scripts/test/corpus/CounterGuard/sany.out | 2 + .../test/corpus/CounterGuard/verdict-1.exit | 1 + .../test/corpus/CounterGuard/verdict-1.out | 64 + .../test/corpus/CounterGuard/verdict-2.exit | 1 + .../test/corpus/CounterGuard/verdict-2.out | 77 + .../test/corpus/CounterInitPast/ChartRun.out | 55 + .../CounterInitPast/CounterInitPast.cfg | 3 + .../CounterInitPast/CounterInitPast.tla | 10 + .../test/corpus/CounterInitPast/chart.mmd | 12 + .../test/corpus/CounterInitPast/graph.dot | 6 + .../test/corpus/CounterInitPast/report.md | 12 + .../test/corpus/CounterInitPast/sany.out | 2 + .../corpus/CounterInitPast/verdict-1.exit | 1 + .../test/corpus/CounterInitPast/verdict-1.out | 33 + .../test/corpus/CounterInitPast/verdict-2.out | 54 + .../corpus/CounterInitPastHolds/ChartRun.out | 54 + .../CounterInitPastHolds.cfg | 3 + .../CounterInitPastHolds.tla | 10 + .../corpus/CounterInitPastHolds/chart.mmd | 1 + .../corpus/CounterInitPastHolds/graph.dot | 6 + .../corpus/CounterInitPastHolds/report.md | 7 + .../test/corpus/CounterInitPastHolds/sany.out | 2 + .../corpus/CounterInitPastHolds/verdict-1.out | 46 + .../test/corpus/CounterInstance/ChartRun.out | 59 + .../CounterInstance/CounterInstance.cfg | 2 + .../CounterInstance/CounterInstance.tla | 10 + .../corpus/CounterInstance/CounterSteps.tla | 6 + .../test/corpus/CounterInstance/chart.mmd | 17 + .../test/corpus/CounterInstance/graph.dot | 15 + .../test/corpus/CounterInstance/report.md | 14 + .../test/corpus/CounterInstance/sany.out | 3 + .../corpus/CounterInstance/verdict-1.exit | 1 + .../test/corpus/CounterInstance/verdict-1.out | 78 + .../test/corpus/CounterJump/ChartRun.out | 59 + .../test/corpus/CounterJump/CounterJump.cfg | 3 + .../test/corpus/CounterJump/CounterJump.tla | 19 + .../scripts/test/corpus/CounterJump/chart.mmd | 26 + .../scripts/test/corpus/CounterJump/graph.dot | 22 + .../scripts/test/corpus/CounterJump/report.md | 12 + .../scripts/test/corpus/CounterJump/sany.out | 2 + .../test/corpus/CounterJump/verdict-1.exit | 1 + .../test/corpus/CounterJump/verdict-1.out | 58 + .../test/corpus/CounterJump/verdict-2.out | 57 + .../test/corpus/CounterLoop/ChartRun.out | 57 + .../test/corpus/CounterLoop/CounterLoop.cfg | 2 + .../test/corpus/CounterLoop/CounterLoop.tla | 11 + .../scripts/test/corpus/CounterLoop/chart.mmd | 17 + .../scripts/test/corpus/CounterLoop/graph.dot | 15 + .../scripts/test/corpus/CounterLoop/report.md | 14 + .../scripts/test/corpus/CounterLoop/sany.out | 2 + .../test/corpus/CounterLoop/verdict-1.exit | 1 + .../test/corpus/CounterLoop/verdict-1.out | 76 + .../test/corpus/CounterOrder/ChartRun.out | 59 + .../test/corpus/CounterOrder/CounterOrder.cfg | 3 + .../test/corpus/CounterOrder/CounterOrder.tla | 11 + .../test/corpus/CounterOrder/chart.mmd | 19 + .../test/corpus/CounterOrder/graph.dot | 10 + .../test/corpus/CounterOrder/report.md | 15 + .../scripts/test/corpus/CounterOrder/sany.out | 2 + .../test/corpus/CounterOrder/verdict-1.exit | 1 + .../test/corpus/CounterOrder/verdict-1.out | 56 + .../test/corpus/CounterOrder/verdict-2.exit | 1 + .../test/corpus/CounterOrder/verdict-2.out | 67 + .../test/corpus/CounterRules/ChartRun.out | 62 + .../test/corpus/CounterRules/CounterRules.cfg | 6 + .../test/corpus/CounterRules/CounterRules.tla | 24 + .../test/corpus/CounterRules/Moves.tla | 5 + .../test/corpus/CounterRules/chart.mmd | 22 + .../test/corpus/CounterRules/graph.dot | 10 + .../test/corpus/CounterRules/report.md | 23 + .../scripts/test/corpus/CounterRules/sany.out | 3 + .../test/corpus/CounterRules/verdict-1.exit | 1 + .../test/corpus/CounterRules/verdict-1.out | 58 + .../test/corpus/CounterRules/verdict-2.exit | 1 + .../test/corpus/CounterRules/verdict-2.out | 66 + .../test/corpus/CounterRules/verdict-3.exit | 1 + .../test/corpus/CounterRules/verdict-3.out | 74 + .../test/corpus/CounterRules/verdict-4.out | 59 + .../test/corpus/CounterStart/ChartRun.out | 58 + .../test/corpus/CounterStart/CounterStart.cfg | 3 + .../test/corpus/CounterStart/CounterStart.tla | 15 + .../test/corpus/CounterStart/chart.mmd | 18 + .../test/corpus/CounterStart/graph.dot | 13 + .../test/corpus/CounterStart/report.md | 11 + .../scripts/test/corpus/CounterStart/sany.out | 2 + .../test/corpus/CounterStart/verdict-1.exit | 1 + .../test/corpus/CounterStart/verdict-1.out | 33 + .../test/corpus/CounterStart/verdict-2.out | 57 + .../test/corpus/CounterStop/ChartRun.out | 57 + .../test/corpus/CounterStop/CounterStop.cfg | 3 + .../test/corpus/CounterStop/CounterStop.tla | 15 + .../scripts/test/corpus/CounterStop/chart.mmd | 7 + .../scripts/test/corpus/CounterStop/graph.dot | 13 + .../scripts/test/corpus/CounterStop/report.md | 6 + .../scripts/test/corpus/CounterStop/sany.out | 2 + .../test/corpus/CounterStop/verdict-1.out | 49 + .../test/corpus/CounterTie/ChartRun.out | 61 + .../test/corpus/CounterTie/CounterTie.cfg | 4 + .../test/corpus/CounterTie/CounterTie.tla | 14 + .../scripts/test/corpus/CounterTie/chart.mmd | 30 + .../scripts/test/corpus/CounterTie/graph.dot | 19 + .../scripts/test/corpus/CounterTie/report.md | 27 + .../scripts/test/corpus/CounterTie/sany.out | 2 + .../test/corpus/CounterTie/verdict-1.exit | 1 + .../test/corpus/CounterTie/verdict-1.out | 56 + .../test/corpus/CounterTie/verdict-2.exit | 1 + .../test/corpus/CounterTie/verdict-2.out | 64 + .../test/corpus/CounterTie/verdict-3.exit | 1 + .../test/corpus/CounterTie/verdict-3.out | 87 ++ .../test/corpus/CounterTie/verdict-4.out | 57 + .../corpus/CounterTieInGraph/ChartRun.out | 60 + .../CounterTieInGraph/CounterTieInGraph.cfg | 3 + .../CounterTieInGraph/CounterTieInGraph.tla | 12 + .../test/corpus/CounterTieInGraph/chart.mmd | 23 + .../test/corpus/CounterTieInGraph/graph.dot | 19 + .../test/corpus/CounterTieInGraph/report.md | 11 + .../test/corpus/CounterTieInGraph/sany.out | 2 + .../corpus/CounterTieInGraph/verdict-1.exit | 1 + .../corpus/CounterTieInGraph/verdict-1.out | 56 + .../corpus/CounterTieInGraph/verdict-2.out | 57 + .../test/corpus/CounterView/ChartRun.out | 61 + .../test/corpus/CounterView/CounterView.cfg | 4 + .../test/corpus/CounterView/CounterView.tla | 14 + .../scripts/test/corpus/CounterView/chart.mmd | 23 + .../scripts/test/corpus/CounterView/graph.dot | 19 + .../scripts/test/corpus/CounterView/report.md | 27 + .../scripts/test/corpus/CounterView/sany.out | 2 + .../test/corpus/CounterView/verdict-1.exit | 1 + .../test/corpus/CounterView/verdict-1.out | 56 + .../test/corpus/CounterView/verdict-2.exit | 1 + .../test/corpus/CounterView/verdict-2.out | 64 + .../test/corpus/CounterView/verdict-3.exit | 1 + .../test/corpus/CounterView/verdict-3.out | 87 ++ .../test/corpus/CounterView/verdict-4.out | 57 + .../scripts/test/corpus/CounterView/view.mjs | 1 + .../scripts/test/corpus/DieHard/ChartRun.out | 59 + .../scripts/test/corpus/DieHard/DieHard.cfg | 4 + .../scripts/test/corpus/DieHard/DieHard.tla | 38 + .../scripts/test/corpus/DieHard/chart.mmd | 92 ++ .../scripts/test/corpus/DieHard/graph.dot | 126 ++ .../scripts/test/corpus/DieHard/report.md | 17 + .../scripts/test/corpus/DieHard/sany.out | 2 + .../test/corpus/DieHard/verdict-1.exit | 1 + .../scripts/test/corpus/DieHard/verdict-1.out | 91 ++ .../scripts/test/corpus/DieHard/verdict-2.out | 57 + .../test/corpus/FirstRule/ChartRun.out | 61 + .../test/corpus/FirstRule/FirstRule.cfg | 6 + .../test/corpus/FirstRule/FirstRule.tla | 11 + .../scripts/test/corpus/FirstRule/chart.mmd | 22 + .../scripts/test/corpus/FirstRule/graph.dot | 16 + .../scripts/test/corpus/FirstRule/report.md | 25 + .../scripts/test/corpus/FirstRule/sany.out | 2 + .../test/corpus/FirstRule/verdict-1.exit | 1 + .../test/corpus/FirstRule/verdict-1.out | 56 + .../test/corpus/FirstRule/verdict-2.exit | 1 + .../test/corpus/FirstRule/verdict-2.out | 64 + .../test/corpus/FirstRule/verdict-3.exit | 1 + .../test/corpus/FirstRule/verdict-3.out | 64 + .../test/corpus/FirstRule/verdict-4.exit | 1 + .../test/corpus/FirstRule/verdict-4.out | 77 + .../test/corpus/HiddenClock/ChartRun.out | 57 + .../test/corpus/HiddenClock/HiddenClock.cfg | 4 + .../test/corpus/HiddenClock/HiddenClock.tla | 11 + .../scripts/test/corpus/HiddenClock/chart.mmd | 13 + .../scripts/test/corpus/HiddenClock/graph.dot | 12 + .../scripts/test/corpus/HiddenClock/report.md | 11 + .../scripts/test/corpus/HiddenClock/sany.out | 2 + .../test/corpus/HiddenClock/verdict-1.exit | 1 + .../test/corpus/HiddenClock/verdict-1.out | 72 + .../scripts/test/corpus/Login/ChartRun.out | 57 + .../scripts/test/corpus/Login/Login.cfg | 3 + .../scripts/test/corpus/Login/Login.tla | 62 + .../scripts/test/corpus/Login/chart.mmd | 27 + .../scripts/test/corpus/Login/graph.dot | 40 + .../scripts/test/corpus/Login/report.md | 7 + .../scripts/test/corpus/Login/sany.out | 1 + .../scripts/test/corpus/Login/verdict-1.out | 47 + .../scripts/test/corpus/Login/view.mjs | 1 + .../test/corpus/LoginGuarded/ChartRun.out | 57 + .../test/corpus/LoginGuarded/LoginGuarded.cfg | 2 + .../test/corpus/LoginGuarded/LoginGuarded.tla | 64 + .../test/corpus/LoginGuarded/chart.mmd | 28 + .../test/corpus/LoginGuarded/graph.dot | 37 + .../test/corpus/LoginGuarded/report.md | 8 + .../scripts/test/corpus/LoginGuarded/sany.out | 1 + .../test/corpus/LoginGuarded/verdict-1.out | 47 + .../scripts/test/corpus/LoginGuarded/view.mjs | 1 + .../test/corpus/LoginParallel/ChartRun.out | 60 + .../corpus/LoginParallel/LoginParallel.cfg | 3 + .../corpus/LoginParallel/LoginParallel.tla | 64 + .../test/corpus/LoginParallel/chart.mmd | 44 + .../test/corpus/LoginParallel/graph.dot | 58 + .../test/corpus/LoginParallel/report.md | 17 + .../test/corpus/LoginParallel/sany.out | 1 + .../test/corpus/LoginParallel/verdict-1.exit | 1 + .../test/corpus/LoginParallel/verdict-1.out | 83 ++ .../test/corpus/LoginParallel/verdict-2.out | 57 + .../test/corpus/LoginParallel/view.mjs | 1 + .../test/corpus/MediaPlayer/ChartRun.out | 60 + .../test/corpus/MediaPlayer/MediaPlayer.cfg | 3 + .../test/corpus/MediaPlayer/MediaPlayer.tla | 103 ++ .../scripts/test/corpus/MediaPlayer/chart.mmd | 43 + .../scripts/test/corpus/MediaPlayer/graph.dot | 93 ++ .../scripts/test/corpus/MediaPlayer/report.md | 14 + .../scripts/test/corpus/MediaPlayer/sany.out | 1 + .../test/corpus/MediaPlayer/verdict-1.exit | 1 + .../test/corpus/MediaPlayer/verdict-1.out | 59 + .../test/corpus/MediaPlayer/verdict-2.out | 72 + .../scripts/test/corpus/MediaPlayer/view.mjs | 3 + .../test/corpus/MediaPlayerFixed/ChartRun.out | 57 + .../MediaPlayerFixed/MediaPlayerFixed.cfg | 2 + .../MediaPlayerFixed/MediaPlayerFixed.tla | 100 ++ .../test/corpus/MediaPlayerFixed/chart.mmd | 31 + .../test/corpus/MediaPlayerFixed/graph.dot | 85 ++ .../test/corpus/MediaPlayerFixed/report.md | 9 + .../test/corpus/MediaPlayerFixed/sany.out | 1 + .../corpus/MediaPlayerFixed/verdict-1.out | 47 + .../test/corpus/MediaPlayerFixed/view.mjs | 3 + .../test/corpus/MediaPlayerProps/ChartRun.out | 59 + .../corpus/MediaPlayerProps/MediaPlayer.tla | 103 ++ .../MediaPlayerProps/MediaPlayerProps.cfg | 3 + .../MediaPlayerProps/MediaPlayerProps.tla | 6 + .../test/corpus/MediaPlayerProps/chart.mmd | 42 + .../test/corpus/MediaPlayerProps/graph.dot | 93 ++ .../test/corpus/MediaPlayerProps/report.md | 19 + .../test/corpus/MediaPlayerProps/sany.out | 2 + .../corpus/MediaPlayerProps/verdict-1.exit | 1 + .../corpus/MediaPlayerProps/verdict-1.out | 61 + .../corpus/MediaPlayerProps/verdict-2.out | 59 + .../corpus/MediaPlayerProps/verdict-3.out | 61 + .../corpus/MediaPlayerProps/verdict-4.exit | 1 + .../corpus/MediaPlayerProps/verdict-4.out | 66 + .../corpus/MediaPlayerProps/verdict-5.exit | 1 + .../corpus/MediaPlayerProps/verdict-5.out | 58 + .../corpus/MediaPlayerProps/verdict-6.out | 49 + .../test/corpus/MediaPlayerProps/view.mjs | 3 + .../test/corpus/PickWorker/ChartRun.out | 57 + .../test/corpus/PickWorker/PickWorker.cfg | 6 + .../test/corpus/PickWorker/PickWorker.tla | 11 + .../scripts/test/corpus/PickWorker/chart.mmd | 5 + .../scripts/test/corpus/PickWorker/graph.dot | 11 + .../scripts/test/corpus/PickWorker/report.md | 7 + .../scripts/test/corpus/PickWorker/sany.out | 5 + .../test/corpus/PickWorker/verdict-1.out | 70 + .../scripts/test/corpus/Shadow/ChartRun.out | 61 + .../scripts/test/corpus/Shadow/Shadow.cfg | 4 + .../scripts/test/corpus/Shadow/Shadow.tla | 11 + .../scripts/test/corpus/Shadow/ShadowLib.tla | 6 + .../scripts/test/corpus/Shadow/ShadowSub.tla | 3 + .../scripts/test/corpus/Shadow/chart.mmd | 9 + .../scripts/test/corpus/Shadow/graph.dot | 16 + .../scripts/test/corpus/Shadow/report.md | 8 + .../scripts/test/corpus/Shadow/sany.out | 4 + .../scripts/test/corpus/Shadow/verdict-1.out | 65 + .../test/corpus/SpacedNames/ChartRun.out | 59 + .../test/corpus/SpacedNames/SpacedNames.cfg | 2 + .../test/corpus/SpacedNames/SpacedNames.tla | 9 + .../scripts/test/corpus/SpacedNames/chart.mmd | 23 + .../scripts/test/corpus/SpacedNames/graph.dot | 17 + .../scripts/test/corpus/SpacedNames/report.md | 15 + .../scripts/test/corpus/SpacedNames/sany.out | 1 + .../test/corpus/SpacedNames/verdict-1.exit | 1 + .../test/corpus/SpacedNames/verdict-1.out | 65 + .../test/corpus/SpacedNames/verdict-2.exit | 1 + .../test/corpus/SpacedNames/verdict-2.out | 75 + .../scripts/test/corpus/TwoPhase/ChartRun.out | 69 + .../scripts/test/corpus/TwoPhase/TwoPhase.cfg | 3 + .../scripts/test/corpus/TwoPhase/TwoPhase.tla | 75 + .../scripts/test/corpus/TwoPhase/chart.mmd | 60 + .../scripts/test/corpus/TwoPhase/graph.dot | 297 ++++ .../scripts/test/corpus/TwoPhase/report.md | 20 + .../scripts/test/corpus/TwoPhase/sany.out | 1 + .../test/corpus/TwoPhase/verdict-1.exit | 1 + .../test/corpus/TwoPhase/verdict-1.out | 95 ++ .../test/corpus/TwoPhase/verdict-2.out | 57 + .../scripts/test/corpus/TwoPhase/view.mjs | 1 + .../test/corpus/TwoPhaseFixed/ChartRun.out | 57 + .../corpus/TwoPhaseFixed/TwoPhaseFixed.cfg | 3 + .../corpus/TwoPhaseFixed/TwoPhaseFixed.tla | 75 + .../test/corpus/TwoPhaseFixed/chart.mmd | 37 + .../test/corpus/TwoPhaseFixed/graph.dot | 223 +++ .../test/corpus/TwoPhaseFixed/report.md | 11 + .../test/corpus/TwoPhaseFixed/sany.out | 1 + .../test/corpus/TwoPhaseFixed/verdict-1.out | 47 + .../test/corpus/TwoPhaseFixed/view.mjs | 1 + .../test/corpus/TypeGuard/ChartRun.exit | 1 + .../test/corpus/TypeGuard/ChartRun.out | 75 + .../test/corpus/TypeGuard/TypeGuard.cfg | 5 + .../test/corpus/TypeGuard/TypeGuard.tla | 11 + .../scripts/test/corpus/TypeGuard/chart.mmd | 18 + .../scripts/test/corpus/TypeGuard/graph.dot | 14 + .../scripts/test/corpus/TypeGuard/report.md | 29 + .../scripts/test/corpus/TypeGuard/sany.out | 2 + .../test/corpus/TypeGuard/verdict-1.exit | 1 + .../test/corpus/TypeGuard/verdict-1.out | 64 + .../test/corpus/TypeGuard/verdict-2.exit | 1 + .../test/corpus/TypeGuard/verdict-2.out | 75 + .../test/corpus/UserNoDeadlock/ChartRun.out | 58 + .../corpus/UserNoDeadlock/UserNoDeadlock.cfg | 2 + .../corpus/UserNoDeadlock/UserNoDeadlock.tla | 8 + .../test/corpus/UserNoDeadlock/chart.mmd | 22 + .../test/corpus/UserNoDeadlock/graph.dot | 16 + .../test/corpus/UserNoDeadlock/report.md | 15 + .../test/corpus/UserNoDeadlock/sany.out | 2 + .../test/corpus/UserNoDeadlock/verdict-1.exit | 1 + .../test/corpus/UserNoDeadlock/verdict-1.out | 56 + .../test/corpus/UserNoDeadlock/verdict-2.exit | 1 + .../test/corpus/UserNoDeadlock/verdict-2.out | 77 + .../scripts/test/differential.test.ts | 565 +++++++ .../statechart/scripts/test/grid/Grid.cfg | 2 + .../statechart/scripts/test/grid/Grid.tla | 9 + .../statechart/scripts/test/grid/sany.out | 2 + .../skills/statechart/scripts/test/java.ts | 63 + .../skills/statechart/scripts/test/labels.ts | 643 ++++++++ .../statechart/scripts/test/messages.test.ts | 212 +++ .../statechart/scripts/test/pipeline.test.ts | 270 ++++ .../statechart/scripts/test/plain-tlc.test.ts | 255 ++++ .../statechart/scripts/test/render.test.ts | 81 + .../statechart/scripts/test/tlc-out.test.ts | 90 ++ .../skills/statechart/scripts/test/tlc.ts | 158 ++ .../skills/statechart/scripts/tsconfig.json | 11 + .../skills/statechart/scripts/worker.ts | 35 + 413 files changed, 20134 insertions(+), 2 deletions(-) create mode 100644 plugins/pstack/skills/ketchup-video/SKILL.md create mode 100644 plugins/pstack/skills/statechart/SKILL.md create mode 100644 plugins/pstack/skills/statechart/references/render.md create mode 100644 plugins/pstack/skills/statechart/scripts/backends/cfg.ts create mode 100644 plugins/pstack/skills/statechart/scripts/backends/mermaid.ts create mode 100644 plugins/pstack/skills/statechart/scripts/backends/plain-text.ts create mode 100644 plugins/pstack/skills/statechart/scripts/backends/report.ts create mode 100644 plugins/pstack/skills/statechart/scripts/bun.lock create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/config.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/dot.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/marks.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/messages.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/spec.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/trace.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/value.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/verdict.ts create mode 100644 plugins/pstack/skills/statechart/scripts/frontends/view.ts create mode 100644 plugins/pstack/skills/statechart/scripts/ir.ts create mode 100644 plugins/pstack/skills/statechart/scripts/package.json create mode 100644 plugins/pstack/skills/statechart/scripts/passes/annotate.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/label.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/lift.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/loop-check.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/paths.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/reach.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/region-check.ts create mode 100644 plugins/pstack/skills/statechart/scripts/passes/regions.ts create mode 100644 plugins/pstack/skills/statechart/scripts/pipeline.ts create mode 100644 plugins/pstack/skills/statechart/scripts/run.ts create mode 100755 plugins/pstack/skills/statechart/scripts/statechart create mode 100644 plugins/pstack/skills/statechart/scripts/statechart.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/ConfigOracle.java create mode 100644 plugins/pstack/skills/statechart/scripts/test/chart.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/charts/Braces.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/charts/Escapes.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/charts/Phases.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/cli.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/config-fuzz.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/Counter.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/Counter.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Counter/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/CounterAction.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/CounterAction.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterAction/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/CounterDeadlock.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/CounterDeadlock.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterDeadlock/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/CounterFan.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/CounterFan.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterFan/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/ChartRun.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/CounterGuard.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/CounterGuard.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterGuard/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/CounterInitPast.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/CounterInitPast.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPast/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/CounterInitPastHolds.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/CounterInitPastHolds.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInitPastHolds/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/CounterInstance.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/CounterInstance.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/CounterSteps.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterInstance/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/CounterJump.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/CounterJump.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterJump/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/CounterLoop.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/CounterLoop.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterLoop/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/CounterOrder.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/CounterOrder.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterOrder/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/CounterRules.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/CounterRules.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/Moves.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-3.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterRules/verdict-4.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/CounterStart.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/CounterStart.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStart/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/CounterStop.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/CounterStop.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterStop/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/CounterTie.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/CounterTie.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-3.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTie/verdict-4.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/CounterTieInGraph.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/CounterTieInGraph.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterTieInGraph/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/CounterView.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/CounterView.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-3.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/verdict-4.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/CounterView/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/DieHard.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/DieHard.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/DieHard/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/FirstRule.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/FirstRule.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-3.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-4.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/FirstRule/verdict-4.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/HiddenClock.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/HiddenClock.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/HiddenClock/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/Login.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/Login.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Login/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/LoginGuarded.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/LoginGuarded.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginGuarded/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/LoginParallel.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/LoginParallel.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/LoginParallel/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/MediaPlayer.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/MediaPlayer.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayer/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/MediaPlayerFixed.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/MediaPlayerFixed.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerFixed/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/MediaPlayer.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/MediaPlayerProps.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/MediaPlayerProps.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-3.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-4.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-4.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-5.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-5.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/verdict-6.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/MediaPlayerProps/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/PickWorker.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/PickWorker.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/PickWorker/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/Shadow.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/Shadow.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/ShadowLib.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/ShadowSub.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/Shadow/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/SpacedNames.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/SpacedNames.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/SpacedNames/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/TwoPhase.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/TwoPhase.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhase/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/TwoPhaseFixed.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/TwoPhaseFixed.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TwoPhaseFixed/view.mjs create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/ChartRun.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/TypeGuard.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/TypeGuard.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/TypeGuard/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/ChartRun.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/UserNoDeadlock.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/UserNoDeadlock.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/chart.mmd create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/graph.dot create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/report.md create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/sany.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/verdict-1.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/verdict-1.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/verdict-2.exit create mode 100644 plugins/pstack/skills/statechart/scripts/test/corpus/UserNoDeadlock/verdict-2.out create mode 100644 plugins/pstack/skills/statechart/scripts/test/differential.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/grid/Grid.cfg create mode 100644 plugins/pstack/skills/statechart/scripts/test/grid/Grid.tla create mode 100644 plugins/pstack/skills/statechart/scripts/test/grid/sany.out create mode 100755 plugins/pstack/skills/statechart/scripts/test/java.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/labels.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/messages.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/pipeline.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/plain-tlc.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/render.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/tlc-out.test.ts create mode 100644 plugins/pstack/skills/statechart/scripts/test/tlc.ts create mode 100644 plugins/pstack/skills/statechart/scripts/tsconfig.json create mode 100644 plugins/pstack/skills/statechart/scripts/worker.ts diff --git a/.gitignore b/.gitignore index b91c35f6..28c9a0b6 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,5 @@ plugins/pstack/skills/poteto-mode/scripts/node_modules/ .claude/skills/verify-open-pstack/node_modules/ + +plugins/pstack/skills/statechart/scripts/node_modules/ diff --git a/package.json b/package.json index 4560426a..89600043 100644 --- a/package.json +++ b/package.json @@ -3,8 +3,8 @@ "private": true, "packageManager": "bun@1.4.0", "scripts": { - "test": "cd plugins/pstack/skills/poteto-mode/scripts && bun install --frozen-lockfile && bun run test", - "typecheck": "cd plugins/pstack/skills/poteto-mode/scripts && bun install --frozen-lockfile && bun run typecheck", + "test": "cd plugins/pstack/skills/poteto-mode/scripts && bun install --frozen-lockfile && bun run test && cd ../../statechart/scripts && bun install --frozen-lockfile && bun run test", + "typecheck": "cd plugins/pstack/skills/poteto-mode/scripts && bun install --frozen-lockfile && bun run typecheck && cd ../../statechart/scripts && bun install --frozen-lockfile && bun run typecheck", "static": "bun -e 'for (const path of process.argv.slice(1)) JSON.parse(await Bun.file(path).text())' .claude-plugin/marketplace.json .agents/plugins/marketplace.json plugins/pstack/.claude-plugin/plugin.json plugins/pstack/.codex-plugin/plugin.json && PSTACK_STATIC_ONLY=1 bash tests/skill-collision-repro.sh" } } diff --git a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md index a950e12d..4b6c93e1 100644 --- a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md @@ -31,6 +31,8 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. +If the check is a TLA+ model, tell the next agent to read every result with the pstack [`statechart`](../statechart/SKILL.md) skill: read its `SKILL.md` and follow it, because it runs only when typed. It shows each invariant violation the checker finds as its shortest path in plain words. When the check passes, `statechart` draws a chart of how the system moves between states. Refer to `statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. + ## Prove it before you hand off Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change. diff --git a/plugins/pstack/skills/ketchup-video/SKILL.md b/plugins/pstack/skills/ketchup-video/SKILL.md new file mode 100644 index 00000000..c0c61428 --- /dev/null +++ b/plugins/pstack/skills/ketchup-video/SKILL.md @@ -0,0 +1,29 @@ +--- +name: ketchup-video +description: "Catch the user up like /ketchup, with a short subtitled video of slides for what happened and the waiting calls as text under it. Use for /ketchup-video." +disable-model-invocation: true +--- + +# Ketchup video + +Follow [`/ketchup`](../ketchup/SKILL.md), but show what happened in a short subtitled video instead of its summary and visuals. Its window starts at the last message the user wrote before `/ketchup-video`, not before any earlier `/ketchup`. Writing and rendering the video, outside the repo, is the one exception to its read-only rule. The reply is ketchup's opening sentence, the embedded video, one line naming any work left that you can do yourself, and the action items. When the video shows a call's options, call each option by the name the video gives it. If the render fails, say so in one line and give only the calls. + +## Slides + +Use the screenshots, recordings, diffs, and data the work produced, not the chat's prose about them. Before you draw, write the one sentence the user should leave with and one line per slide. Drop each slide that does not change what the user knows. Use at most 10 slides, and fewer is better. Neither note goes in the reply. + +Each slide makes one point. Build the slides on one picture and change it from slide to slide, rather than cut to an unrelated one. A color or shape means the same thing on every slide. Show the work in pictures, such as how a system works, a PR stack with each PR's state, a before and after of a fix, or options side by side. Point at what changed with arrows, highlights, and motion. A slide is never a bullet list, a status list, a table, or boxes with nothing connecting them. + +Keep text to the minimum. Put each label on the thing it names, in plain words a person would say, not tags like "Tests: pass". Never caption what a picture shows, and never give a fact twice, across slides or in the text under them. + +Show what came of each thing the user asked for, and whether it is done, still running, failed, or not checked. Never show something done that still waits on the user. Show any bug found and fixed on the way. If a visible change has no screenshot, say so on its slide and name what changed on screen. Draw only from facts you have. Never invent a number, and never draw a screen you did not capture. + +## Subtitles + +Give each slide one short subtitle line, about ten words, that says its point the way you would tell the user, from only what that slide shows. Say what the picture means rather than read out its labels. Put the subtitle in a strip below the slide, the same height on every slide and empty except for the subtitle, so it never covers the slide. Set it small, but readable when the video plays at chat size. + +## Render + +Render one silent landscape video, such as an mp4, with motion between slides. Every frame is the slide itself, edge to edge, above its subtitle strip. Make the frames from the slides, never by recording a screen, and burn each subtitle into its slide's frames so it stays on screen for the slide's whole hold. The hold is the time a slide is fully on screen, not counting the motion into or out of it. Hold each slide long enough to read the words it adds, at least one second for each three words. A slide adds its subtitle and each word that was not on the slide before it, including a label it changes. The first slide adds all its words. Words inside a screenshot do not count. + +Before you embed the video, check the rendered file. Look at one frame from each slide at chat size, and check that its subtitle is readable and covers nothing. Measure each hold by matching the file's frames to the slide, not with a still-frame detector, which counts the faint ends of a fade as still. Count the words each slide adds against its measured hold. Fix any slide you cannot read in that time, render again, and check again. diff --git a/plugins/pstack/skills/poteto-help/SKILL.md b/plugins/pstack/skills/poteto-help/SKILL.md index 63610b96..defaeca0 100644 --- a/plugins/pstack/skills/poteto-help/SKILL.md +++ b/plugins/pstack/skills/poteto-help/SKILL.md @@ -71,6 +71,7 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Understand a change or subsystem, explained plainly | [`/teach`](../teach/SKILL.md) | | Catch up on their own recent work on a topic | [`/recall`](../recall/SKILL.md) | | Catch up on what changed in this chat since their last message, in plain words and small visuals, with every item waiting on them listed and decidable from the reply alone | [`/ketchup`](../ketchup/SKILL.md) | +| Catch up like `/ketchup`, in a short subtitled video of slides, with the waiting calls as text under it | [`/ketchup-video`](../ketchup-video/SKILL.md) | | Know what a small diff could break outside itself | [`/blast-radius`](../blast-radius/SKILL.md) | | Settle types and module shape before code that crosses a function boundary | [`/architect`](../architect/SKILL.md) | | Get several attempts at one brief, merged into the best one | [`/arena`](../arena/SKILL.md) | @@ -86,6 +87,7 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | | Formally verify a race, invariant, or other property that tests rarely reach | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) | | Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | +| Show a PM or designer what the user sees as a chart checked by a TLA+ model, with the shortest path to each state that breaks a rule | [`/statechart`](../statechart/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/plugins/pstack/skills/statechart/SKILL.md b/plugins/pstack/skills/statechart/SKILL.md new file mode 100644 index 00000000..f5a64a8d --- /dev/null +++ b/plugins/pstack/skills/statechart/SKILL.md @@ -0,0 +1,82 @@ +--- +name: statechart +description: "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." +disable-model-invocation: true +--- + +# Statechart + +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 +/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR] +``` + +`scripts/statechart.ts` is TypeScript, so run it with a runtime that can execute TypeScript. + +The first run installs TLC and Java with mise and needs the network. + +## Write the spec + +- Write each rule that the reader agrees to as an INVARIANT. A rule can be about a screen, a result, a stored value, or a message. If the model has no variable for a rule, add the variable. Never weaken a rule to make it hold. +- Write `Next` as a disjunction of the actions, such as `YouPressPlay \/ YouPressStop`. If you do not, TLC names every step `Next`. +- A state with no step out breaks `NoDeadlock`, also when it is a correct end state. When an INVARIANT or a PROPERTY already has that name, the rule is `CHECK_DEADLOCK`. Add to `Next` an action that is true only in the end states and changes nothing, such as `Done == phase \in {"paid", "failed"} /\ UNCHANGED vars`, and give it a label in `step()`. + +## Pick the chart + +You do the work that needs judgment: the words on each state and arrow, the phases and their colors, the title, and the report to the reader. Put your work in a view module, and give it with `--view`. + +To show the reader's words, the view exports `state(vars)`. The value that `state()` returns picks the form: + +- A string gives a flat chart: `export const state = (v) => (v.paid ? "Paid" : "Paying");` +- An array gives parent states: `export const state = (v) => v.main.split(".");` +- An object gives one parallel region for each key: `export const state = (v) => ({ Playback: v.playback, Volume: v.volume });` + +Label each state with what the reader can see or cares about, such as "Paying" or "Lease held, write pending". Keep variable names out of labels. In `vars`, a TLA+ sequence is an object with keys from 1, so `v.pc[1]` is `pc[1]`. A set is an array. + +The view can also export `step(action, from, to)`. It gets the TLC action name and the values before and after the step, and it returns the label of the arrow. Write each step label as the user sees it happen, such as "you press play" or "the connect fails". Do not name the code or the TLA+ action. Two actions that end the same in the chart get the same label, so that they share one arrow. + +When a step can occur only in some conditions, end its label with the condition in brackets, in the reader's words, such as `you press play [while the file loads]`. In a regions chart, the command writes the condition on the other regions on the arrow, in the words of their labels, such as `[when Offline]`. Your brackets replace it, and two arrows from one state can then look the same. So in a regions chart, do not write brackets for a condition on another region. When a value that no label shows decides where a step goes, name the result in the label, such as "the roster read fails". + +The view can also export these: + +- `group(vars)` returns the name of a phase. Each chart state gets the color of its group. When the model states behind one chart state are in different groups, that state gets no color. +- `colors` gives each group name a color class. +- `title` is a string that the chart shows at the top. + +The command calls `state()` and `group()` at most once for each model state, and `step()` at most once for each step. The chart and the report both use those answers. So make each function depend only on its arguments. + +The chart does not draw a step that stays in one label. Split a label when the reader must see such a step. + +Aim for about 20 arrows or fewer, because a busier chart is hard to read. First return coarser labels from `state()`. Give one label to values that act the same, and leave out a detail that the reader does not need, such as a call in flight whose return changes nothing. Keep each state of a bug path, and keep each mark. When a merge changes a `breaks` state to `mayBreak`, it hides where a rule breaks. Do not merge two states that break different rules, because the reader then cannot see which rule breaks where. If the chart is still too busy, return `null` from `step()` for the steps that the reader does not need, such as a reset that every state has, or a step whose arrow repeats what other arrows show. Obey these rules when you hide steps: + +- Keep each chart state reachable by arrows from a start state. +- Keep at least one arrow out of each chart state that has a step out in the model. +- Hide all the steps of an arrow, or none of them. When you hide only some, its condition gets narrower. +- In the hand-off, say which steps the chart hides. + +## Read the report + +- In the chart, a state that breaks a rule has the class `breaks`. When only some model states behind it break the rule, it has the class `mayBreak`. The Legend names the rules of each mark. When two rules break, it names both on one mark, so say in the hand-off which state breaks which rule. In a regions chart, a state gets a mark when each combination of region states that includes it can break a rule. When a combination can break a rule and none of its states has a mark, each state in that combination gets a mark. +- TLC goes past a state that breaks a rule, so the chart shows the states after a bug. +- Because TLC goes past bugs, a model with no limit on its states can run without end. Keep the constants small, or add a CONSTRAINT. +- With a VIEW or a SYMMETRY, TLC counts states that it treats as the same as one state, and the chart draws that one state. An arrow can lead to it rather than to the state that the step reaches, and the report says so. +- TLC checks the rules in each state past a CONSTRAINT or an ACTION_CONSTRAINT, but it does not explore that state or check it for deadlock. When TLC's shortest path for a rule ends in such a state, the chart draws that state, and the report gives that path. The chart does not draw the other states past the bound. A deadlock in such a state does not show. TLC also checks the rules after each step that an ACTION_CONSTRAINT excludes, also when it reaches the next state another way. When TLC's shortest path for a rule ends with such a step, the chart draws that step. +- The command checks the rules with TLC on the config as written, with one worker. When a rule breaks, the command removes that rule and runs TLC again, until no rule breaks. After the first break, each run stops at 100,000 distinct states, so that a large model does not run without end. When a run reaches that bound or stops on an error, the report lists the rules that it did not check under "Rules not checked", and the chart does not mark them. A rule that is not checked can hold or break. To check it, remove the rules that break from the config, or make the model smaller. The bound adds a module that changes TLC's order of the variables, so for a property TLC can find a different counterexample than a run without the bound. +- `tlc.out` is what TLC printed on the config as written. When the chart does not show the bug path of a rule that breaks, `tlc-RULE.out` is what TLC printed for the run that found it. When TLC repeats its first warning, plain TLC prints it twice, but `tlc.out` shows it once, because TLC leaves the second copy out of the output that this command reads. That happens only when Java runs with `-XX:+UseParallelGC`, since otherwise TLC's first warning is its advice to pass that flag, which it prints once. + +## Show the chart + +Show `chart.mmd` to the user as a `mermaid` code block. The chart has a budget of 500 states, counted by TLC on the config as written. Above that, the chart draws only the paths to the rules that break, and when no rule breaks, the command writes no `chart.mmd`. It still checks each rule, and the report gives the state count and each bug path. To see the whole graph, make the model smaller. + +Render charts with Pele. When the user asks for an image, or a chart is too large to read as text, follow `references/render.md`. Do not use a different renderer unless the user asks for it. + +## Hand off + +Give each chart and its Mermaid text to the person who must decide. Add one line for each bug: the rule, the reader's sentence for that rule, and the path as the report numbers it. Say what the model leaves out. Give the command that makes the files again, with a new `--out` folder. + +When the model describes code, replay each bug path against the real code, as a test or a live repro, one step for each action. If a bug does not occur, think that the model is wrong until you show that it is not. diff --git a/plugins/pstack/skills/statechart/references/render.md b/plugins/pstack/skills/statechart/references/render.md new file mode 100644 index 00000000..5ef0519d --- /dev/null +++ b/plugins/pstack/skills/statechart/references/render.md @@ -0,0 +1,93 @@ +# Render a chart + +Render each `.mmd` file that you show with the npm package `pele@1.9.0`, and give the user the SVG. Install Pele once, outside the repo. Write each SVG next to its `.mmd` file, with the same name. The API is at https://pele.run/api. Pass `{ limit: 1_000_000, outputLimit: 8_000_000, maxEdges: 10_000 }` as the options of `render`. Pele's defaults are smaller than a chart of 500 states can be. When Pele throws a `PeleError`, show the user the Mermaid text and the error. + +## Colors + +Pele ignores Mermaid `theme` and `themeVariables`. Set its `--pele-*` CSS variables on `.pele`. https://pele.run/theming lists them. The command gives each state the color class of its group, such as `class sN teal`. It marks each bad state with `class sN breaks` or `class sN mayBreak`, each state on the shortest path to a bug with `class sN bugPath`, and each state that a PROPERTY counterexample repeats forever with `class sN repeats`. Pele puts these classes on the state's node. Color the classes with CSS. + +The `.mmd` file has a `classDef` line for `breaks` and for `mayBreak`, so that any Mermaid viewer shows the bug marks. It has no `classDef` for the group colors, `bugPath`, or `repeats`. Pele writes each `classDef` color as a `style` attribute on the node, and a `style` attribute wins over a normal CSS rule. So the rules for the marks below use `!important`. Without it, a dark theme keeps the light mark colors. A bug mark sets the fill and the text, and `bugPath` and `repeats` set the border. Put the mark rules after the group colors, so that a mark shows over the group color. + +These colors are suggestions. They are the colors of the old skill. Put them in a `