Statechart 是一个 pstack 技能，用于以 Mermaid 状态图的形式，展示任意系统如何在状态之间迁移，例如产品流程、协议或服务。技能文档指出：以加粗、反引号或 /<name> 形式提及的技能，对应本技能目录旁的 ../<name>/SKILL.md；无前缀提及的原则对应 ../principle-<name>/SKILL.md，需读取并遵循。多数 pstack 技能仅供用户使用，技能工具无法加载。
用途 状态图用“读者”的语言描述系统迁移。读者决定行为是否正确，可能是阅读产品流程的产品经理、阅读协议或服务的工程师，或阅读设计的评审者。每个状态应标注读者可观察或关心的内容（如应用中的“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+ 模型，或代码/设计足够具体可建模时使用。若代码已有 TLA+ 规范，从该规范的副本开始，补充标签和规则所需变量，保留原有不变量；若要审计代码与规范的一致性，让副本建模代码实际行为，并将原规范作为 --against 传入，用作者声明的配置检查并作为 --against-config 传入（除非配置与规范文件同名）。两个模型共用一个映射，因此状态和步骤应基于两者都有的变量；只存在于副本的变量，标签须先测试 "name" in v。模型描述代码时，每个变量和动作要绑定评审者可打开的代码，并以代码命名；每个动作是代码中的一个不可分步骤；动作各条件的检查代码位置以注释形式写在条件上，如 * pay.ts:120。
- from-chart：没有模型、且行为的所有者应在构建或修改前先达成一致时使用。
规范到图 选择状态；当读者关心的内容会被标签掩盖时写入标签（如第二次扣费后屏幕仍显示“Paying”时标为“Paying, charged twice”）。从少量状态开始；当拆分能区分两个 bug，或读者必须看到不改变标签的步骤时再拆分。读者认可的每条规则写成一个不变量，以读者的话作为注释；规则可涉及屏幕显示、请求返回、存储值或部件间消息；模型没有对应变量时新增变量，不得丢弃规则。对一切稳定后适用的规则，定义 Settled == ~ENABLED System；对更窄时点适用的规则，写谓词并让规则在该处成立。对系统必须可达的目标，写“目标永不发生”的规则并用 --expect-broken 传入，破坏它的路径即为通往目标的路径；该目标在图中显示为违反规则的状态，并在 stories.md 中作为 bug 讲述，交接时需点名每个目标规则。其他违反规则均按 bug 报告，绝不削弱规则以让图通过。运行 from-spec 后填写生成的映射文件，在 state 和 step 中写标签；需要区分读者动作与周边事件时，在 readerActions 中按动作名列出读者动作，否则留空。概览过大时加 --cover，只保留到每个稳定状态的最短路径及所有 bug 路径，并列出省略内容。两个 bug 因不同原因终止于同一状态时，加 cause 命名各原因。要按读者关心内容给状态着色时，从 group 返回该分组；图例列出分组名，PNG 中违反规则的状态以红色替代分组颜色。若有拟议修复，将其建模并作为 --fixed 传入。用 --png 渲染每张图并逐张查看，确认编号路径按顺序可读；标签像代码时修正 state 或 step 后重跑。
模型描述代码时的验证 将每个 bug 的故事回放到真实代码上（测试或现场复现），每个模型动作对应一步；只驱动用户、客户端或系统其他部分可达的入口，只断言它们可观察的内容。断言自己设置的标志或搜索源码文本的测试不能证明任何东西。运行证明部分故事、读代码证明其余时，说明各自证明的部分；测试复制无法导入的代码时，给出副本的提交和行范围，并列出副本省略的内容。bug 不复现时，应先假定模型有误，修正模型而非规则。尚无代码的设计以 TLC 轨迹为证据，交接时必须说明。
图到规范 画出读者认可的状态图，为每个独立变化的部分（如设备连接与设备运行的任务）使用一个区域；每条规则加一行 %% never，附读者的话；停止或重启某部分的事件（如“应用关闭”“进程重启”）画为指向下一状态的边。运行 render CHART.mmd 得到供读者查看的 PNG。运行 from-chart；规则被破坏说明认可的设计有 bug，应交给认可该图的人。把真实代码的守卫和变量加入 from-chart 生成的规范并再次运行；对其打印的每处差异，询问读者是代码有误还是图需修正。
交接 把每张图的 PNG 和 Mermaid 源交给决策者；每个 bug 一行，注明违反的规则、图中编号步骤、是否复现、拟议修复是否有效。被破坏的 PROPERTY 在图上没有路径，应给出 stories.md 命名的 TLC 反例。使用 --against 时，还要说明规范是否已列出该问题（stories.md 命名的配置中、规范关于模型省略内容的说明中，或完全未列出）。模型描述代码时，命令列出没有文件和行号的条件期间，不得报告规则成立。引用的所有计数取自 summary.json。附上 stories.md 和重新生成全部内容的命令，并说明模型省略了什么。
限制 文档未提供关于收费、价格、支持平台的具体信息；首次运行需联网下载约 305 MB 并安装 TLC 和 Java；多数 pstack 技能仅限用户使用，技能工具无法加载；输出需在仓库外临时文件夹中生成。