Statechart 是一个面向 Pstack 任务的技能，用于把系统如何在状态之间迁移画成 Mermaid 状态图，并用 TLA+ 模型进行检查。它适用于产品流程、协议或服务等需要向读者说明行为的场景。
主要能力与使用方式：
- 用读者能观察或关心的内容标注状态，例如应用中的“Paying”，或锁服务中的“Lease held, write pending”；用推动系统迁移的事件标注步骤，例如“tap Pay”“the request reads the count”或“the lease expires”。标签中不出现变量名和动作名。
- 通过 node <skill dir>/scripts/statechart.mjs --help 查看命令与读图说明。命令把输出写在输入文件旁边，建议在仓库外的临时文件夹中工作。首次运行会用 mise 安装 TLC 和 Java，约下载 305 MB，需要网络；帮助文档的 TLC 部分说明如何使用已有的 TLC 和 Java。
- 两种方向：from-spec 用于已有 TLA+ 模型，或代码、设计足够具体可建模的情况；from-chart 用于没有模型、需要行为负责人先就图表达成一致的情况。
- 从规格生成图表时，需填写映射文件中的 state 和 step，可通过 readerActions 区分读者动作与环境动作，用 --cover 精简过大的总览，用 cause 区分同一状态的不同 bug 原因，用 group 按读者关心的事项着色。
- 从图表生成规格时，用 %% never 行表达每条规则，用独立 region 表示独立变化的部分，先渲染 CHART.mmd 得到 PNG，再运行 from-chart；若规则被破坏，则说明已达成一致的图表存在设计缺陷。
- 支持用 --png 渲染并逐张检查；当模型描述代码时，应把每个 bug 的故事回放到真实代码上作为测试或现场复现，只驱动用户、客户端或系统其他部分可达的入口，只断言可观察的内容。
- 交付时提供图表 PNG 与 Mermaid 源码，每个 bug 一行说明所破坏的规则、步骤编号、是否复现、提议修复是否有效，并附上 stories.md 和重新生成全部内容的命令，说明模型省略了什么。
适用场景：产品流程评审、协议或服务行为审查、设计评审、代码与规格一致性审计，以及尚无代码时先就行为达成一致的讨论。
限制：首次运行需要联网下载约 305 MB 的 TLC 和 Java；不得为了让图表通过而削弱规则；无法复现的 bug 应先假设模型有误；尚无代码的设计以 TLC 轨迹为证据。其他功能、收费、价格与支持平台暂未提供。