[poteto]

Why

A TLA+ model is hard to review for anyone who does not read TLA+. The new /statechart skill draws the states that an app's user sees as a Mermaid statechart, built from the state graph that TLC explores. The chart and the checked model are one object, so a PM or a designer can judge the design from the chart.

What changed

• pstack/skills/statechart/ adds the skill, a shared library, four scripts, and 58 unit tests. statechart.mjs from-spec checks each rule and draws the charts. --fixed shows what a fix changes, and --against audits code against an existing spec. from-chart writes a TLA+ skeleton from a chart that the PM agreed to.
• scripts/model/OutputFolder.tla, with its .cfg and mapping, models two runs that share one output folder. A test draws its chart and checks that its five rules hold. Five mutants each remove one guard from the model, and the test checks that each mutant breaks the rule that its guard protects.
• The pstack README, the verify-and-ship guide, and poteto-help list the skill. The harness tree gets its generated copy, and the pstack version goes from 0.15.29 to 0.15.30.
• validate-plugins.yml runs the skill tests with node --test.

Scope

• The scripts find TLC only through TLA2TOOLS and JAVA. Without TLA2TOOLS, they say where to download tla2tools.jar and exit 2.
• Each run works in its own temporary folder and replaces the output folder with one rename at the end. A refused run, or a run whose spec changed while TLC read it, leaves the output folder as it was.
• A run does not overwrite or delete a file that it did not write. It exits 2 and names the file instead.
• Runs that overlap on one folder all finish, and the last one to finish owns the folder. A rerun replaces the whole folder, so an old chart.png does not stay behind.
• CI has no TLC, so the 31 tests that need it skip there. Two of them also need a C compiler, and one of those also needs unprivileged unshare. Each skips when its tool is missing.

Blast Radius

The skill is new, and nothing outside it imports its scripts. The CI change adds one node --test step.

Verification

• With TLC 1.7.4, all 58 skill tests pass and none skip. Without TLC, 27 pass and 31 skip. The harness copy is byte for byte the same as the skill folder.
• With a TLC nightly build, 57 of 58 pass. The one failure is a test that expects Naturals.tla directly in the run's own TLC temp folder. The nightly writes it one folder deeper, still inside that temp folder. The scripts work, and only the test's path check is too strict.
• validate-plugins.mjs, check-pstack-docs.mjs, generate-pstack-harness-trees.mjs --check, quick-validate, and lint-skill-frontmatter pass.
• A scan for internal paths, names, and model ids finds 0 hits in the patch and in this description.

The charts below come from the test chart, an invented notes app with one rule. The badge never shows Synced while the app is offline. statechart.mjs from-chart notes-app.mmd --expect-broken NeverSyncedWhileOffline --title "Notes app sync" --png finds the one path that breaks the rule and draws both charts. These scripts write the same chart.mmd and bug-1.mmd that the images show.

  

[cursor]

Cursor Bugbot has reviewed your changes using high effort and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit f149a2d. Configure here.}