[poteto]

Why

The statechart skill has six fixes since the version in pstack. Before them, a run can give a wrong chart or a wrong exit code and not say so: a second model with different variables, a crash in TLC, or a rule that the config lists as both INVARIANT and PROPERTY. A failed publish can lose the run's work. A PROPERTY line stays in every TLC run, so a broken PROPERTY is reported as a break of an INVARIANT that holds, and --expect-broken does not accept a PROPERTY. This change brings the skill up to its current version.

What changed

Each commit is one fix, in the order in which the fixes landed:

1. test(pstack): accept Naturals.tla anywhere under the run's temp folder. TLC 1.8.0 writes the standard modules one folder deeper inside the run's temp folder. The test accepts any path under that folder. This is the one failure that feat(pstack): add the statechart skill to draw TLA+ models as charts #741 found with a TLC nightly build.
2. fix(pstack): stop three silent wrong outputs in statechart
   • The command stops when the label map reads a variable or field that the --fixed or --against model does not have. Before, it gave that variable the current model's start value.
   • New options --config, --fixed-config, and --against-config. The agreed spec is never checked with the code model's config. When a config does not exist, the error lists the configs beside the spec.
   • When the agreed config does not check a rule, the stories mark the rule "not checked". Before, they said that the agreed spec keeps it.
3. fix(pstack): keep statechart work when TLC or publishing fails
   • When TLC finds a broken rule and then throws a Java exception while it reports it, the command keeps the paths that TLC printed, marks the rule broken, and warns that the charts can miss states.
   • When the file system cannot rename into the output folder (ENOSYS, EXDEV, or EISDIR, as on FUSE mounts), the command copies the files into place.
   • The command writes the label map scaffold before TLC runs, and checks the inputs again before --png renders.
4. feat(pstack): check every rule with all CPUs, and check PROPERTY rules in statechart
   • TLC checks each rule with one worker per CPU. When a rule is broken, TLC checks it again with one worker, which gives the shortest bug paths, the same on every run. The command prints how many times TLC ran and how long that took.
   • Each PROPERTY gets its own TLC run, and --expect-broken accepts it. The charts draw only INVARIANT rules, so a broken PROPERTY names TLC's counterexample file.
5. feat(pstack): say whether the agreed spec lists each bug, and flag uncited conditions in statechart
   • With --against, each story says whether a config beside the agreed spec expects TLC to break the bug's rule, from the config's \* expect: and \* module: lines. summary.json records this.
   • With --fixed or --against, the command lists each condition of an action that has no \* file:line comment, when a rule holds. A rule can hold only because the model waits for a condition that the code does not check.
   • SKILL.md asks for those citations, defines a valid replay, and asks the hand-off to say whether the spec already lists each bug.
6. fix(pstack): report the bug when a config lists one rule as both INVARIANT and PROPERTY
   • That rule gets one TLC run, as an INVARIANT.
   • The command reads each form of a broken PROPERTY that TLC prints: invariant, action property, property of the initial state, and temporal property.
   • The test that kills a run no longer fails when the process has already stopped.

Adapted or left out

• The scripts find TLC only through TLA2TOOLS and JAVA, as in feat(pstack): add the statechart skill to draw TLA+ models as charts #741. The source of item 4 also installs a repo-pinned TLC on demand, with tests for that. This repo pins no TLC version, so that part is not in this change. The help text and the "no TLC" message stay as in feat(pstack): add the statechart skill to draw TLA+ models as charts #741.
• A code comment that names another repo's checks now says "lines of each config".
• Every other line matches the current skill.

Blast radius

Only pstack/skills/statechart/ and its generated copy in harness/pstack/claude-code/skills/statechart/ change. Nothing outside the skill imports its scripts. The pstack version stays at 0.15.30. A separate PR bumps it.

Verification

• With TLC 1.7.4, all 67 skill tests pass and none skip. Without TLC, as in CI, 29 pass and 38 skip.
• Each commit passes the skill tests with TLC 1.7.4 and without TLC, and passes generate-pstack-harness-trees.mjs --check.
• With the TLC 1.8.0 prerelease, 66 of 67 pass. TLC 1.8.0 words a broken temporal property as "Temporal property X was violated." in place of "Temporal properties were violated.", and the scripts know only the 1.7.4 words. The current source of the skill has the same gap, so this change keeps it. The latest stable TLA+ release, which the "no TLC" message points to, is 1.7.4.
• With INVARIANT PaidMeansCharged and PROPERTY ChargedAtMostOnce on the payment model below, the current skill says "PaidMeansCharged is broken". With this change, it says that PaidMeansCharged holds and ChargedAtMostOnce is broken, and it names the counterexample file.
• validate-plugins.mjs, check-pstack-docs.mjs, and generate-pstack-harness-trees.mjs --check pass. A scan for internal paths, names, and model ids finds 0 hits in the patch.
• An end-to-end run on a small payment model, with the output folder on a FUSE mount: the code model retries a charge, and the agreed spec forbids that. from-spec PayCode.tla --against Pay.tla --against-config PayChecked.cfg --expect-broken NoDoubleCharge,ChargedAtMostOnce first writes the mapping scaffold and exits 2. After the labels are filled in, it exits 0. It finds the double charge, checks NoDoubleCharge once although the config lists it as both INVARIANT and PROPERTY, and says that PayRetry.cfg beside the agreed spec expects this bug. It also flags the one condition that has no code citation, and publishes the folder by copy.

  

[cursor]

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

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

[cursor]

PROPERTY-only rules marked unchecked

Medium Severity · Logic Bug

--against-rules and warnUnchecked look only at INVARIANT results. A rule the agreed spec actually checks as a PROPERTY is still treated as unchecked, so stories say the spec does not check it even though this run already printed that it holds or is broken.

Additional Locations (2)

• pstack/skills/statechart/scripts/statechart.mjs#L829-L836
• pstack/skills/statechart/scripts/tlc-to-chart.mjs#L517-L520

 

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