用途
Statechart 技能用于将 TLA+ 模型转化为面向产品经理（PM）的 Mermaid 状态图，展示应用用户所见的行为。产品经理可据此判断行为是否正确。状态标签描述屏幕内容（如“Paying”），步骤标签描述用户操作或可见事件（如“tap Pay”或“the charge goes through”），避免使用变量名和动作名。脚本将产品经理称为 reader。
主要能力
- 从 TLA+ 规范生成状态图（from-spec）：当存在 TLA+ 模型或代码足够具体可建模时使用。可基于现有规范副本，添加用户可见的变量，保留原有不变量。
- 从图表生成 TLA+ 规范（from-chart）：当没有模型且产品经理应在编码前就行为达成一致时使用。
- 支持设计缺陷审查：通过不变量（invariant）表达产品经理同意的规则，以注释形式保留产品经理的原句。违反规则即报告为缺陷，不得弱化规则使图表通过。
- 状态着色：根据产品经理关注的分组（如“Toast shown”）着色，违反规则的状态仍带红色边框。图例命名分组。
- 缺陷复现：每个缺陷需以测试或实时复现方式针对真实代码重放，每个模型动作对应一步。若缺陷未复现，默认模型有误，应修正模型而非规则。
- 支持开放修复：若有未完成的修复，从代码建模并通过 --fixed 传入。
- 输出文件：生成 Mermaid 源文件、PNG 图片、mapping 文件、summary.json、stories.md 及重新生成命令。
使用方式
- 在仓库外的临时文件夹中工作。命令会将文件写在输入文件旁边。
- 运行
node <skill dir>/scripts/statechart.mjs --help查看命令和图表阅读方法。 - 选择方向：存在 TLA+ 模型或代码足够具体时用 from-spec；否则用 from-chart。
- 从规范生成图表时：选择状态（从少量开始，仅在拆分能区分两个缺陷时拆分）；将每条产品经理同意的规则写为一个不变量，以产品经理的句子作为注释；定义 Settled == ~ENABLED System，其中 System 是用户不执行的动作的析取。
- 运行 from-spec，填写生成的映射文件：在 state 和 step 中放置标签，在 readerActions 中按动作名列出用户动作。若两个缺陷通过不同代码路径到达同一屏幕，添加 cause 命名代码路径。若要按产品经理关注点着色，从 group 返回该分组。
- 用 --png 渲染每个图表并查看所有 PNG，检查每条编号路径按顺序阅读。若标签读起来像代码，修正 state 或 step 后重新运行命令。
- 从图表生成规范时：绘制产品经理同意的图表，每个独立变化的事物（如连接和同步徽章）使用一个区域。每条规则添加一行
%% never行，附产品经理的句子。将“应用关闭”绘制为指向用户所见下一状态的边。 - 运行 from-chart。若规则被破坏，同意的图表存在设计缺陷，需反馈给产品经理。将真实代码的守卫和变量添加到 from-chart 写出的规范中，再次运行 from-chart。对每个打印的差异，询问产品经理是代码错误还是图表需要修正。
- 交付：向产品经理提供每个图表的 PNG 和 Mermaid 源文件；每个缺陷一行，包含违反的规则、图表编号步骤、是否复现、开放修复是否修复它。所有引用计数取自 summary.json。附上 stories.md 和重新生成一切的命令。说明模型省略了什么。
适用场景
- 产品经理需要审查应用用户可见行为是否正确。
- 已有 TLA+ 规范，需生成面向非技术读者的状态图。
- 无模型时，需产品经理先就行为达成一致再编码或修改代码。
- 需要审计代码是否符合规范，或跟踪缺陷修复状态。
限制
- 需要 TLA+ 建模基础或配合建模人员。
- 脚本应在仓库外的临时文件夹运行，文件写在输入文件旁。
- 模型可能省略某些细节，交付时需明确说明。
- 若缺陷未在真实代码中复现，默认模型有误，需修正模型。
- 不提供收费、平台或效果保证信息。