一句话

把「用户看到的行为」画成从 TLA+ 模型生成的 Mermaid 状态图：每个 bug 是一条编了号、通向违规状态的路径，用读者的话命名状态和步骤。

何时用

• 适合：给 PM、设计师、评审看行为而不是读 spec；把达成一致的图转成 TLA+ 骨架；拿已有 spec 审计代码。
• 不适合：只要文字结论不要图；没有状态可讲的纯函数。

怎么用

/statechart 用户离线编辑笔记时看到什么

1. 选方向：有模型或代码够具体走 from-spec；没有模型、要先和人达成一致走 from-chart；有现成 spec 则用 --against 审计代码。
2. from-spec：挑状态、把读者认可的每条规则写成 invariant（读者原话当注释）、跑命令后填 mapping 的 state/step/readerActions；有修复方案就传 --fixed。
3. 每条 bug 路径在真实代码里逐动作回放（测试或现场复现）后才上报；复现不了先怀疑模型。
4. from-chart：画好大家都认可的图、%% never 行写规则、跑 from-chart 生成骨架，再把真实代码的守卫补回去看分歧。
5. 移交：PNG 加 Mermaid 源加每条 bug 一行（违反的规则、编号路径、是否复现、修复是否生效），数字以 summary.json 为准，附 stories.md 和可重跑命令。

产出

• 状态图 PNG 与 .mmd 源、bug 路径清单、（审计模式）代码与 spec 的差异；全部在仓库外 scratch 目录生成。

要点与坑

• 标签用读者语言不写变量名；规则不许为让图变绿而削弱。
• 首次运行用 mise 装 TLC 和 Java，下载约 305 MB，需要网络；命令细节跑 node <skill dir>/scripts/statechart.mjs --help。
• 是 pstack-create-formal-verification-skill 推荐的 TLA+ 结果阅读器。

关联

• 配套：pstack-create-formal-verification-skill、pstack-maintain-formal-verification-skill
• 所属：00-pstack-概览