[poteto]

What it does

The new /statechart skill draws what a user sees as a Mermaid statechart. It builds the chart from the state graph that TLC explores for a TLA+ model. The chart and the checked model are one object, so they cannot drift apart.

The reader's rules become invariants. An example rule is "you never see Synced while you are offline." TLC checks each rule in its own run. Each path that breaks a rule appears on the chart as a numbered path in the reader's words. A PM, a designer, or a reviewer can judge the chart without reading TLA+.

Each state has one of three colors. Gray states work today. Red states are still wrong. Green states are fixed or new in an open PR.

The skill works in both directions.

• From a model to a chart. tlc-to-chart.mjs reads the TLC state graph, the counterexample traces, and a mapping module in the reader's words. It writes the chart, a story for each bug in reader steps, and a JSON summary of the counts. With --fixed-dot, it also shows what a fix changes.
• From a chart to a model. chart-to-tla.mjs writes a TLA+ skeleton, a TLC config, and a mapping module from an agreed chart. compare-charts.mjs compares the agreed chart with the chart that the model draws back.

Example

The skill uses an invented notes app as its example. The app has one rule. The sync badge never shows Synced while the app is offline. TLC finds one path that breaks the rule. The network drops while a note waits to sync. A late server confirmation then sets the badge to Synced.

The fix accepts a server confirmation only while the app is online. With the fix, the last state of the same path turns green. The blocked step shows as a loop.

Both charts come from the commands in SKILL.md, run on this branch with TLC.

Changes

• pstack/skills/statechart/ adds SKILL.md, a shared library, three scripts, and 21 unit tests with two example charts.
• harness/pstack/claude-code/ gets the generated copy of the skill and the docs.
• The pstack README, the verify-and-ship guide, and poteto-help list the new skill.
• The pstack version goes from 0.15.29 to 0.15.30 in the four plugin.json files.
• validate-plugins.yml now runs the skill script tests with node --test.

Review fixes

A deep review of the first commit found 14 defects. The second commit fixes all 14, and each fix has a unit test. 12 of the new or changed tests fail on the first commit. These are the main fixes.

• A TLC run that failed or did not complete is refused. It no longer reads as "no bugs."
• A rule that a start state breaks counts as a bug.
• A bug that only the fixed model has is drawn as wrong. Its story says "New with the fix."
• compare-charts.mjs compares the combined machine of all parallel regions. It now finds regions that stop moving together.
• Five Mermaid forms that were read wrong are now read correctly or refused.
• Quotes in reader labels no longer break the Mermaid output.

A fresh agent also followed the skill on two invented products. It found 14 points that were unclear or wrong. 13 are fixed in SKILL.md or in the scripts. The last point does not block.

The third commit fixes a Bugbot finding. A -- outside a composite state dropped every region after it without an error. The parser now refuses that chart. A new unit test covers the parser, chart-to-tla.mjs, and compare-charts.mjs. It fails on the second commit.

The fourth commit makes compare-charts.mjs exit 2 for a chart it cannot read, as SKILL.md says. Exit 1 now means only that the charts differ.

Verification

All checks ran on the branch head 3c5adb6.

• The skill tests pass 21 of 21 with TLC 1.7.4 and with a current TLC nightly build. Without TLC, 16 pass and 5 skip.
• The chart-to-model commands in SKILL.md run as written. TLC finds the one design bug in the example. compare-charts.mjs prints same and exits 0.
• validate-plugins.mjs passes. check-pstack-docs.mjs reports 0 problems.
• generate-pstack-harness-trees.mjs --check reports that the harness tree is up to date.
• The skill lint checks quick-validate and lint-skill-frontmatter pass with 0 problems.
• A scan for internal paths and names finds 0 hits in the patch, the skill tree, and this description.

The skill was also tried on a larger product model with 2,394 states. Three reader rules found six bug classes. Tests against the real code reproduce two of them.

  

[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.}