用途
pstack-statechart 用于在 Pstack 任务中展示系统如何在状态间迁移，例如产品流程、协议或服务。图表用“读者”能理解的语言表达：读者可以是阅读产品流程的产品经理、阅读协议或服务的工程师，或阅读设计的评审者。读者决定行为是否正确。
主要能力
- 生成 Mermaid 状态图，并用 TLA+ 模型配合 TLC 检查图表与规则。
- 两种方向：
- from-spec：已有 TLA+ 模型，或代码/设计足够具体可建模时使用。
- from-chart：没有模型、需要行为负责人先就图表达成一致时使用。
- 将读者认可的规则写成不变式，并在模型中检查；支持针对稳定状态（Settled == ~ENABLED System）或特定时点的规则。
- 对系统必须能达到的目标，写成“目标永不发生”的规则并配合 --expect-broken，破坏路径即为达到目标的路径。
- 支持 --cover 精简过大的总览，只保留每个稳定状态的最短路径和所有缺陷路径；支持用 cause 区分同一状态的不同原因；用 group 按读者关心的分组着色。
- 可用 --fixed 对提议的修复建模验证。
- 输出 PNG、Mermaid 源文件、stories.md 与 summary.json，便于交付和复现。
使用方式
- 在仓库外的临时目录工作。命令会把文件写在输入文件旁边。
- 运行 node <skill dir>/scripts/statechart.mjs --help 查看命令和读图方式。
- 首次运行会通过 mise 安装 TLC 和 Java，约下载 305 MB，需要网络；帮助中的 TLC 部分说明如何使用已有的 TLC 和 Java。
- 选择 from-spec 或 from-chart 方向，填写映射文件（state、step、readerActions、cause、group 等）。
- 用 --png 渲染每张图并逐张检查编号路径顺序；若标签像代码，修正 state 或 step 后重跑。
- 对描述代码的模型，将每个缺陷故事按模型动作逐步对真实代码回放（测试或现场复现），只驱动用户、客户端或系统其他部分可达的入口，只断言可观察内容。
- 交付时提供每张图的 PNG 与 Mermaid 源文件，每个缺陷一行说明（违反的规则、按图表编号的步骤、是否复现、提议修复是否有效），并附 stories.md 与重新生成全部产物的命令。
适用场景
- 产品流程评审，如支付流程中的“Paying”状态。
- 协议或服务行为说明，如锁服务中的租约与写请求。
- 设计评审，在实现前就行为达成一致。
- 审计代码是否符合已有 TLA+ 规格。
限制
- 首次运行需要联网下载约 305 MB（TLC 与 Java）。
- 图表不绘制“标签保持不变”的步骤，必要时需拆分状态。
- 对无代码的设计，TLC 轨迹是唯一证据，交付时需说明。
- 若缺陷未能复现，应假定模型有误并修正模型，而不是弱化规则。
- 当命令列出缺少文件与行号的条件时，不得报告规则成立。