quint-modeling

Quint 建模

根据用户提供的任何起点生成 Quint 规范。本技能负责共享建模准则（如下），并根据输入类型转交给相应的流程指南——也就是将特定类型的输入转化为理解，而共享步骤会以此为基础展开。

有关语言语法、运算符、CLI 和 basicSpells，请参阅 quint-lang 参考文档。本技能关注的是如何建模，而不是 Quint 语法。

---

选择流程

先确定用户的起点，再阅读匹配的指南。指南负责输入处理——从来源中提取系统的状态、操作和假设。完成输入处理后，所有流程都会汇入下方的共享建模主干。

起点	流程	指南
只有一个想法 / 非正式提案，通过与用户互动逐步构建	从零开始	guidelines/from-nothing.md
一份书面需求 / 功能规范文档	从需求开始	guidelines/from-requirements.md
源代码（Rust、Go、TypeScript、……）	从代码开始	guidelines/from-code.md
现有的 TLA+ 规范	从 TLA+ 开始	guidelines/from-tlaplus.md
要审查的已完成 .qnt 规范，而非要构建的规范	审查	guidelines/review.md

前四种是构建流程：输入处理 → 下方的共享建模主干。审查流程则不同——无需生成新模型；你需要按照检查清单审查现有规范并报告发现的问题。该流程不使用主干；请直接阅读并遵循 guidelines/review.md。

如果起点不明确（例如“包含一些伪代码的设计文档”），请先询问用户哪个来源是权威依据，再选择流程——不同流程的输入处理方式会有实质差异。

---

共享建模主干

所有流程最终都会汇入此处。输入处理（因流程而异）会形成对系统的理解：系统的实体、它们执行的操作、每个操作读取和写入的状态，以及系统模型的假设（通信、故障、时间、参与者）。主干会将这种理解转化为经过验证的 Quint 规范。

整个过程中都遵循两项原则：

• 从第一行开始即可执行。 Quint 规范可以立即运行——在做出设计决策时就进行验证，而不是等到最后。每次最多只构建一个步骤，然后就验证上一步：quint typecheck，然后运行 quint run。仅进行类型检查还不够——规范通过类型检查后仍可能无法执行，这会让可执行规范失去意义。需要留意的陷阱：未赋值的 const 可以通过类型检查，但无法运行——quint run 会因 Uninitialized const 而失败。要让规范可运行，请在具体实例模块中实例化该 const—— module spec_3 { import spec(C = Set(1,2,3)).* }——然后运行该模块。（assume 用于记录前提，并不提供值——请参阅步骤 1 和 quint-lang 的 guidelines/simulations.md。） 每次添加内容后，都要实际运行——如果无法对该模块运行 quint run，就说明尚未完成。 只使用 quint run——绝不要使用 quint verify。 这一要求适用于整个技能：构建、迭代、审查、检查不变量——每一步都使用抽样的 quint run，绝不使用 quint verify，最终检查也不例外。verify 是穷举式的有界模型检查（Apalache），速度慢得多（需要数分钟到数小时），不属于建模工作流。它是一种模型检查工具，在 quint-lang 中有说明（guidelines/cli.md、guidelines/simulations.md）——只有在用户明确要求对规范进行模型检查时才使用，切勿自行使用。
• 描述是什么，而不是怎么做。 对可观察的状态转换及其影响进行建模。抽象掉实现细节（序列化、内存管理、重试流程）。如果某个细节不会影响你关注的不变量，就不应纳入规范。

参考示例

examples/ 中附带了两个完整、可运行的规范，分别对应组件协调的两种方式——传递消息或共享状态。几乎所有系统都能归入其中一种；请根据这个问题来选择，而不是根据领域标签，并将更贴近的示例视为主干模式的完整实例（第 2 步状态塑形、第 4 步受保护操作、第 5 步见证与不变量），以了解各部分如何组合成完整规范。（它们是值得学习的典型模式，但不是唯一有效的模式。）

示例	协调方式……	建模以下内容时阅读……
examples/tendermint/	消息传递（choreo:: 广播/发送；真实 BFT 共识）	参与方通过交换消息进行通信的任意分布式协议——共识、BFT、复制、原子提交、领导者选举、可靠广播/闲聊协议、请求/响应、内存池。这是分布式系统的默认参考示例。展示了：分组的 Id -> LocalState（第 2 步）、受保护转换（第 4 步）、choreo::cue 的监听/操作分离、安全不变量（agreement/validity）+ 可问责性/活性视角 + 反例演示（第 5 步）、const 实例化，以及测试分离。横幅中提供了“快速阅读”路径，因此无需通读约 760 行。另请参阅第 2 步的“何时使用 Choreo”和 ../quint-lang/guidelines/choreo.md。
examples/ewd426.qnt	共享状态（无消息）	各部分通过共同状态而非消息进行协调的系统——互斥锁/锁、令牌环、共享寄存器、自稳定系统，以及进程直接读取邻居或环境的任何系统。展示了：分组映射状态（第 2 步）、受保护的 step（第 4 步）、const 实例化，以及 temporal 活性属性（第 5 步）。

如果某个系统同时采用两种方式（例如，通过消息传递通信的节点也会访问共享账本），请从 tendermint 入手（消息传递结构占主导），并按照第 2 步所述，将共享状态作为独立的 var 添加。没有 Choreo 框架的纯消息集合（Set[Msg]）并不是另一种独立形式——Choreo 的广播在底层就是集合，因此 tendermint/ 也可作为这种模式的参考（阅读状态声明和一个受保护转换；choreo:: 封装只是额外的一层）。

第 1 步 — 分离关注点

将理解内容划分为三个层次。将它们分开，才能让规范可测试；把它们混在一起，是规范无法测试最常见的原因。

• 状态机 — 变量、初始化、转换 → var、init、actions
• 函数逻辑 — 纯计算：守卫条件、法定人数检查、状态更新 → pure def
• 属性 — 始终必须成立的内容、必须可达的内容、最终必须发生的内容 → val 不变式 + 见证，以及用于活性的 temporal 属性（第 5 步；quint-lang 中有详细说明）

还要明确系统模型假设——它们会影响其上构建的每个不变式。将它们编码为 const 声明。要实际检查某项假设（例如 2 * f < n 这样的法定人数条件），请编写一个断言该条件的 run 测试——assume 关键字只是记录前提，并不会强制执行，因此不要依赖它来进行检查（关于原因及 run 测试模式，请参阅 quint-lang 的 ## Assume）。每个流程都会根据自身来源（访谈、需求文档、代码或 TLA+）填写以下内容；检查清单始终相同：

关注点	需要回答的问题
通信	参与者如何通信——通过消息还是共享状态？如果通过消息：消息是否可靠、是否有序、是广播还是点对点？（另一个影响模型的问题——在回答参与者问题后立即回答；它会决定第 2 步的消息媒介，并结合参与者数量决定是否采用 Choreo。）
故障	崩溃停止？崩溃恢复？拜占庭故障？n 个中的 f 个占比是多少？
时间	同步？异步？部分同步？是否对超时进行建模？
参与者 / 参与方	参与者和角色分别是什么？每个参与者持有哪些本地状态？（这是最具体的输入问题——首先回答；它会直接影响第 2 步的 Id -> LocalState 结构。）成员固定还是动态？有多少个进程？

如果假设有误，基于它构建的每个属性都会有误——请在开始构建前明确这些假设。

第 2 步 — 确定状态结构

从第 1 步回答的两个问题开始——参与者是谁以及他们如何通信。这两个问题共同决定了本步骤的所有结构选择。 它们不只是背景信息；它们会决定状态结构、消息媒介和框架：

• 参与者数量 → 状态结构。 一个参与者 → 单个 var s: Record。N 个相同类型的参与者 → 一个 Id -> LocalState 映射（记录描述一个参与者；参见下文“扩展至 N 个参与者”）。角色不同 → 将角色设为 LocalState 的一个字段（例如 role: Coordinator | Participant），或使用单独的映射。参与者数量和角色确定后，状态结构也就随之明确。
• 参与者如何通信 → 消息媒介。 使用消息 → 为媒介单独设置一个 var，不要塞进 LocalState：使用无序的 Set[Message] 集合（默认选择），或仅当交付顺序至关重要时，使用按参与者对排序的 ... -> List[Message] 队列。不使用消息、通过公共状态协调 → 共享内存（不需要媒介变量；参见 examples/ewd426.qnt）。这就是下文将详细说明的“通信形态”选择。
• 参与者 + 通信方式 → 是否使用 Choreo。 多个参与者通过交换消息进行协调 → 默认使用 Choreo（参见下文“默认使用 Choreo”）。单个参与者，或通过共享状态进行协调的多个参与者 → 使用普通 Quint。因此，请先回答“参与者是谁、有多少个、他们如何通信？”，这样在编写类型之前，下面三个选择基本就已确定。

将内聚的状态组合成一个记录，让函数层操作该记录——这是推荐的结构，因为大多数情况下，描述一个实体的变量本身就是内聚的；组合起来能让函数层保持整洁，不变式也更易读。保持变量扁平是有意采用的例外，而不是与之并列的默认选择：

• 当以下情况成立时，应将字段组合为一条记录： 这些字段是某个实体的本地状态（节点的阶段 + 日志 + 投票），总是一起传递，或它们之间存在不变式。这是通常情况。
• 仅在以下情况保持扁平（分开的 var）： 变量确实代表彼此独立、会自行变化的关注点，或规范足够小，组合起来不会更清晰。（一些典型示例，例如 ewd840，会将每个字段的映射保持扁平，因为这些字段并未构成明显的整体。）

紧密关联的情况——一个整体：

type State = {
  phase:    str,
  balances: NodeId -> int,
  members:  Set[NodeId],
}

var state: State

纯函数 apply… 接收并返回 State；操作直接赋值下一个状态记录（state' = applyTransfer(state, …)）。无需逐个字段重新组装。

扩展到 N 个实例——有 N 个参与者时，记录描述一个参与者的本地状态，变量则变为以参与者 ID 为键的映射。纯函数无需更改——它们仍然对单个 LocalState 进行操作；只需更改外围连接方式：

type NodeId = int
type LocalState = { phase: str, balance: int, voted: bool }

var nodes:    NodeId -> LocalState   // per-actor cohesive state
var messages: Set[Message]           // genuinely global concern → its OWN var, not inside LocalState

	一个实例	N 个实例
状态变量	var state: State	var nodes: NodeId -> LocalState
纯函数	can…(State, …): bool + apply…(State, …): State	can…(LocalState, …): bool + apply…(LocalState, …): LocalState — 形态相同
操作读取	读取 state	nodes.get(id)
操作写入	state' = applyOp(state, …)	nodes' = nodes.set(id, applyOp(nodes.get(id), …))
init	一个记录字面量	NODES.mapBy(_ => <record>)

简而言之：将紧密关联的状态组合成一条记录（一个整体对应一个变量，N 个实例则使用 Id -> LocalState 映射），并将真正独立的关注点——消息集合、共享注册表——分别作为独立变量，切勿塞进每个实例的记录中。只有当各字段无法构成一个整体时，才使用扁平的逐字段变量。

通信结构（应与状态结构一并决定）：

• 消息集合——var network: Set[Message]，进程接收任意正在传输中的消息。这是异步协议的默认方式；除非顺序确实重要，否则应使用它。
• 共享内存——没有消息介质；进程直接读写公共状态。参见附带的 examples/ewd426.qnt（一个令牌环，每个节点都会读取其邻居）。
• 有序的逐对队列——... -> List[Message]，配合头部/尾部操作。仅在语义上必须保证传递顺序时使用（例如逻辑时钟因果关系）；与消息集合相比，它的模型检查开销更高。语料库规范 LamportMutex 是典型示例——除非能明确说明顺序为何不可或缺，否则优先使用消息集合。

对分布式协议默认使用 Choreo

对于任何包含 N 个进程的分布式消息传递协议（共识、BFT、复制、多阶段提交、广播／gossip、领导者选举），默认使用 Choreo 框架；如果不打算使用，就应经过审慎权衡并说明理由。这不是风格上的随意选择：Choreo 的 listen → react 结构，以及它对本地状态更新与网络效应的清晰拆分（choreo::cue 模式），会主动引导你编写结构更好、也更易审查的规范，而不是手工编写 NodeId -> LocalState 加上杂乱消息的 step。默认预期是使用 Choreo；对于消息传递协议，使用纯 Quint 反而需要给出理由。

唯一合理的弃用理由：对于一个小型协议，Choreo 的脚手架（类型样板代码——LocalContext/Transition/effects——以及框架接线）可能带来过多仪式，而规范结构的收益不足以抵消，使规范明显更加冗长却收获甚少。这确实需要权衡判断，但这是唯一常见的例外，即便如此，也应倾向于使用 Choreo。还有两种结构性情况不适用 Choreo：单个参与者（没有进程间消息需要协调）和共享内存协调（完全没有消息媒介 → 使用纯 Quint，参见 examples/ewd426.qnt）。

不算理由：“还在探索设计。” 你可以在 Choreo 中探索，而且之后切换框架代价很高，因此不要以此为由推迟决定。

这是一个结构性分岔——应在编写逻辑之前决定。 如果你打算对本可使用 Choreo 的协议采用纯 Quint，请告知用户，说明冗长程度与收益之间的取舍，并征得同意（将此纳入下方类型草图的确认环节）。

适用 Choreo 时，每个进程的状态仍遵循上述分组规则——Choreo 只是在此基础上提供消息传递和处理器脚手架。框架 API 和模式请参阅 ../quint-lang/guidelines/choreo.md；完整、可运行的 Choreo 规范请参阅 examples/tendermint/。其中的真实 BFT 共识展示了 choreo::cue 的 listen/act 拆分、agreement/validity/accountability 不变量，以及在单独的 tendermintTest.qnt 中基于 with_cue 的测试（通过 --main=valid 运行）。

与用户共同决定分组方式（以及是否使用 Choreo），并且在编写任何逻辑之前，先就类型草图取得明确批准（步骤 3）。先对类型和 var 声明进行类型检查；这是最具杠杆效应的审查节点——如果形状不对，之后改起来代价很高。

步骤 3 — 编写函数式逻辑（纯函数）

将每个操作的逻辑实现为 pure def——它们接收状态记录和参数，并返回普通值，因此你可以在 REPL 中用手工构造的状态进行测试。将转换要回答的两个不同问题拆开：

• 能否发生？——返回 bool 的 pure def … 守卫（前置条件）。
• 结果状态是什么？——返回 State 的 pure def …，用于计算下一状态，前提是守卫成立。

pure def canTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): bool =
  amount > 0 and from != recipient and s.balances.get(from) >= amount

pure def applyTransfer(s: State, from: NodeId, recipient: NodeId, amount: int): State =
  { ...s, balances: s.balances.setBy(from, b => b - amount)
                              .setBy(recipient, b => b + amount) }

先编写签名（用存根填充函数体），进行类型检查，然后一次填充一个函数，并在继续之前用手工构造的状态在 REPL 中测试每个函数。如果输出出乎意料，说明函数有 bug——在将其接入状态机之前先修好。

将守卫与更新分开，因为它们是关于操作的两个独立事实：一个说明何时允许操作，另一个说明操作的效果。动作（步骤 4）会使用守卫来决定是否触发。使用单个 pure def 返回 { success, newState }——在守卫失败时返回未改变的状态——会把两者合并，并使动作倾向于采用无操作分支；应优先采用拆分方式。（如果系统会观察并响应操作失败这一事实，就将该失败建模为独立的有守卫动作，而不是后备行为。）

步骤 4 — 编写状态机连线（带守卫的动作）

一个动作会在同一个 all { ... } 中将守卫和更新组合起来：守卫控制动作是否触发，更新设置下一个状态。守卫为假时，动作处于禁用状态——不会触发，也不会改变任何内容。无需 success 标志，也无需无操作分支。

action init: bool = all {
  state' = { phase: "idle",
             balances: NODES.mapBy(_ => INITIAL_BALANCE),   // pre-populate every map
             members: NODES },
}

action transferAction(from: NodeId, recipient: NodeId, amount: int): bool = all {
  canTransfer(state, from, recipient, amount),          // guard — disables the action when false
  state' = applyTransfer(state, from, recipient, amount),
}

禁用动作是“此状态下不可能发生”的忠实模型。不要为了让流程继续而添加一概适用的 else / unchanged_all 回退分支——这会在模型中加入真实系统无法执行的转换，无论之后如何处理规范，这都是建模不准确。

动作和 pure def 不能同名。在 init 中预先填充每个映射——对不存在的键调用 .get() 会导致未定义行为。完整的此类注意事项列表请参阅 quint-lang。

步骤 5 — 属性：先检查可达性，再检查不变量

先检查可达性。 可达性检查会指定目标状态，并询问它是否可达——以肯定形式编写谓词（即希望到达的状态），并传给 quint run --witnesses，该命令会报告采样轨迹中有多少条到达了该状态。每个主要动作都添加一个可达性检查：若 0 条轨迹到达该状态，说明该动作已失效（其前置条件永远不可能成立），因此应先修复，再投入精力检查安全性。

// the state you want to be reachable — written plainly, no negation
val someBalanceChanged: bool =
  state.members.exists(n => state.balances.get(n) != INITIAL_BALANCE)

quint run spec.qnt --witnesses someBalanceChanged --max-steps 10
  → someBalanceChanged was witnessed in 90 trace(s) out of 100 explored (90.00%)

计数非零表示该状态可达；0% 表示从未发生——请进行调查。

还有第二种互补形式：将条件取反，写成不变量——val w = not(target)——这样报告的“违反”就表示某次执行到达了该状态。它无法与其他不变量一起批量检查，而且要把“违反”视为成功；但它能提供 --witnesses 无法提供的内容：一条到达该状态的实际轨迹。根据需求选择——常规可达性和覆盖率检查使用 --witnesses；想要查看路径（了解或记录如何到达该状态，或调试意外触发的可达性检查）时，使用取反不变量形式。

然后检查不变量——这些安全属性必须在每个可达状态中成立：

val noNegativeBalances: bool =
  state.members.forall(n => state.balances.get(n) >= 0)

不变量和可达性检查可在一次运行中一起执行：quint run --invariant noNegativeBalances --witnesses someBalanceChanged。

当某个源产生许多候选属性，而你需要安排验证工作的优先级时，from-requirements 流程提供了一种按影响程度划分高／中／低的辅助方法（guidelines/from-requirements.md）；只要是根据明确要求进行建模，都可以使用它。

（关于可达性检查与不变量的解读、公平性和时序属性的详细说明，请参阅 quint-lang 的 guidelines/simulations.md。someBalanceChanged 是状态证据——应恰当表述这类目标，使其只能由某个动作触发为真，因为若某个谓词在 init 时就已成立，它会在第 0 步被视为“已到达”，因此不构成可达性证据。若要确认多个动作中某个特定动作已触发，请使用每个动作专属的 var 标志——quint-lang 的 guidelines/patterns.md §7 介绍了相关方法，以及如何调试始终未触发的可达性检查。）

步骤 6 — 组合 step 并进行模拟

在 any { ... } 中组合各个动作，并通过随机游走对模型进行压力测试。

action step: bool = {
  nondet from = NODES.oneOf()
  nondet dst  = NODES.oneOf()   // `dst`, not `to` (a built-in) — see quint-lang
  any {
    transferAction(from, dst, 10),
    // other actions…
  }
}

• 使用 quint run --witnesses 检查可达性——预期轨迹计数非零（状态可达）；0% 表示动作已失效。
• 使用 quint run 检查不变量（采样）——预期不会出现违反；出现反例时，逐步阅读轨迹。为此请使用 quint run，而不是 quint verify（参见“从第一行即可执行”原则——只有用户明确要求进行模型检查时才使用 verify）。

带守卫的模型可能到达没有任何操作可执行的状态

由于操作带有守卫（步骤 4），模型可能到达没有任何可执行操作的状态。构建期间容易踩到的陷阱：quint run 不会检测死锁——它会提前停止，并输出 [ok] No violation found，且轨迹短于 --max-steps。短轨迹是唯一的提示，而运行结果看起来像是成功，因此，如果你预期协议会继续运行，就要留意轨迹长度。（补充说明：quint verify 会直接报告死锁——Found a deadlock——但那是模型检查步骤，只有用户明确要求时才会用到；构建期间如果怀疑有死锁，不要为了追查它而改用 verify——而应使用 quint run 检查短轨迹。）

到达这种状态是否正确，取决于系统：应该持续提供服务的系统绝不能卡住，而确实会结束的系统（所有人都已提交，没有待办事项）本就应该进入终止状态。工具无法区分二者——只有你知道自己期望哪一种。（这也是步骤 4 避免使用空操作兜底的另一个原因：一概使用 unchanged_all 会让每条轨迹无限延长，因此模型永远无法到达或揭示这种状态。）

关于边界的说明。 --max-steps（一次运行探索的深度）不是建模决策——它始终存在。模型本身是否具有有界状态空间才是建模决策：有些协议按设计就是会终止的（一次性提交到达最终状态后便停止），如此建模是正确的——到达终止状态是设计目标，并非死锁。你也可以有意限制原本无界的模型，以缩小状态空间，但绝不能通过空操作作为逃生口（步骤 4）——应通过建模真实的终止状态来限制模型，而不是添加虚假的步骤。

测试（run 定义）应放在单独的 *_test.qnt 文件中，并导入规范——让主模块不包含测试场景。逐步构建：每次添加后都进行类型检查，每个操作后都进行模拟。

步骤 7 — 自我审查，然后移交规范

在撰写移交记录之前，快速检查一下自己的规范，标准与审阅者会采用的相同——现在发现这些问题，比之后被退回修改更省事。大部分要求你在编写时已经遵循；这是最后一次检查，确保它们彼此一致：

• 带守卫的操作 — 操作中除守卫和赋值外不包含业务逻辑；业务逻辑放在 pure def 中，并将守卫提升到操作中，使其在无法触发时被禁用（步骤 4）。
• 每个主要操作都有见证 — step 中的每个操作都有一个见证，并且在 quint run --witnesses 下，每个操作在 > 0 条迹中都能被触达，而不是在 0 条迹中成为死代码（步骤 5）。
• 至少一个协议级不变量 — 真正的安全属性（没有两个领导者、守恒、一致性），而不只是类型／边界检查；并且每个不变量都引用一个 var。
• init 为每个 var 赋值，且每个操作都为每个 var 赋值（缺少 x' = x 会造成静默的停滞错误）；每个映射都已预填充（步骤 4）。
• 抽象层次恰当 — ID 是不透明的（不进行字符串操作）；除非顺序本身就是待验证的属性，否则消息使用 Set；不引入序列化、重试或内存细节。

如果规范较大或要移交给其他人，请运行 guidelines/review.md 中的完整审查（包含报告的 C1–C6 / R1–R2 检查清单）——自查不够时再采用。

完成的规范需要一份简短记录，让下一位读者了解其范围并能够信任它。请以注释块、README.md 或工作流偏好的其他形式编写，涵盖以下内容：

• 涵盖内容 — 建模了哪些模块／协议，编码了哪些假设（const 声明，以及对必须成立的假设进行的 run 测试检查），验证了哪些属性。
• 未涵盖内容 — 有意省略的实现细节、排除的边缘情况（及原因）、仍需添加的属性。这份诚实说明可以防止他人过度信任该规范。
• 何时更新 — 对于作为某个制品（代码、TLA+ 源文件）依据的规范，修改制品之前先更新规范并重新验证。

规范是真实依据。绝不要为了匹配有缺陷的代码而修改规范。 如果规范有误，请停下来与用户讨论——这是最具杠杆效应的审查环节。

每种工作流还有各自的格式细节（代码工作流要求注明与源文件的对应关系，TLA+ 工作流要求提供记录了 quint run 输出的翻译 README，交互式构建则要求使用注释块）。

---

约定

• 每个参与者的状态使用 NodeId / LocalState，参与者集合使用 NODES（模型所遍历的 Set[NodeId]）；协议相关的类型名称应具有描述性（VoteRequest、PrepareMsg），不要使用 Msg1、Msg2。
• 小规模取值域：参与者数量设为 N = 3（初步探索时也可以是 N = 2），值域使用 0..10 等范围，就足以覆盖大多数安全属性，也能让模拟成本较低。参与者使用符号 ID（int 或 str）。
• 消息集合：将已发送的消息存储在一个 Set 中，除非顺序本身就是待验证的内容，否则不要对消息传递顺序建模。
• 抽象时间：当协议包含时间或进度概念时，将其建模为整数轮次／纪元计数器（round: int），而不是墙上时钟时间或计时器机制——超时只需让轮次递增即可。例外：只有待验证的内容本身是时间界限时，才明确对计时建模。
• 从一个操作开始：先让 init、一个操作和一个见证正常运行，再添加其余部分。对于 N 个参与者，先对一个参与者建模并验证，然后再推广到映射——绝不要一次性接入全部 N 个参与者。
• 在 REPL 中使用手动构造的状态，单独测试纯函数；这样能在逻辑错误与状态机纠缠之前发现它们。

对于语法相关的所有内容——运算符、未定义行为规则、basicSpells、CLI 标志——请查阅 quint-lang 参考文档，而不要在此重述。