Back to Details

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

类型

TypeDescriptionExample
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
vs 
pure val
: 
const
is a module parameter bound at instantiation (
import A(N = 3)
); 
pure val
is a fixed expression computed once. 
def
vs 
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:
QuestionGroup → record if...Keep flat if...
Do these vars always change together?Yes, in most actionsNo, they're independent
Do they describe the same entity?Same node / same message / same roundDifferent 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 entityInvariant 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

Assume

quint
assume nodeCountPositive = N > 0
assume quorumMajority = 2 * quorum > N
An 
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
or 
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 locationCorrect 
--main
Invariant defined in main modulemain 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:
DefinitionWhat 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:
FileContents
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()
测试、基于见证的测试发现