[Jrecos]

Why

/statechart should draw a checked chart, or tell you what setup it needs. On a machine with no mise and no TLA2TOOLS, the command fails with spawn mise ENOENT. The skill never said that mise had to be installed, so agents searched the disk and downloaded a 209 MB Java runtime that nobody asked for.

What changed

• The skill's Run section says the default path needs mise on PATH. It says when an unset JAVA falls back to java on PATH.
• Before writing a model, the agent checks for TLA2TOOLS or mise. If neither is there, it stops and names the two setups. It does not search or download.

Scope

• Prose only. The compiler, the tests, and the dependencies don't change.
• This does not install Java or mise, and it does not remove the skill.

Blast Radius

Only /statechart runs change, and only when no toolchain is set up. Runs with a toolchain behave as before.

Verification

• Headless OMP, no toolchain, same prompt on both arms. The base skill ran find across /tmp, /opt, and /home, then reused a downloaded JRE. The fixed skill ran command -v mise, stopped, and wrote no files.
• Headless OMP with TLA2TOOLS and JAVA set. The fixed skill went from model to TLC to a Pele SVG with no search and no download.
• bun run check:content passes. Two independent read-only reviews checked the changed claims against run.ts, and all ten are confirmed.
• Docs: skills/statechart/SKILL.md changed. The README and docs/guide/06-verify-and-ship.md stay as they are. They describe what /statechart reports and link to SKILL.md, which owns setup.

[Jrecos]

Closed in favor of restoring the upstream statechart skill byte for byte. This PR added a local adaptation, and the skill should match P Stack 0.15.36.