Repository navigation
pstack statechart: help and docs promise more than the scripts do #783
Description
Summary
Several user-facing statements in the statechart skill promise more than the scripts do. Each one below was checked by running the real CLI or helper. TLC output was scripted in these runs, so they test the wrapper's routing, chart writing, and output handling, not TLC itself.
All five statements are present on main at 9b93e81fb292.
1. Stories overstate route counts and path minimality
tlc-to-chart.mjs lines 1324 to 1326
c.count counts the counterexamples grouped into one bug, not the paths through the model. Given a valid DOT graph with both Start → Left → Broken and Start → Right → Broken and one completed counterexample, the story says "This is the only way to get here in the model." In a second graph, the shortest model trace to a bad state had three reader steps and a longer trace to the same state had one. The story reported the three-step path as the shortest.
Suggested wording: "This bug group contains one counterexample." and "This bug group contains N counterexamples. This has the fewest reader steps among them." The story assertions in scripts/test/statechart.test.mjs would change with it.
2. --expect-broken does not stop on any chart change
The help says the regenerate script "rebuilds every chart and stops on any change". Two runs with the same TLC results and the same expected broken rules, with a mapping label changed between them, both exited 0 while chart.mmd changed. The flag checks the broken-rule set. Suggested wording: "rebuilds every chart and checks the broken-rule set".
3. Output folder protection checks names, not provenance
statechart.mjs lines 102 to 104
The help says the command "does not use an output folder that has files that it did not write". foreign() compares entry names against OWN. An output folder holding only a hand-written chart.mmd was accepted, and the file was replaced with exit 0. The test titled "statechart.mjs does not use an output folder that has files that it did not write" makes the same promise. #773 reports a related case with nested entries.
4. tlc-to-chart.mjs write list omits two flags
The help says it "Writes only the files that --out, --story, and --summary name." With --regions --highlight 0 --out regions-chart.mmd --proof proof.mmd --regions-all all.mmd on a six-state graph, it wrote all three files. Suggested wording: "Writes only the files that --out, --story, --summary, --proof, and --regions-all name."
5. Charts draw invariant bugs only, but the docs say every bug
skills/statechart/SKILL.mddescriptionREADME.mdline 154docs/guide/06-verify-and-ship.mdlines 126 and 130
These say each bug TLC finds is drawn as a numbered path. With a broken temporal PROPERTY, the CLI reported the property broken and exited 1, but summary.json classes was empty and no bug-N.mmd was written. The CLI's own output says charts draw only INVARIANT rules. Suggested wording: "Invariant bugs are drawn as numbered paths."
Activity
deanrie commentedon Oct 25, 2026
Hey @creedants, a status pass over the five points against
mainafter #791 (the Pele renderer port rewrote most of the statechart scripts after you filed this), by reading the code, not by rerunning your scripts:c.count/ "only way to get here" wording is no longer intlc-to-chart.mjs. A story now opens withwaysLinefromways-in.mjs, which counts the distinct steps that lead into the broken state ("one step leads into this ...", "N different steps lead into this ...") and says nothing about path count or minimality. I have not run your two-path graph against it.--expect-broken"stops on any change": still true onmain.fromSpechandsfinishonlyrulesAsExpected(...), so the exit code is 0/1 from the rule set (2 when a PNG fails to render) and a chart that merely redraws exits 0. Thefrom-chartpath does also compare the chart (compare-charts.mjs, exit 1 when the spec does not draw it back), but the Regenerate example isfrom-spec. I changed that help line in fix(pstack): statechart refuses foreign files nested under tlc/ or behind an owned name #785 (02ba374) to "stops when a rule breaks or heals", since that PR already editsstatechart-help.mjs.tlc/.written.jsonrecord, nested and renamed foreign files refused).tlc-to-chart-args.mjs(--proof,--regions-allare parsed there). I did not find a replacement sentence that lists what the command writes, so the claim is gone rather than corrected.statechart.mjsnow checksPROPERTYrules separately (one TLC run per property, L312) and reports a broken one throughproperty-loop.mjsas a loop sentence (L424 to 447). Charts still mark broken states for invariants only (L293: "has no INVARIANT, so the chart marks no state broken"), so the "numbered path for each one" wording inSKILL.md,README.mdand06-verify-and-ship.mdis still wider than what gets drawn. That is a maintainer call on which side to move.So on
maintoday: 2 and 3 are addressed in #785, 1 and 4 are moot as written and may need a fresh look at the new scripts, 5 is unchanged in the docs.