statechart

状态图

该图展示系统如何在各状态之间转换，描述方式由阅读者决定。阅读者会判断行为是否正确。

运行

在仓库之外的临时文件夹中操作。编写 TLA+ 规范及其配置文件，然后运行：

<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR]

scripts/statechart.ts 是 TypeScript 文件，因此请使用能够运行 TypeScript 的运行时来执行它。

首次运行时，mise 会安装 TLC 和 Java，需要联网。

编写规范

• 将阅读者认可的每条规则写成 INVARIANT。规则可以涉及屏幕、结果、存储的值或消息。如果模型中没有用于表示某条规则的变量，就添加该变量。绝不要为了让规则成立而弱化它。
• 将 Next 写成各个动作的析取，例如 YouPressPlay \/ YouPressStop。否则，TLC 会将每一步都命名为 Next。
• 没有后续步骤的状态会导致 NoDeadlock 失败，即使它是正确的结束状态也是如此。当 INVARIANT 或 PROPERTY 已使用该名称时，该规则为 CHECK_DEADLOCK。向 Next 添加一个仅在结束状态下为真且不做任何更改的动作，例如 Done == phase \in {"paid", "failed"} /\ UNCHANGED vars，并在 step() 中为它指定标签。

选择图表

需要判断的部分由你来完成：每个状态和箭头上的文字、阶段及其颜色、标题，以及给读者看的报告。将你的实现放在一个视图模块中，并通过 --view 指定。

若要显示读者看到的文字，视图会导出 state(vars)。state() 返回的值决定图表的形式：

• 返回字符串会生成平面图表：export const state = (v) => (v.paid ? "Paid" : "Paying");
• 返回数组会生成父状态：export const state = (v) => v.main.split(".");
• 返回对象会为每个键生成一个并行区域：export const state = (v) => ({ Playback: v.playback, Volume: v.volume });

用读者能看到或关心的内容为每个状态命名，例如“正在付款”或“租约已持有，等待写入”。不要在标签中使用变量名。在 vars 中，TLA+ 序列是一个键从 1 开始的对象，因此 v.pc[1] 对应 pc[1]。集合是数组。

视图还可以导出 step(action, from, to)。它会接收 TLC 操作名称以及步骤前后的值，并返回箭头标签。每个步骤标签都应描述用户看到的情况，例如“你按下播放”或“连接失败”。不要提及代码或 TLA+ 操作。图表中最终到达相同状态的两个操作应使用相同标签，这样它们就会共用一条箭头。

当步骤只能在某些条件下发生时，在标签末尾用方括号注明条件，并采用读者能理解的说法，例如 你按下播放 [文件加载期间]。对于区域图表，命令会在箭头上写出其他区域的条件，并使用这些区域标签中的文字，例如 [当处于离线状态时]。你写的方括号会替换该条件，因此从同一状态出发的两条箭头可能看起来相同。所以在区域图表中，不要为其他区域的条件写方括号。当某个未显示在任何标签中的值决定步骤的去向时，要在标签中说明结果，例如“读取成员名单失败”。

视图还可以导出以下内容：

• group(vars) 返回阶段名称。每个图表状态都会采用所属组的颜色。如果同一个图表状态背后的模型状态属于不同的组，该状态就不会着色。
• colors 为每个组名指定一个颜色类。
• title 是图表顶部显示的字符串。

对于每个模型状态，命令最多调用一次 state() 和 group()；对于每个步骤，最多调用一次 step()。图表和报告都会使用这些结果。因此，每个函数都应只依赖其参数。

对于标签不变的步骤，图表不会绘制箭头。如果读者需要看到这样的步骤，就拆分相应标签。

尽量将箭头数量控制在 20 条以内，因为太繁杂的图表难以阅读。首先让 state() 返回更粗略的标签。对于行为相同的值，使用同一个标签；省略读者不需要的细节，例如一次返回结果不会改变任何内容的进行中调用。保留错误路径中的每个状态，并保留每个标记。当合并操作将 breaks 状态改为 mayBreak 时，就会隐藏规则被违反的位置。不要合并违反不同规则的两个状态，否则读者就无法看出各条规则分别在哪里被违反。如果图表仍然太繁杂，可以让 step() 对读者不需要的步骤返回 null，例如每个状态都有的重置操作，或箭头内容与其他箭头重复的步骤。隐藏步骤时请遵守以下规则：

• 从起始状态出发，必须能通过箭头到达每个图表状态。
• 对于模型中存在出边的每个图表状态，至少保留一条出边。
• 要么隐藏某条箭头对应的所有步骤，要么一个都不隐藏。只隐藏部分步骤会使其条件范围变窄。
• 在交接说明中指出图表隐藏了哪些步骤。

阅读报告

• 在图表中，违反规则的状态带有 breaks 类。如果其背后的模型状态中只有部分状态违反规则，则带有 mayBreak 类。图例会标出每个标记对应的规则。如果有两条规则被违反，图例会在一个标记上同时标出这两条规则，因此在交接时要说明哪个状态违反了哪条规则。在区域图表中，如果包含某个状态的每种区域状态组合都可能违反规则，该状态就会带有标记。如果某个组合可能违反规则，而其中没有任何状态带有标记，则该组合中的每个状态都会带有标记。
• TLC 会继续越过违反规则的状态，因此图表会显示 bug 之后的状态。
• 由于 TLC 会继续越过 bug，如果模型中的状态没有上限，运行可能永远不会结束。请将常量设得较小，或添加 CONSTRAINT。
• 使用 VIEW 或 SYMMETRY 时，TLC 会把它视为相同的状态计为一个状态，图表也会绘制这个状态。箭头可能指向这个状态，而不是指向该步骤实际到达的状态；报告会对此作出说明。
• TLC 会检查 CONSTRAINT 或 ACTION_CONSTRAINT 之后状态中的规则，但不会探索该状态，也不会检查其中是否存在死锁。如果某条规则的 TLC 最短路径终止于这种状态，图表会绘制该状态，报告也会提供这条路径。图表不会绘制越过边界后的其他状态。这种状态中的死锁不会显示。TLC 还会在 ACTION_CONSTRAINT 排除的每一步之后检查规则，即使它通过其他路径到达了下一个状态也是如此。如果某条规则的 TLC 最短路径以这种步骤结束，图表会绘制该步骤。
• 该命令会使用 TLC，按照原样编写的配置和单个工作线程检查规则。若有规则被违反，命令会移除该规则并再次运行 TLC，直到没有规则被违反。首次发现违反后，每次运行都会在 100,000 个不同状态处停止，避免大型模型永远运行下去。如果运行达到此上限或因错误停止，报告会在“Rules not checked”下列出未检查的规则，图表也不会为它们添加标记。未检查的规则可能成立，也可能被违反。若要检查这些规则，请从配置中移除被违反的规则，或缩小模型范围。此上限会添加一个模块来改变 TLC 对变量的处理顺序，因此对于某个属性，TLC 找到的反例可能与不设上限时运行所找到的不同。
• tlc.out 是 TLC 按照原样编写的配置运行时输出的内容。如果图表没有显示某条被违反规则的 bug 路径，tlc-RULE.out 就是 TLC 在找到该路径的运行中输出的内容。如果 TLC 重复显示其第一条警告，普通的 TLC 会打印两次，但 tlc.out 只会显示一次，因为 TLC 会从此命令读取的输出中省略第二份副本。只有在 Java 使用 -XX:+UseParallelGC 运行时才会发生这种情况，因为在其他情况下，TLC 的第一条警告会建议传入该标志，而这条建议只会打印一次。

展示图表

将 chart.mmd 作为 mermaid 代码块展示给用户。图表的状态数量上限为 500，按 TLC 使用原样编写的配置统计。超过上限后，图表只会绘制通向被违反规则的路径；如果没有规则被违反，命令就不会生成 chart.mmd。命令仍会检查每条规则，报告也会给出状态数量和每条 bug 路径。若要查看完整图形，请缩小模型范围。

使用 Pele 渲染图表。当用户要求提供图像，或图表过大而无法以文本形式阅读时，请遵循 references/render.md。除非用户提出要求，否则不要使用其他渲染器。

交接

将每张图表及其 Mermaid 文本交给负责决策的人。每个 bug 用一行说明：规则、读者对该规则的描述，以及报告所标注的路径。说明模型未涵盖的内容。提供可重新生成这些文件的命令，并使用新的 --out 文件夹。

如果模型描述的是代码，请将每条 bug 路径作为测试或实时复现应用于真实代码，每个动作对应一步。如果某个 bug 没有发生，在证明模型没有问题之前，都应先认为模型有误。