quint-lang

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Quint Language Reference

Quint语言参考手册

Quint is an executable specification language for complex systems, developed by Informal Systems. It compiles to TLA+ and supports simulation and model checking.

Quint是由Informal Systems开发的面向复杂系统的可执行规范语言，可编译为TLA+，并支持模拟与模型检查。

Module structure

模块结构

quint

module MyProtocol {
  // type aliases, constants, state, actions, properties
}

Modules can import others:

quint

import Voting.*              // all definitions
import Voting(quorum)        // specific definition
import Voting as V           // namespace alias

quint

module MyProtocol {
  // 类型别名、常量、状态、动作、属性
}

模块可导入其他模块：

quint

import Voting.*              // 导入所有定义
import Voting(quorum)        // 导入特定定义
import Voting as V           // 命名空间别名

Types

类型

Type	Description	Example
`int`	Integers	`-1, 0, 42`
`bool`	Booleans	`true, false`
`str`	Strings	`"hello"`
`Set[T]`	Finite set	`Set(1, 2, 3)`
`List[T]`	Ordered sequence	`List(1, 2, 3)`
`K -> V`	Key-value map (type is `K -> V` , not `Map[K, V]` )	value: `Map("a" -> 1)`
`(T1, T2)`	Tuple	`(1, "x")`
`{ f: T, g: U }`	Record	`{ x: 1, ok: true }`
`T \| U`	Sum (variant)	(use type alias)

Type aliases:

quint

type NodeId = int
type Phase = Idle | Propose | Vote | Commit   // enum — prefer over string literals

类型	描述	示例
`int`	整数	`-1, 0, 42`
`bool`	布尔值	`true, false`
`str`	字符串	`"hello"`
`Set[T]`	有限集合	`Set(1, 2, 3)`
`List[T]`	有序序列	`List(1, 2, 3)`
`K -> V`	键值映射（类型为 `K -> V` ，不是 `Map[K, V]` ）	值： `Map("a" -> 1)`
`(T1, T2)`	元组	`(1, "x")`
`{ f: T, g: U }`	记录	`{ x: 1, ok: true }`
`T \| U`	求和类型（变体）	（使用类型别名）

类型别名：

quint

type NodeId = int
type Phase = Idle | Propose | Vote | Commit   // 枚举——优先于字符串字面量

Definitions

定义

quint

// Module parameter — fixed at instantiation, not a state variable
const N: int
const Nodes: Set[str]

// Pure function — no state access, usable anywhere
pure def max(a: int, b: int): int = if (a > b) a else b

// Stateful operator — can read vars, takes arguments (unlike val)
def isActive(n: str): bool = active.contains(n)

// State-reading value — can read vars, no arguments
val quorum: bool = votes.size() * 2 > nodes.size()

// Compile-time constant
pure val N: int = 4
val threshold: int = N / 2 + 1

const

pure val

const

is a module parameter bound at instantiation (

import A(N = 3)

);

pure val

is a fixed expression computed once.

def

val

def

takes arguments;

val

does not.

quint

// 模块参数——实例化时固定，不是状态变量
const N: int
const Nodes: Set[str]

// 纯函数——无状态访问，可在任意位置使用
pure def max(a: int, b: int): int = if (a > b) a else b

// 有状态运算符——可读取变量，接受参数（与val不同）
def isActive(n: str): bool = active.contains(n)

// 读取状态的值——可读取变量，无参数
val quorum: bool = votes.size() * 2 > nodes.size()

// 编译时常量
pure val N: int = 4
val threshold: int = N / 2 + 1

const

与

pure val

的区别：

const

是实例化时绑定的模块参数（

import A(N = 3)

）；

pure val

是仅计算一次的固定表达式。

def

与

val

的区别：

def

接受参数；

val

不接受参数。

State variables

状态变量

quint

type LocalState = {
  leader: int,
  phase: Phase,        // enum (see Type aliases) — prefer over a bare str
  votes: Set[int],
  log: List[str],
}

var localState: LocalState  // cohesive local protocol state
var peers: int -> str       // independent concern (peer metadata)

State variables can only be read in

val

definitions and actions; they cannot be read in

pure def

quint

type LocalState = {
  leader: int,
  phase: Phase,        // 枚举（见类型别名）——优先于裸字符串
  votes: Set[int],
  log: List[str],
}

var localState: LocalState  // 内聚的本地协议状态
var peers: int -> str       // 独立关注点（节点元数据）

状态变量仅能在

val

定义和动作中读取；无法在

pure def

中读取。

Actions

动作

Actions describe state transitions. They return

bool

—

true

if the action fires.

quint

action init: bool = all {
  leader' = 0,
  phase' = Idle,
  votes' = Set(),
  log' = List(),
  state' = Map(),
}

action propose(node: int): bool = all {
  phase == Idle,
  node > 0,
  leader' = node,
  phase' = Propose,
  votes' = votes,
  log' = log,
  state' = state,
}

Key rules:

Every
```
var
```
must be assigned in every action (use
```
x' = x
```
to leave unchanged).
```
all { ... }
```
— all sub-expressions must hold (conjunction). Guards are plain boolean expressions inside
```
all { }
```
.
```
any { ... }
```
— at least one must hold (disjunction); the REPL picks non-deterministically.

动作描述状态转换，返回

bool

值——返回

true

表示动作触发。

quint

action init: bool = all {
  leader' = 0,
  phase' = Idle,
  votes' = Set(),
  log' = List(),
  state' = Map(),
}

action propose(node: int): bool = all {
  phase == Idle,
  node > 0,
  leader' = node,
  phase' = Propose,
  votes' = votes,
  log' = log,
  state' = state,
}

核心规则：

每个
```
var
```
必须在每个动作中赋值（使用
```
x' = x
```
保持不变）。
```
all { ... }
```
——所有子表达式必须成立（合取）。守卫是
```
all { }
```
内的普通布尔表达式。
```
any { ... }
```
——至少有一个表达式成立（析取）；REPL会非确定性选择。

Non-determinism

非确定性

quint

action step: bool = any {
  propose(1),
  propose(2),
  vote,
  timeout,
}

// Non-deterministic choice from a set
action deliverMessage: bool = {
  nondet msg = pending.oneOf()
  all {
    pending.size() > 0,
    delivered' = delivered.union(Set(msg)),
    pending' = pending.exclude(Set(msg)),
    // ... other vars unchanged
  }
}

quint

action step: bool = any {
  propose(1),
  propose(2),
  vote,
  timeout,
}

// 从集合中非确定性选择
action deliverMessage: bool = {
  nondet msg = pending.oneOf()
  all {
    pending.size() > 0,
    delivered' = delivered.union(Set(msg)),
    pending' = pending.exclude(Set(msg)),
    // ... 其他变量保持不变
  }
}

Set operators

集合运算符

quint

Set(1, 2, 3).contains(2)          // true
Set(1, 2).union(Set(2, 3))        // Set(1, 2, 3)
Set(1, 2, 3).intersect(Set(2, 3)) // Set(2, 3)
Set(1, 2, 3).exclude(Set(2))      // Set(1, 3)
Set(1, 2, 3).filter(x => x > 1)  // Set(2, 3)
Set(1, 2, 3).map(x => x * 2)     // Set(2, 4, 6)
Set(1, 2, 3).fold(0, (acc, x) => acc + x)  // 6
Set(1, 2, 3).size()               // 3
Set(1, 2, 3).forall(x => x > 0)  // true
Set(1, 2, 3).exists(x => x > 2)  // true
1.to(5)                           // Set(1, 2, 3, 4, 5)
nondet x = Set(1, 2, 3).oneOf()   // non-deterministic pick — only valid in nondet bindings

quint

Set(1, 2, 3).contains(2)          // true
Set(1, 2).union(Set(2, 3))        // Set(1, 2, 3)
Set(1, 2, 3).intersect(Set(2, 3)) // Set(2, 3)
Set(1, 2, 3).exclude(Set(2))      // Set(1, 3)
Set(1, 2, 3).filter(x => x > 1)  // Set(2, 3)
Set(1, 2, 3).map(x => x * 2)     // Set(2, 4, 6)
Set(1, 2, 3).fold(0, (acc, x) => acc + x)  // 6
Set(1, 2, 3).size()               // 3
Set(1, 2, 3).forall(x => x > 0)  // true
Set(1, 2, 3).exists(x => x > 2)  // true
1.to(5)                           // Set(1, 2, 3, 4, 5)
nondet x = Set(1, 2, 3).oneOf()   // 非确定性选择——仅在nondet绑定中有效

List operators

列表运算符

quint

List(1, 2, 3).head()              // 1
List(1, 2, 3).tail()              // List(2, 3)
List(1, 2, 3).length()            // 3
List(1, 2, 3).nth(1)              // 2  (0-indexed)
List(1, 2, 3).append(4)           // List(1, 2, 3, 4)
List(1, 2).concat(List(3, 4))     // List(1, 2, 3, 4)
List(1, 2, 3).foldl(0, (acc, x) => acc + x)  // 6
List(1, 2, 3).select(x => x > 1) // List(2, 3)

quint

List(1, 2, 3).head()              // 1
List(1, 2, 3).tail()              // List(2, 3)
List(1, 2, 3).length()            // 3
List(1, 2, 3).nth(1)              // 2 （0索引）
List(1, 2, 3).append(4)           // List(1, 2, 3, 4)
List(1, 2).concat(List(3, 4))     // List(1, 2, 3, 4)
List(1, 2, 3).foldl(0, (acc, x) => acc + x)  // 6
List(1, 2, 3).select(x => x > 1) // List(2, 3)

Map operators

映射运算符

quint

Map("a" -> 1, "b" -> 2).get("a")        // 1
Map("a" -> 1).put("b", 2)               // Map("a" -> 1, "b" -> 2)
Map("a" -> 1, "b" -> 2).keys()          // Set("a", "b")
Set(1, 2, 3).mapBy(k => k * 2)          // Map(1 -> 2, 2 -> 4, 3 -> 6)  — set of keys → map

quint

Map("a" -> 1, "b" -> 2).get("a")        // 1
Map("a" -> 1).put("b", 2)               // Map("a" -> 1, "b" -> 2)
Map("a" -> 1, "b" -> 2).keys()          // Set("a", "b")
Set(1, 2, 3).mapBy(k => k * 2)          // Map(1 -> 2, 2 -> 4, 3 -> 6)  —— 键集合→映射

Records

记录

Records group related fields into a named type. They are the primary tool for modelling structured state in Quint.

记录将相关字段分组为命名类型，是Quint中建模结构化状态的主要工具。

Type aliases for records

记录的类型别名

quint

type NodeState = {
  phase:  Phase,   // enum: Idle | Propose | Vote | Commit
  voted:  bool,
  log:    List[int],
}

type Message = {
  from:    int,
  to:      int,
  round:   int,
  payload: str,
}

quint

type NodeState = {
  phase:  Phase,   // 枚举：Idle | Propose | Vote | Commit
  voted:  bool,
  log:    List[int],
}

type Message = {
  from:    int,
  to:      int,
  round:   int,
  payload: str,
}

Creating and accessing

创建与访问

quint

val n: NodeState = { phase: Idle, voted: false, log: List() }
n.phase                          // Idle
n.voted                          // false

quint

val n: NodeState = { phase: Idle, voted: false, log: List() }
n.phase                          // Idle
n.voted                          // false

Updating (immutable — returns a new record)

更新（不可变——返回新记录）

quint

{ ...n, phase: Propose }                            // ✅ preferred — idiomatic, handles multiple fields
{ ...n, voted: true, phase: Vote }                  // ✅ multiple fields at once

n.with("phase", Propose)                            // ⚠️ valid but non-idiomatic — field name is a string literal

quint

{ ...n, phase: Propose }                            // ✅ 推荐——符合惯用写法，支持多字段更新
{ ...n, voted: true, phase: Vote }                  // ✅ 同时更新多个字段

n.with("phase", Propose)                            // ⚠️ 合法但不符合惯用写法——字段名为字符串字面量

Records as state — when to group variables

作为状态的记录——何时分组变量

TLA+ specs typically flatten all state into independent top-level variables. Quint's type system lets you group them. When fields describe one cohesive local state, make a record type and use a single state variable of that type.

Group into a record when:

They represent the local state of a single actor (e.g. one node's phase + log + vote)
They are always passed together as function arguments
An invariant relates multiple fields of the same conceptual entity

Keep flat when:

The variables represent distinct concerns that change independently
The component is simple and grouping adds no clarity
The variables are intentionally in different ownership/lifecycle domains

TLA+规范通常将所有状态扁平化为独立的顶层变量。Quint的类型系统允许将变量分组。当字段描述一个内聚的本地状态时，创建记录类型并使用该类型的单个状态变量。

适合分组为记录的场景：

它们代表单个参与者的本地状态（例如一个节点的阶段+日志+投票）
它们总是作为函数参数一起传递
某个不变量涉及同一概念实体的多个字段

适合保持扁平的场景：

变量代表独立变化的不同关注点
组件简单，分组不会增加清晰度
变量属于不同的所有权/生命周期域

Example: preferred grouped local state vs. anti-pattern

示例：推荐的分组本地状态 vs 反模式

Preferred (cohesive local state):

quint

type LocalState = {
  id: int,
  phase: Phase,
  est1: int,
  est2: Option[int],   // Option is from basicSpells, not built in — see Basic spells below
  round: int,
  crashed: bool,
  leader: int,
  received_messages: Set[Message],
}

var localState: LocalState

Avoid for cohesive local state:

quint

var id: int
var phase: Phase
var est1: int
var est2: Option[int]
var round: int
var crashed: bool
var leader: int
var received_messages: Set[Message]

For N actors, use a map of grouped records:

quint

type LocalState = { phase: Phase, votedFor: int, log: List[int] }

var nodes: int -> LocalState

action commit(id: int): bool = {
  val node = nodes.get(id)
  all {
    node.phase == Vote,
    nodes' = nodes.put(id, {...node, phase: Commit}),
  }
}

推荐（内聚本地状态）：

quint

type LocalState = {
  id: int,
  phase: Phase,
  est1: int,
  est2: Option[int],   // Option来自basicSpells，非内置——见下方基础工具集
  round: int,
  crashed: bool,
  leader: int,
  received_messages: Set[Message],
}

var localState: LocalState

内聚本地状态应避免的写法：

quint

var id: int
var phase: Phase
var est1: int
var est2: Option[int]
var round: int
var crashed: bool
var leader: int
var received_messages: Set[Message]

对于N个参与者，使用分组记录的映射：

quint

type LocalState = { phase: Phase, votedFor: int, log: List[int] }

var nodes: int -> LocalState

action commit(id: int): bool = {
  val node = nodes.get(id)
  all {
    node.phase == Vote,
    nodes' = nodes.put(id, {...node, phase: Commit}),
  }
}

Nested records

嵌套记录

quint

type ClusterState = {
  nodes:   int -> NodeState,
  leader:  int,
  epoch:   int,
}

var cluster: ClusterState

// Read nested field:
cluster.nodes.get(1).phase

// Update nested field (must rebuild from the inside out):
val updated = {...cluster.nodes.get(1), phase: Commit}
cluster' = {...cluster, nodes: cluster.nodes.put(1, updated)}

quint

type ClusterState = {
  nodes:   int -> NodeState,
  leader:  int,
  epoch:   int,
}

var cluster: ClusterState

// 读取嵌套字段:
cluster.nodes.get(1).phase

// 更新嵌套字段（必须从内到外重建）:
val updated = {...cluster.nodes.get(1), phase: Commit}
cluster' = {...cluster, nodes: cluster.nodes.put(1, updated)}

Records in sets (messages, events)

集合中的记录（消息、事件）

quint

var inFlight: Set[Message]

action send(src: int, dst: int, r: int, p: str): bool = all {
  inFlight' = inFlight.union(Set({ from: src, to: dst, round: r, payload: p })),
  // ...
}

// Filter by field:
inFlight.filter(m => m.to == nodeId)
inFlight.exists(m => m.round == currentRound and m.payload == "vote")

quint

var inFlight: Set[Message]

action send(src: int, dst: int, r: int, p: str): bool = all {
  inFlight' = inFlight.union(Set({ from: src, to: dst, round: r, payload: p })),
  // ...
}

// 按字段过滤:
inFlight.filter(m => m.to == nodeId)
inFlight.exists(m => m.round == currentRound and m.payload == "vote")

Sum types

求和类型

Sum types (variants) represent a value that can be one of several distinct cases.

quint

type Action =
  | Propose({ value: int, proposer: int })
  | Vote({ value: int, voter: int })
  | Decide({ value: int })

Each variant has a named constructor and carries one payload. A constructor takes exactly one argument — wrap multiple fields in a record (as above) or a tuple.

Construct a value by calling the constructor:

quint

val a: Action = Propose({ value: 1, proposer: 2 })

Pattern-match with

match

, binding the payload:

quint

pure def describeAction(a: Action): str =
  match a {
    | Propose(p) => "proposal"
    | Vote(v)    => "vote"
    | Decide(d)  => "decision"
  }

Use

to ignore the payload when you only care which variant it is:

quint

match a {
  | Propose(_) => "proposal"
  | _          => "other"
}

Use sum types when a message, event, or state can take structurally different forms — not just different values of the same type.

求和类型（变体）表示可以是几种不同情况之一的值。

quint

type Action =
  | Propose({ value: int, proposer: int })
  | Vote({ value: int, voter: int })
  | Decide({ value: int })

每个变体都有一个命名构造函数，并携带一个负载。构造函数恰好接受一个参数——将多个字段包装在记录（如上）或元组中。

调用构造函数创建值：

quint

val a: Action = Propose({ value: 1, proposer: 2 })

使用

match

进行模式匹配，绑定负载：

quint

pure def describeAction(a: Action): str =
  match a {
    | Propose(p) => "proposal"
    | Vote(v)    => "vote"
    | Decide(d)  => "decision"
  }

当仅关心变体类型而忽略负载时，使用

：

quint

match a {
  | Propose(_) => "proposal"
  | _          => "other"
}

当消息、事件或状态可以采用结构不同的形式（而不仅仅是同一类型的不同值）时，使用求和类型。

Enum types

枚举类型

Enum types are a special case of sum types where each case has no additional data.

quint

type Phase = Idle | Propose | Vote | Commit
var phase: Phase

if (phase == Propose) { ... }

枚举类型是求和类型的特殊情况，每个情况没有额外数据。

quint

type Phase = Idle | Propose | Vote | Commit
var phase: Phase

if (phase == Propose) { ... }

Variable grouping — decision guide

变量分组决策指南

Before writing

var

declarations, answer these questions for each candidate group:

Question	Group → record if...	Keep flat if...
Do these vars always change together?	Yes, in most actions	No, they're independent
Do they describe the same entity?	Same node / same message / same round	Different concerns
Is there one instance or N instances?	Either one or N (group if cohesive; for N use `Id -> RecordType` )	Flat only when concerns are truly independent
Do invariants relate them?	Invariant spans multiple fields of one entity	Invariant uses vars independently

编写

var

声明前，针对每个候选分组回答以下问题：

问题	分组为记录的情况...	保持扁平的情况...
这些变量是否总是一起变化？	是，在大多数动作中	否，它们相互独立
它们是否描述同一实体？	同一节点/同一消息/同一轮次	不同关注点
是单个实例还是N个实例？	单个或N个（内聚则分组；N个实例使用 `Id -> RecordType` ）	仅当关注点真正独立时保持扁平
不变量是否关联它们？	不变量涉及同一实体的多个字段	不变量独立使用变量

Boolean operators

布尔运算符

quint

not(p)             // negation — Quint has no ! operator
p and q            // conjunction
p or q             // disjunction
p implies q        // p => q  (not(p) or q)
p iff q            // p == q for booleans

and { p1, p2, p3 } // block form — equivalent to p1 and p2 and p3
or  { p1, p2, p3 } // block form — at least one must hold

and { }

and

or { }

are the same operators as

all { }

and

any { }

in actions — use whichever reads more naturally in context.

quint

not(p)             // 否定——Quint没有!运算符
p and q            // 合取
p or q             // 析取
p implies q        // p => q  (not(p) or q)
p iff q            // 布尔值的等价性

and { p1, p2, p3 } // 块形式——等价于p1 and p2 and p3
or  { p1, p2, p3 } // 块形式——至少一个必须成立

and { }

和

or { }

与动作中的

all { }

和

any { }

是相同的运算符——根据上下文选择可读性更高的写法。

Invariants and temporal properties

不变量与时态属性

quint

// Safety invariant — must hold in every reachable state
// @invariant
val noDuplicateLeader: bool =
  leaders.size() <= 1

// Temporal property — evaluated over traces
// @temporal
temporal eventualProgress: bool =
  eventually(committed.size() > 0)

// Temporal operators
eventually(p)      // p holds in some future state
always(p)          // p holds in all future states
p.implies(q)       // p => q

quint

// 安全不变量——必须在所有可达状态中成立
// @invariant
val noDuplicateLeader: bool =
  leaders.size() <= 1

// 时态属性——在轨迹上评估
// @temporal
temporal eventualProgress: bool =
  eventually(committed.size() > 0)

// 时态运算符
eventually(p)      // p在某个未来状态成立
always(p)          // p在所有未来状态成立
p.implies(q)       // p => q

Assume

quint

assume nodeCountPositive = N > 0
assume quorumMajority = 2 * quorum > N

assume

states a premise about constants, but it is not enforced — a violated

assume

is silently ignored by

quint typecheck

quint run

, and

quint verify

(none of them flags it). It is documentation, not a checked constraint. To actually check a condition on constants, write a

run

test that asserts it (it executes and fails when the condition is false):

quint

run quorumAssumptionTest = all {
  2 * quorum > N,
  N > 0,
}

Run it with

quint test

; the test fails (reporting which conjunct broke) if a constant assignment violates the condition.

quint

assume nodeCountPositive = N > 0
assume quorumMajority = 2 * quorum > N

assume

声明关于常量的前提，但它不被强制执行——违反的

assume

会被

quint typecheck

、

quint run

和

quint verify

静默忽略（这些工具都不会标记它）。它是文档，而非受检查的约束。要实际检查常量的条件，请编写断言该条件的

run

测试（条件为假时会执行并失败）：

quint

run quorumAssumptionTest = all {
  2 * quorum > N,
  N > 0,
}

使用

quint test

运行它；如果常量赋值违反条件，测试会失败（报告哪个合取项不成立）。

Conditional and let

条件语句与let

quint

if (x > 0) "positive" else "non-positive"

val result = {
  val doubled = x * 2
  doubled + 1
}

quint

if (x > 0) "positive" else "non-positive"

val result = {
  val doubled = x * 2
  doubled + 1
}

REPL usage

REPL使用

Prefer CLI commands (

quint typecheck

quint run

quint test

quint verify

) for all validation and execution tasks. Open the REPL (

quint

quint -r spec.qnt::ModuleName

) only when you need expression-level interaction the CLI does not provide.

Type inspection:

>>> :type myExpression

所有验证和执行任务优先使用CLI命令（

quint typecheck

、

quint run

、

quint test

、

quint verify

）。仅当需要CLI不支持的表达式级交互时，才打开REPL（

quint

或

quint -r spec.qnt::ModuleName

）。

类型检查：

>>> :type myExpression

File layout

文件布局

Split specs across two files:

<protocol-name>.qnt        # main module — step, init, vars, invariants
<protocol-name>_test.qnt   # test module — run tests and scenario witnesses (imports main)

将规范拆分为两个文件：

<protocol-name>.qnt        // 主模块——step、init、变量、不变量
<protocol-name>_test.qnt   // 测试模块——运行测试和场景见证（导入主模块）

Module responsibilities

模块职责

Main module (

<protocol-name>.qnt

Declares all state variables,
```
init
```
, actions, and safety invariants
step
must live in the main module — it is the entry point for
```
quint run
```
simulation
The module name matches the file stem:
```
module myProtocol
```
in
```
myProtocol.qnt
```

Test module (

<protocol-name>_test.qnt

Imports the main module (
```
import myProtocol.*
```
)
Contains
```
run
```
tests and scenario witnesses invoked via
```
quint test
```
or
```
quint run
```
Inherits
```
step
```
from the main module through the import

主模块（

<protocol-name>.qnt

）：

声明所有状态变量、
```
init
```
、动作和安全不变量
step
必须位于主模块中——它是
```
quint run
```
模拟的入口点
模块名称与文件名匹配：
```
myProtocol.qnt
```
中对应
```
module myProtocol
```

测试模块（

<protocol-name>_test.qnt

）：

导入主模块（
```
import myProtocol.*
```
）
包含通过
```
quint test
```
或
```
quint run
```
调用的
```
run
```
测试和场景见证
通过导入继承主模块的
```
step
```

Which

--main

to pass for

quint run

quint run

应传入哪个

--main

参数

quint run

must receive the module that owns the property being checked:

Property location	Correct `--main`
Invariant defined in main module	main module name
Witness / `run` test defined in test module	test module name (it imports `step` from main)

The primitive's

module_name

field (set during indexing) always holds the correct value. Use it directly — do not derive from the filename.

quint run

必须接收拥有待检查属性的模块：

属性位置	正确的 `--main` 参数
主模块中定义的不变量	主模块名称
测试模块中定义的见证/ `run` 测试	测试模块名称（它从主模块导入 `step` ）

原语的

module_name

字段（索引时设置）始终保存正确值。直接使用该值——不要从文件名推导。

Basic spells

基础工具集（basicSpells）

Many useful operators are not built into Quint but are available in

basicSpells.qnt

, a standard library shipped with most Quint projects. Import it with:

quint

import basicSpells.* from "./basicSpells"

Key definitions it provides:

Definition	What it does
`type Option[a] = Some(a) \| None`	The option type — Quint has no built-in `Option` . Any spec field typed `Option[T]` depends on this import.
`unwrap(o)`	The value inside `Some` ; undefined on `None`
`require(cond)`	Blocks the action if `cond` is false (cleaner than bare `all { cond, ... }` )
`values(m)`	Set of all values in map `m`
`transformValues(m, f)`	New map with `f` applied to every value
`has(m, key)`	True if `key` is bound in `m`
`getOrElse(m, key, default)`	`m.get(key)` if present, otherwise `default`
`mapRemove(m, key)` / `mapRemoveAll(m, ks)`	Copy of `m` without `key` (or without the set of keys `ks` )
`setRemove(s, e)` / `setAdd(s, e)`	Copy of set `s` without / with element `e`
`find(s, f)` / `findFirst(l, f)`	First element of set / list satisfying `f` , as `Option`
`max(i, j)` / `min(i, j)` / `abs(i)`	Max / min of two integers; absolute value

When you see a spec using

Option

require

values

, or

transformValues

without an import, it is relying on basicSpells — check whether the project includes it. (Less common operators live in a sibling

rareSpells.qnt

许多实用运算符并非Quint内置，但可在

basicSpells.qnt

中获取，这是随大多数Quint项目分发的标准库。通过以下方式导入：

quint

import basicSpells.* from "./basicSpells"

它提供的核心定义：

定义	功能
`type Option[a] = Some(a) \| None`	可选类型——Quint没有内置 `Option` 。任何类型为 `Option[T]` 的规范字段都依赖此导入。
`unwrap(o)`	`Some` 内部的值； `None` 时未定义
`require(cond)`	如果 `cond` 为假则阻止动作（比裸 `all { cond, ... }` 更简洁）
`values(m)`	映射 `m` 中所有值的集合
`transformValues(m, f)`	将 `f` 应用于每个值后的新映射
`has(m, key)`	如果 `key` 在 `m` 中已绑定则为真
`getOrElse(m, key, default)`	存在则返回 `m.get(key)` ，否则返回 `default`
`mapRemove(m, key)` / `mapRemoveAll(m, ks)`	移除 `key` （或移除键集合 `ks` ）后的 `m` 副本
`setRemove(s, e)` / `setAdd(s, e)`	移除/添加元素 `e` 后的集合 `s` 副本
`find(s, f)` / `findFirst(l, f)`	集合/列表中第一个满足 `f` 的元素，返回 `Option` 类型
`max(i, j)` / `min(i, j)` / `abs(i)`	两个整数的最大值/最小值；绝对值

当看到规范使用

Option

、

require

、

values

或

transformValues

但未导入时，它依赖于basicSpells——检查项目是否包含该库。（不太常用的运算符位于同级的

rareSpells.qnt

中。）

Guidelines

指南

Detailed references — read these when you need more than the quick reference above:

File	Contents
`guidelines/operators.md`	Complete operator reference: extended set/list/map operators, `run` / `then` / `expect` / `reps` for tests and witnesses, temporal fairness, `q::debug`
`guidelines/simulations.md`	Witnesses vs invariants, result interpretation, progressive increase protocol, trace analysis, coverage standard
`guidelines/constraints.md`	Hard language limitations: no string ops, no nested match, no destructuring, no loops, no early returns
`guidelines/cli.md`	Full CLI reference: `quint run` , `quint test` , `quint verify` flags, verbosity guide, reading output
`guidelines/patterns.md`	14 core patterns: State Type, Pure Functions, Thin Actions, Map Pre-population, Syntax Rules, Undefined Behavior, Witnesses, Nondeterministic Testing, Separate Test Files, REPL-First Debugging, Separate Concerns First, Extract System Model, Types-First Scaffolding, Logic Stubs
`guidelines/tests.md`	Writing and debugging tests: `run` / `then` / `expect` / `reps` / `fail` , nondeterministic tests, error location ≠ failure point, frame counting, REPL-first debugging
`guidelines/choreo.md`	Choreo framework for distributed protocols: two-file split, `choreo::cue` pattern, `.with_cue().perform()` testing, witness-based test discovery

详细参考资料——当需要超出上述快速参考的内容时阅读：

文件	内容
`guidelines/operators.md`	完整运算符参考：扩展的集合/列表/映射运算符、测试和见证用的 `run` / `then` / `expect` / `reps` 、时态公平性、 `q::debug`
`guidelines/simulations.md`	见证与不变量的对比、结果解读、渐进式协议、轨迹分析、覆盖标准
`guidelines/constraints.md`	语言硬限制：无字符串操作、无嵌套match、无解构、无循环、无提前返回
`guidelines/cli.md`	完整CLI参考： `quint run` 、 `quint test` 、 `quint verify` 的标志、详细程度指南、输出解读
`guidelines/patterns.md`	14个核心模式：状态类型、纯函数、轻量动作、映射预填充、语法规则、未定义行为、见证、非确定性测试、分离测试文件、REPL优先调试、优先分离关注点、提取系统模型、类型优先脚手架、逻辑存根
`guidelines/tests.md`	测试编写与调试： `run` / `then` / `expect` / `reps` / `fail` 、非确定性测试、错误位置≠失败点、帧计数、REPL优先调试
`guidelines/choreo.md`	分布式协议的Choreo框架：双文件拆分、 `choreo::cue` 模式、 `.with_cue().perform()` 测试、基于见证的测试发现

quint-lang

Original

Translation

Quint Language Reference

Quint语言参考手册

Module structure

模块结构

Types

类型

Definitions

定义

State variables

状态变量

Actions

动作

Non-determinism

非确定性

Set operators

集合运算符

List operators

列表运算符

Map operators

映射运算符

Records

记录

Type aliases for records

记录的类型别名

Creating and accessing

创建与访问

Updating (immutable — returns a new record)

更新（不可变——返回新记录）

Records as state — when to group variables

作为状态的记录——何时分组变量

Example: preferred grouped local state vs. anti-pattern

示例：推荐的分组本地状态 vs 反模式

Nested records

嵌套记录

Records in sets (messages, events)

集合中的记录（消息、事件）

Sum types

求和类型

Enum types

枚举类型

Variable grouping — decision guide

变量分组决策指南

Boolean operators

布尔运算符

Invariants and temporal properties

不变量与时态属性

Assume

Assume

Conditional and let

条件语句与let

REPL usage

REPL使用

File layout

文件布局

Module responsibilities

模块职责

Which --main to pass for quint run

quint run应传入哪个--main参数

Basic spells

基础工具集（basicSpells）

Guidelines

指南

Which
`--main`
to pass for
`quint run`

`quint run`
应传入哪个
`--main`
参数