statechart

状态图

此图展示系统如何在不同状态之间转换，采用的是阅读者的表述。脚本将此人称为阅读者，例如 readerActions 和阅读者步骤中的用法。行为是否正确由阅读者决定。阅读者可以是阅读产品流程的 PM、阅读协议或服务的工程师，也可以是阅读设计的审阅者。每个状态都用阅读者能够观察到或在意的内容来标注，例如应用中的“正在付款”，或锁服务中的“已持有租约，写入待处理”。每个步骤都用推动系统转换的事件来标注，例如应用中的“点击付款”、服务中的“请求读取计数”，或锁服务中的“租约到期”。标签中不要使用变量名和动作名。

运行 node <skill dir>/scripts/statechart.mjs --help，查看命令以及如何阅读图表。请在仓库外的临时文件夹中操作。该命令会将文件写在输入文件旁边。首次运行时，会通过 mise 安装 TLC 和 Java，需要下载约 305 MB 数据并连接网络。帮助中的 TLC 部分介绍了如何使用已有的 TLC 和 Java。

选择方向

当存在 TLA+ 模型，或代码或设计具体到足以建模时，使用 from-spec。没有模型，且负责该行为的人员应在任何人构建或修改行为之前就该行为达成一致时，使用 from-chart。

如果代码已有 TLA+ 规范，请从该规范的副本开始。添加标签和规则所需的变量，并保留规范已有的不变式。若要依据该规范审查代码，请让副本描述代码的实际行为，并将未经修改的规范作为 --against 传入。使用其作者声明可通过的配置进行检查；除非该配置的文件名与规范相同，否则将其作为 --against-config 传入。一份映射同时标注两个模型，因此状态和步骤应根据两个模型共有的变量来标注。如果标签读取的变量仅存在于副本中，必须先检查 "name" in v，并以其他方式标注规范的状态。如果模型描述的是代码，每个变量和动作都要关联到审阅者可以打开的代码，并沿用代码中的名称。代码中的每个动作都应是一个不可再分的步骤。将检查动作各项条件的代码文件和行号写在对应条件的注释中，例如 \* pay.ts:120。

从规范生成图表

1. 选择图表中的状态。当读者关心某件事，而标签会掩盖它时，就把它写进标签，例如第二次扣款后屏幕仍显示“正在付款”，这时应标为“正在付款，扣款两次”。从少量状态开始。如果拆分状态能区分两个 bug，或者读者必须看到一个不会改变标签的步骤（例如读取计数的请求），就拆分状态，因为图表不会绘制这类步骤。
2. 将读者认同的每条规则写成一个不变量，并用读者的原话作为注释。规则可以针对模型中的任何状态：屏幕显示的内容、请求返回的内容、存储的值，或各部分之间传递的消息。如果模型描述的是代码，规则还要指出能够更改该状态的代码。如果模型中没有表示规则所针对内容的变量，就添加该变量。不要删除规则。对于一切稳定下来后适用的规则，定义 Settled == ~ENABLED System，其中 System 是所有不需要读者参与的动作的析取。对于在更具体时点适用的规则，例如每次请求完成后，编写该时点的谓词，并让规则在该谓词为真时成立。对于系统必须能够到达的目标，编写一条说明该目标永远不会发生的规则，并使用 --expect-broken 运行。破坏该规则的路径就是通往目标的路径。图表仍会将该目标绘制为违反规则的状态，而 stories.md 会将其描述为 bug，因此要在交接文档中注明每条目标规则的名称。将其他所有被破坏的规则都报告为 bug。绝不要为了让图表通过而弱化规则。
3. 运行 from-spec，然后填写它生成的映射文件。将标签放入 state 和 step。当图表必须区分读者执行的操作与读者周围发生的事情时，按动作名称将读者的操作列入 readerActions。如果所有动作都同等处理，则将列表留空。当概览太大而难以阅读时，添加 --cover。这样概览只会保留到达每个稳定状态的最短路径，以及每条 bug 路径；命令还会列出省略的内容。如果两个 bug 因不同原因结束于同一状态，则添加 cause，并让它标明每个原因。若要按读者关心的内容为状态着色，例如“订单已发货”，则从 group 返回该组。图例会列出各组名称；在 PNG 中，违反规则的状态会显示为红色，而不是其所属组的颜色。
4. 如果有拟议的修复方案，就对其建模，并将该模型作为 --fixed 传入。
5. 使用 --png 渲染每张图表，并查看每个 PNG。检查每条编号路径是否按顺序可读。如果标签看起来像代码，就修正 state 或 step，然后重新运行命令。
6. 如果模型描述的是代码，就针对真实代码重放每个 bug 的故事：通过测试或实时复现，按模型中的每个动作逐步执行。只驱动用户、客户端或系统其他部分能够触及的入口点，并且只断言它们能够观察到的内容。断言自己设置的标志，或搜索源文本，都不能证明任何问题。如果运行结果证明了故事的一部分，而阅读代码证明了其余部分，就说明各自证明了哪些部分。如果测试复制了无法导入的代码，就提供该副本对应的提交和行范围，并列出副本遗漏的内容。如果 bug 无法复现，除非另有证明，否则应假定模型有误。修正模型，而不是规则。对于尚无代码的设计，TLC 跟踪记录就是证据，交接文档必须明确说明这一点。

图表转规范

1. 绘制读者认可的图表。为每个独立变化的部分分别使用一个区域，例如设备的连接状态和设备运行的任务。每条规则添加一行 %% never，并写上读者的原话。将停止或重新启动某个部分的事件（例如“应用关闭”或“进程重新启动”）绘制为指向后续状态的边。运行 render CHART.mmd，生成图表的 PNG 文件供读者查看。
2. 运行 from-chart。如果违反了规则，说明达成一致的图表存在设计缺陷。将问题提交给同意该图表的人。
3. 将真实代码中的守卫条件和变量添加到 from-chart 写出的规范中，然后再次运行 from-chart。对于它打印出的每一处差异，询问读者是代码有误，还是图表需要修正。

移交

将每个图表的 PNG 文件和 Mermaid 源文件交给负责决策的人。每个问题写一行，列出违反的规则、图表编号的步骤、是否复现，以及建议的修复是否解决了问题。违反的 PROPERTY 在图表上没有路径，因此请提供 stories.md 中列出的 TLC 反例。使用 --against 时，还要说明规范是否已列出该问题：列在 stories.md 指定的配置中、列在规范关于模型未涵盖内容的注释中，或完全未列出。当模型描述代码时，如果命令列出了没有文件和行号的条件，就不要声称某条规则成立。引用的所有计数都取自 summary.json。附上 stories.md 以及重新生成所有内容的命令。说明模型未涵盖的内容。