statechart

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Statechart

状态图（Statechart）

The chart shows what an app's user sees. A PM reads it to decide whether that behavior is right. Label each state with what is on the screen, such as "Paying". Label each step with what the user does or sees happen, such as "tap Pay" or "the charge goes through". Keep variable and action names out of labels. The scripts call this user the reader, as in

readerActions

and reader steps.

Run

node <skill dir>/scripts/statechart.mjs --help

for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input.

图表展示应用用户看到的内容。PM 阅读图表，以判断该行为是否正确。为每个状态标注屏幕上显示的内容，例如“正在支付”。为每个步骤标注用户做了什么或看到了什么，例如“点击支付”或“扣款成功”。标签中不要使用 variable 或 action 名称。脚本将这位用户称为 reader，例如

readerActions

和 reader 步骤。

运行

node <skill dir>/scripts/statechart.mjs --help

查看可用命令以及图表的阅读方式。在 repo 之外的临时工作目录中操作。该命令会在输入文件旁写入生成的文件。

Pick the direction

选择方向

Use

from-spec

when a TLA+ model exists or the code is concrete enough to model. Use

from-chart

when there is no model and the PM should agree on the behavior before anyone writes or changes the code.

If the code already has a TLA+ spec, start from a copy of that spec. Add the variables the user sees, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as

--against

. In a new spec, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code.

已有 TLA+ 模型，或者代码具体到足以建模时，使用

from-spec

。没有模型，且需要 PM 在任何人编写或修改代码之前先认可行为时，使用

from-chart

。

如果代码中已有 TLA+ spec，则从该 spec 的副本开始。添加用户可见的 variable，并保留 spec 中已有的 invariant。若要根据 spec 审计代码，则让副本反映代码的实际行为，并将未经修改的 spec 作为

--against

传入。在新 spec 中，将每个 variable 和 action 与 reviewer 可以打开的代码关联起来，并沿用代码中的名称。让每个 action 在代码中对应一个不可分割的步骤。

Spec to chart

从 spec 到图表

Choose the chart's states. When the PM cares about something the screen does not show, such as a second charge while the screen still says "Paying", name the state "Paying, charged twice". Start with few states, and split a state only when the split separates two bugs.
Write each rule the PM agrees to as one invariant, with the PM's sentence as its comment. For a rule that applies once everything settles, define
```
Settled == ~ENABLED System
```
, where
```
System
```
is the disjunction of the actions the user does not take. Report each broken rule as a bug. Never weaken a rule to make the chart pass.
Run
```
from-spec
```
, then fill in the mapping file it writes. Put the labels in
```
state
```
and
```
step
```
, and list the user's actions in
```
readerActions
```
by action name. When two bugs end on the same screen through different code paths, add
```
cause
```
and make it name the code path. To color the states by what the PM cares about, such as "Toast shown", return that group from
```
group
```
. The legend names the groups, and states that break a rule still get a red border.
If there is an open fix, model it from the code and pass that model as
```
--fixed
```
.
Render each chart with
```
--png
```
and look at every PNG. Check that each numbered path reads in order. If a label reads like code, fix
```
state
```
or
```
step
```
and run the command again.
Replay each bug's story against the real code, as a test or a live repro, one step per model action. If a bug does not reproduce, assume the model is wrong until you show otherwise. Fix the model, not the rule.

选择图表的状态。当 PM 关心某个屏幕上未显示的内容时，例如屏幕仍显示“正在支付”期间发生了第二次扣款，则将状态命名为“正在支付，已扣款两次”。先从少量状态开始，仅当拆分能够区分两个 bug 时，才拆分状态。
将 PM 认可的每条规则写成一个 invariant，并以 PM 的原句作为注释。对于一切稳定后才适用的规则，定义
```
Settled == ~ENABLED System
```
，其中
```
System
```
是用户不会执行的 action 之析取。将每条被违反的规则报告为一个 bug。绝不能为了让图表通过而弱化规则。
运行
```
from-spec
```
，然后填写它生成的 mapping 文件。将标签填入
```
state
```
和
```
step
```
，并按 action 名称将用户操作列入
```
readerActions
```
。如果两个 bug 通过不同代码路径最终落在同一屏幕状态中，添加
```
cause
```
，并让它指明代码路径。要按照 PM 关注的内容为状态着色，例如“显示 Toast”，请从
```
group
```
返回该分组。图例会命名这些分组；违反规则的状态仍会带红色边框。
如果存在待合入的修复，则根据代码为该修复建模，并将模型作为
```
--fixed
```
传入。
使用
```
--png
```
渲染每张图表，并逐一查看每个 PNG。检查每条带编号的路径是否能够按顺序阅读。如果某个标签读起来像代码，修正
```
state
```
或
```
step
```
，然后重新运行命令。
针对真实代码重放每个 bug 的故事，可以通过测试或现场复现进行，并让模型中的每个 action 对应一个步骤。如果 bug 无法复现，在拿出反证之前，先假定模型有误。应修正模型，而不是规则。

Chart to spec

从图表到 spec

Draw the chart the PM agrees to. Use one region for each thing that changes independently, such as the connection and the sync badge. Add one
```
%% never
```
line per rule, with the PM's sentence. Draw "the app closes" as an edge to the state the user sees next.
Run
```
from-chart
```
. If a rule breaks, the agreed chart has a design bug. Take the bug to the PM.
Add the real code's guards and variables to the spec that
```
from-chart
```
wrote, and run
```
from-chart
```
again. For each difference it prints, ask the PM whether the code is wrong or the chart needs a correction.

绘制 PM 认可的图表。对每个独立变化的事物使用一个 region，例如连接状态和同步徽标。每条规则添加一行
```
%% never
```
，并附上 PM 的原句。将“应用关闭”绘制为一条边，指向用户接下来看到的状态。
运行
```
from-chart
```
。如果某条规则被违反，说明已认可的图表存在设计 bug。将该 bug 提交给 PM。
将真实代码中的 guard 和 variable 添加到
```
from-chart
```
生成的 spec 中，然后再次运行
```
from-chart
```
。对于它打印出的每一处差异，询问 PM：是代码有误，还是图表需要更正。

Hand off

交付

Give the PM the PNG and the Mermaid source of each chart. Add one line per bug with the rule it breaks, its steps as the chart numbers them, whether it reproduced, and whether the open fix fixes it. Take every count you quote from

summary.json

. Attach

stories.md

and the command that regenerates everything. Say what the model leaves out.

向 PM 提供每张图表的 PNG 和 Mermaid 源码。每个 bug 添加一行，记录其违反的规则、按图表编号列出的步骤、是否成功复现，以及待合入的修复能否解决它。引用的每个计数都应取自

summary.json

。附上

stories.md

以及可重新生成全部内容的命令。说明模型未涵盖哪些内容。