Quint

https://quint.sh/docs
Admin
Quint is a modern specification language used to describe executable models and properties, which...
Tokens:79,465
Snippets:1,100
Trust Score:5.8
Update:2 months ago
Show doc for...
Tokens:
Raw
### Module Instance Example

Source: https://quint.sh/docs/lang

Example of creating a module instance and accessing its members.

```text
// An instance of Voting:
//  - It copies all definitions of Voting into a new namespace V
//  - It replaces Value with Set(0, 1)
import Voting(Value = Set(0, 1)) as V
 
// the names of V are accessed via "::"
val MyValues = V::Value
```

--------------------------------

### Execute exponentiation examples

Source: https://quint.sh/docs/lessons/integers

Examples of running exponentiation operations using the quint command-line tool.

```bash
quint "2^32"
```

```bash
quint "2^64"
```

```bash
quint "2^256"
```

```bash
quint "2^512"
```

--------------------------------

### Execute integer comparison examples

Source: https://quint.sh/docs/lessons/integers

Command-line examples for testing integer comparison logic.

```bash
quint "10 < 11"
```

```bash
quint "10 < 10"
```

```bash
quint "10 <= 11"
```

```bash
quint "10 <= 10"
```

```bash
quint "10 <= 9"
```

```bash
quint "11 > 10"
```

```bash
quint "10 > 10"
```

```bash
quint "11 >= 10"
```

```bash
quint "10 >= 10"
```

```bash
quint "10 >= 9"
```

```bash
quint "10 == 10"
```

```bash
quint "10 == 11"
```

```bash
quint "10 != 10"
```

```bash
quint "10 != 11"
```

--------------------------------

### Install Quint via Homebrew

Source: https://quint.sh/docs/getting-started

Installs the Quint binary using the Homebrew package manager.

```bash
brew install quint
```

--------------------------------

### Example of module instantiation syntax

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Demonstrates the current syntax for creating module instances.

```quint
module general {
  module I3 = general(N = 3)
  module I5 = general(N = 5)
  ...
}
```

--------------------------------

### Execute integer negation examples

Source: https://quint.sh/docs/lessons/integers

Command-line examples for testing integer negation.

```bash
quint "-(3 + 2)"
```

```bash
quint "-(-2^63) == 2^63"
```

--------------------------------

### Define module instances

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of creating fixed-size instances of a module.

```Quint
module fixed {
  module I3 = general(N = 3)
  module I5 = general(N = 5)
 
  action init3 = I3::init
  action init5 = I5::init
 
  import I3.*
}
```

--------------------------------

### Launch the Quint REPL

Source: https://quint.sh/docs/repl

Execute this command in the terminal to start the interactive environment.

```bash
$ quint
```

--------------------------------

### Simulator OK Output Example

Source: https://quint.sh/docs/simulator

Example output when the simulator completes without finding any invariant violations.

```text
Running... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 9999/10000 samples
An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> 0, "bob" -> 37, "charlie" -> 0) }
 
[State 2] { balances: Map("alice" -> 0, "bob" -> 79, "charlie" -> 0) }
 
[State 3] { balances: Map("alice" -> 0, "bob" -> 3, "charlie" -> 0) }
 
[State 4] { balances: Map("alice" -> 0, "bob" -> 90, "charlie" -> 0) }
 
[State 5] { balances: Map("alice" -> 0, "bob" -> 90, "charlie" -> 79) }
 
[ok] No violation found (2459ms).
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xe924b0166c3c5 to reproduce.
```

--------------------------------

### Execute reachability queries

Source: https://quint.sh/docs/lessons/sets

Command-line examples for running the reachability function with different swap counts.

```bash
quint -r sets.qnt::sets 'buyableNSwaps(Set("ATOM"), 3)'
```

```bash
quint -r sets.qnt::sets 'buyableNSwaps(Set("ATOM"), 4)'
```

```bash
quint -r sets.qnt::sets 'buyableNSwaps(Set("ATOM"), 5)'
```

--------------------------------

### Rust Pattern Matching Example

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Provides a reference example of Rust's match syntax for comparison.

```rust

match x {
    A    => println!("a"),
    B    => println!("b"),
    C(v) => println!("cv"),
    _    => println!("anything"),
}
```

--------------------------------

### Define module names and operators

Source: https://quint.sh/docs/lang

Example demonstrating constants, variables, and operator definitions within a module.

```quint

module names {
  const acceleration: int
  var clock: int
 
  pure def myMul(i, j) = i * j
 
  pure def sqr(i) = myMul(i, i)
 
  val distance = acceleration * sqr(clock)
 
  action init = {
    clock' = 0
  }
 
  action next = {
    clock' = clock + 1
  }
}
```

--------------------------------

### Implement module instance usage

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example usage of the proposed module instance syntax within a module definition.

```text
module fixed {
  import general(N = 3).*
  import general(N = 5) as I5
  import statelessModule as M
  ...
}
```

--------------------------------

### Task Result Examples

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr001-transpiler-architecture

Examples of error and success responses returned by task handlers.

```json
{
  "result": "error",
  "messages": [ { "explanation": "QNT404: Module MyModule not found", ...} ]
}
```

```json
{ "result": "OK" }
```

--------------------------------

### Install Quint via NPM

Source: https://quint.sh/docs/getting-started

Installs the Quint package globally using the Node Package Manager.

```bash
npm i @informalsystems/quint -g
```

--------------------------------

### Injection syntax comparison

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Example of injection syntax as defined in Leijen05.

```text
<l = i> :: ∀αr . α → <l :: α | r > -- injection
```

--------------------------------

### Example of rewritten export statement

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr007-flattening

This example shows the recommended way to rewrite an export statement to avoid unsupported namespace changes.

```quint
module A {
  const N: int
  val a = N
}
 
module B {
  import A(N=1) as A1
  export A1
}
```

--------------------------------

### Invoke Quint REPL

Source: https://quint.sh/docs/quint

Commands to start the interactive Read-Evaluate-Print-Loop.

```bash
$ quint
```

```bash
$ quint repl --help
quint repl
 
run an interactive Read-Evaluate-Print-Loop
 
Options:
      --help     Show help                                             [boolean]
      --version  Show version number                                   [boolean]
  -r, --require  filename[::module]. Preload the file and, optionally, import
                 the module                                             [string]
      --verbosity  control how much output is produced (0 to 5)
                                                           [number] [default: 2]
      --seed       random seed to use for non-deterministic choice      [string]
      --backend    the backend to use for evaluation
                [string] [choices: "typescript", "rust"] [default: "typescript"]
```

```bash
quint repl
```

--------------------------------

### quint repl

Source: https://quint.sh/docs/quint

Starts an interactive Read-Evaluate-Print-Loop for the Quint language.

```APIDOC
## quint repl

### Description
Starts an interactive Read-Evaluate-Print-Loop (REPL) for learning and testing Quint specifications.

### Options
- **--require** (string) - Optional - Preload a file and optionally import a module.
- **--verbosity** (number) - Optional - Control output detail (0 to 5, default: 2).
- **--seed** (string) - Optional - Random seed for non-deterministic choice.
- **--backend** (string) - Optional - Backend for evaluation ("typescript" or "rust", default: "typescript").
```

--------------------------------

### Define modules and imports

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of encapsulating definitions in a module and importing them into another.

```Quint
module fun {
  pure def dec(i) = i - 1
  pure def inc(i) = i + 1
}
 
module general {
  import fun.*
 
  // to be defined later
<<<definitions>>>
}
```

--------------------------------

### Configure Vim for Quint

Source: https://quint.sh/docs/getting-started

Installs the language server and configures Neovim for syntax highlighting and LSP integration.

```bash
npm i @informalsystems/quint-language-server -g
```

```vim
autocmd FileType quint lua vim.lsp.start({name = 'quint', cmd = {'quint-language-server', '--stdio'}, root_dir = vim.fs.dirname()})
au BufRead,BufNewFile *.qnt  setfiletype quint
au BufNewFile,BufReadPost *.qnt runtime syntax/quint.vim
```

--------------------------------

### Example of Quint modules with instances

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr007-flattening

Initial state of modules A, B, and C where A is instanced twice with different overrides.

```quint

module A {
  const N: int // id 1
  val a = N // id 2
}
 
module B {
  import A(N=1) as A1
  val b = A1::a // id 3
}
 
module C {
  import A(N=0) as A1
  val C = A1::a // id 4
}
```

--------------------------------

### Launch Quint REPL for Choreo

Source: https://quint.sh/docs/choreo/tutorial

Start the Quint REPL to interact with a specific Choreo specification file.

```bash
quint -r two_phase_commit.qnt::two_phase_commit
```

--------------------------------

### Define an initialization action

Source: https://quint.sh/docs/lessons/hello

Uses the all operator to assign initial values to state variables, transitioning the machine to a starting state.

```quint

 
    // initialize the state machine that captures the protocol
    action init = all {
      consoleOutput' = "",
      readByUser' = ""
    }
```

--------------------------------

### Rust Construction Syntax

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Examples of constructing instances of Rust structs and enums.

```rust
let s = Either::Left(4)
let p = Pair{
    fst: 4,
    snd: "Two"
}
```

--------------------------------

### Define a general module

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of a module importing another module and defining constants and actions.

```quint
module general {
  import fun.*
 
  const N: int
  var x: int
 
  action init = { x' = N }
  action step = { x' = dec(x) }
}
```

--------------------------------

### Solidity constructor example

Source: https://quint.sh/docs/lessons/coin

Standard Solidity constructor that sets the minter to the message sender.

```Solidity
// in Solidity
constructor() {
    minter = msg.sender;
}
```

--------------------------------

### Evaluate integer division and remainder expressions

Source: https://quint.sh/docs/lessons/integers

Examples demonstrating integer division and remainder calculations.

```quint
quint "99 / 2 == 49"
```

```quint
quint "99 % 2 == 1"
```

```quint
quint "98 % 2 == 0"
```

```quint
quint "((2^64 - 1) % 2^64 + 1) % 2^64"
```

```quint
quint "(2^64 - 123) % 2^63"
```

--------------------------------

### Constructing Records

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Examples of creating records using standard syntax and the Rec operator.

```quint
val n : int = 1
val s : str = "one"
val ex : {a : int, b : str} = {a : n, b : s}
// Or, using our exotic Rec operator, which is currently the normal form
val ex_ : {a : int, b : str} = Rec("a", n, "b", s)
```

--------------------------------

### Decomposition syntax comparison

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Example of decomposition syntax as defined in Leijen05.

```text
(l ∈ _ ? _ : _) :: ∀αβr . <l :: α | r> → (α → β) → (<r> → β) → β -- decomposition
```

--------------------------------

### Define constants, variables, and actions

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of defining state machine components within a module.

```Quint
  const N: int
  var x: int
 
  action init = { x' = N }
  action step = { x' = dec(x) }
```

--------------------------------

### Example Specification with then Operator

Source: https://quint.sh/docs/lang

Demonstrates using then to chain actions in a module, showing both concrete value assignments and action-based transitions.

```Quint
module counters {
  var n: int
 
  action Init = {
    n' = 1
  }
 
  action Even = all {
    n % 2 == 0,
    n' = n / 2,
  }
 
  action ByThree = all {
    n % 3 == 0,
    n' = 2 * n
  }
 
  action Positive = all {
    n > 0,
    n' = n + 1,
  }
 
  action Next = any {
    Even, ByThree, Positive
  }
 
  run run1 = (n' = 1).then(n' = 2).then(n' = 3).then(n' = 6).then(n' = 3)
 
  run run2 = (Init).then(Positive).then(Positive).then(ByThree).then(Even)
 
  run run3 = (Init).then(Next).then(Next).then(Next).then(Next)
}
```

--------------------------------

### Install Quint via Nix

Source: https://quint.sh/docs/getting-started

Provides commands to run Quint in a temporary shell or add it to the user profile.

```bash
nix shell "github:NixOS/nixpkgs#quint"
```

```bash
nix profile add "github:NixOS/nixpkgs#quint"
```

--------------------------------

### Example of unsupported export namespace change

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr007-flattening

This example demonstrates an export statement that attempts to remove namespaces, which is currently unsupported in the flattening process.

```quint
module A {
  const N: int
  val a = N
}
 
module B {
  import A(N=1) as A1
  export A1.*
}
```

--------------------------------

### Evaluate expressions in REPL

Source: https://quint.sh/docs/repl

Basic examples of entering expressions into the REPL to receive immediate evaluation results.

```Quint

>>> 1 + 3
4
```

```Quint

>>> Set(1, 2, 3).map(i => i * 2)
Set(2, 4, 6)
```

--------------------------------

### Flattened module structure

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of how a module is transformed after the flattening stage.

```quint
module fixed {
  // the instance general(N = 3)
 
  // this is how `import fun.*` is transformed
  import fun as I3
 
  val I3::N = 3
  var I3::x: int
 
  action I3::init = { I3::x' = I3::N }
  action I3::step = { I3::x' = I3::dec(x) }
 
  // the instance general(N = 5)
 
  // this is how `import fun.*` is transformed
  import fun.* as I5
 
  val I5::N = 3
  var I5::x: int
 
  action I5::init = { I5::x' = I5::N }
  action I5::step = { I5::x' = I5::dec(x) }
 
  // import I3.* is not allowed, see Section 4.3
}
```

--------------------------------

### Check action enablement

Source: https://quint.sh/docs/builtin

Examples demonstrating the enabled operator to verify action preconditions and satisfiability.

```TLA+

var x: int
action Init = x' = 0
action Under10 = all {
  x < 10,
  x' = x + 1,
}
action Over10 = all {
  x >= 10,
  x' = x + 1,
}
temporal Property = always(and {
  enabled(Under10) iff x < 10,
  enabled(Over10) iff x >=10,
})
```

```TLA+

var x: int
action Init = x' = 0
action impossible = {
  nondet i = Set().oneOf()
  x' = i
}
temporal Property = always(not(enabled(impossible)))
```

--------------------------------

### Execute exponentiation edge cases

Source: https://quint.sh/docs/lessons/integers

Examples demonstrating behavior with negative bases, negative exponents, and zero.

```bash
quint "(-2)^3"
```

```bash
quint "(-2)^4"
```

```bash
quint "2^(-4)"
```

```bash
quint "0^3"
```

```bash
quint "0^0"
```

```bash
quint "0^(-2)"
```

--------------------------------

### Example fold calculation

Source: https://quint.sh/docs/lessons/coin

Shows the expansion of the fold operation over a set of addresses.

```quint
 ((((0 + balances.get("null")) + balances.get("alice")) + balances.get("bob"))
   + balances.get("charlie")) + balances.get("eve")
```

--------------------------------

### TLC configuration example

Source: https://quint.sh/docs/quint

A JSON configuration file for tuning TLC runtime parameters such as heap size and worker count.

```json
{
  "maxHeap": "-Xmx8G",
  "stackSize": "-Xss515m",
  "workers": "auto"
}
```

--------------------------------

### Evaluate integer addition expressions

Source: https://quint.sh/docs/lessons/integers

Examples of adding integers and verifying commutativity and associativity laws.

```quint
quint "2022 + 2023"
```

```quint
quint "11 + 17 == 17 + 11"
```

```quint
quint "(11 + 17) + 19 == 11 + (17 + 19)"
```

--------------------------------

### Tuple unpacking in lambdas

Source: https://quint.sh/docs/lang

Example showing how tuple unpacking is desugared in single-argument lambda expressions.

```quint

(t =>
  val x = t._1
  val y = t._2
  e2
)
```

--------------------------------

### Implement a Tendermint proposal cue

Source: https://quint.sh/docs/choreo/cue-pattern

Example of invoking the cue pattern within a main listener to handle proposal messages.

```choreo
// In the main listener
choreo::cue(ctx, listen_proposal_in_propose, broadcast_prevote_for_proposal)
```

--------------------------------

### Initialize Local and Global State

Source: https://quint.sh/docs/choreo/tutorial

Defines the initial state for nodes and the system, assigning roles and starting stages.

```Quint
   // =============================================================================
   // INITIALIZATION
   // =============================================================================
 
-  // TODO: Define how to initialize each process's local state
   pure def initialize(n: Node): LocalState = {
     {
       process_id: n,
-      // TODO: Initialize your state fields
-      // phase: Init,
-      // value: None,
-      // round: 0,
+      role: if (n == COORDINATOR) Coordinator else Participant,
+      stage: Working,
     }
   }
 
- // TODO: Define initial global state
   action init = choreo::init({
     system: NODES.mapBy(n => initialize(n)),
-    messages: NODES.mapBy(n => Set()),  // Or add initial messages if needed
+    messages: NODES.mapBy(n => Set()),
-    events: NODES.mapBy(n => Set()),    // Or add initial events if needed
+    events: NODES.mapBy(n => Set()),
-    extensions: ()  // Or initialize your extensions
+    extensions: ()
   })
```

--------------------------------

### Example REPL Execution Sequence

Source: https://quint.sh/docs/development-docs/stories/story008-repl-traces

A sequence of commands executed in the REPL to reach a specific protocol state.

```text
>>> init
true
>>> pressButton
true
>>> heat
true
>>> depressButton
true
```

--------------------------------

### Simulator output for witness check

Source: https://quint.sh/docs/checking-properties

Example output showing the percentage of traces where the witness property was satisfied.

```text
[ok] No violation found (599ms).
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Witnesses:
alice_more_than_bob was witnessed in 7094 trace(s) out of 10000 explored (70.94%)
Use --seed=0x1c8a2137939c73 to reproduce.
```

--------------------------------

### Initialize Quint REPL Session

Source: https://quint.sh/docs/development-docs/stories/story008-repl-traces

Navigate to the tutorial directory and launch the Quint REPL to begin a session.

```bash
$ cd ./tutorials/repl
$ quint
Quint REPL 0.9.1
Type ".exit" to exit, or ".help" for more information
>>> import kettle.* from "./kettle"
```

--------------------------------

### View REPL startup output

Source: https://quint.sh/docs/repl

The expected output upon successfully launching the Quint REPL.

```text
Quint REPL vN.N.N
Type ".exit" to exit, or ".help" for more information
>>>
```

--------------------------------

### Simulator Violation Output Example

Source: https://quint.sh/docs/simulator

Example output when the simulator identifies an invariant violation and provides a counter-example.

```text
An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> -63, "bob" -> 0, "charlie" -> 0) }
 
[violation] Found an issue (44ms).
Use --seed=0x4e85b3a53f7ef to reproduce.
Use --verbosity=3 to show executions.
error: Invariant violated
```

--------------------------------

### Execute non-deterministic initialization

Source: https://quint.sh/docs/repl

Demonstrates the execution of the non-deterministic initialization action in the REPL.

```Quint
>>> initNondet
true
```

--------------------------------

### Operator Effect Signature Example

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

Example signature for the addition operator showing how entity variables are used to combine effects.

```Quint
iadd: (Read[r1] & Temporal[t1]) => (Read[r2] & Temporal[t2]) => Read[r1, r2] & Temporal[t1, t2]
```

--------------------------------

### get

Source: https://quint.sh/docs/builtin

Retrieves the value associated with a key in a map.

```APIDOC
## get

### Signature
`pure def get: ((a -> b), a) => b`

### Description
Returns the value for a given key in the map. Behavior is undefined if the key is not present.
```

--------------------------------

### Defining Operators

Source: https://quint.sh/docs/lang

Examples of various operator definitions including pure values, functions, stateful variables, actions, and temporal formulas.

```text
// a static constant value, which is not changing over time
pure val Nodes: Set[int] = 1.to(10)
 
// a two-argument operator that returns its first argument, independent of state
pure def fst(x: a, y: b): a =
    x
 
// the maximum operator
pure def max(x: int, y: int): int =
    if (x > y) x else y
 
// A definition over `x` that returns a Boolean result.
// In logic, such definition is usually called a predicate.
pure def isPositive(x: int): bool =
    x > 0
 
// a higher-order operator that accepts another operator as its first argument
pure def F(G: a => b, x: a): b = G(x)
 
// introduce a variable to define stateful definitions
var timer: int
 
// a value that depends on the state (the variable timer) and may change over time
val isTimerPositive =
    timer >= 0
 
// an operator definition that depends on the state and may change over time
def hasExpired(timestamp: int): bool =
    timer >= timestamp
 
// an initialization action that assigns initial values to the state variables
action init =
  timer' = 0
 
// an action that updates the value of the state variable timer
action advance(unit: int): bool =
    // a delayed assignment (see below in the manual)
    timer' = timer + unit
 
// a temporal formula that ensures that the timer variable never goes negative
temporal neverNegative =
    always(timer >= 0)
```

--------------------------------

### Execute Initialization in REPL

Source: https://quint.sh/docs/lessons/coin

Command to run the init action and evaluate the resulting state.

```bash

quint -r coin.qnt::coin "init" "state"
```

--------------------------------

### Import Choreo Abstractions

Source: https://quint.sh/docs/choreo

Initialize the Choreo framework by importing it with the required number of processes.

```Quint
import choreo(processes = NODES) as choreo from "./choreo"
```

--------------------------------

### Initialize Protocol State

Source: https://quint.sh/docs/development-docs/stories/story008-repl-traces

Execute the initialization command within the REPL.

```quint
>>> init
true
```

--------------------------------

### Reference TLA+ LOCAL

Source: https://quint.sh/docs/lang

Example of TLA+ syntax for local operator definitions.

```tla
------ MODULE Local ------
VARIABLE y
LOCAL F(x) == { x, y }
G(x) == { F(x) }
==========================
```

--------------------------------

### Apply initialization action

Source: https://quint.sh/docs/repl

Execute the defined action to update the state machine.

```text

>>> init
true
```

--------------------------------

### Execute kettle actions in REPL

Source: https://quint.sh/docs/repl

Demonstrates a sequence of actions to heat the kettle and turn it off, followed by inspecting the resulting state.

```quint

>>> init
true
>>> pressButton
true
>>> heat
true
>>> depressButton
true
>>> kettleState
{ beeping: false, heatingOn: false, temperature: 21 }
```

--------------------------------

### Haskell Datatype Definition

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Example of a Haskell datatype definition with field labels.

```haskell
data S = S1 { a :: Int, b :: String }
```

--------------------------------

### Defining init and step actions

Source: https://quint.sh/docs/language-basics

Shows the standard structure for defining the initial state and transition steps of a model.

```quint
var x: int
 
action init = x' = 1
 
action step = x' = x + 1
```

--------------------------------

### Define module instance syntax

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Syntax definitions for creating instances and importing names, either globally or with a prefix.

```text
  // creating an instance and importing all names introduced in the instance
  'import' name '(' [name = expr (',' name = expr)*] ')' '.' '*'
  // creating an instance and importing all names with a prefix 
  'import' name '(' [name = expr (',' name = expr)*] ')' 'as' name
```

--------------------------------

### Built-in Operator Signatures

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

Examples of signatures for general and non-general built-in operators.

```text
propagateComponents(['read', 'temporal'])(2):
  (Read[r1] & Temporal[t1], Read[r2] & Temporal[t2]) => Read[r1, r2] & Temporal[t1, t2]
```

```text
always: (Read[r] & Temporal[t]) => Temporal[r, t]
guess: (Read[r1], (Read[r1]) => Read[r2] & Update[u]) => Read[r1, r2] & Update[u]
assign: (Read[r1], Read[r2]) => Read[r2] & Update[r1]
```

--------------------------------

### Execute protocol actions in REPL

Source: https://quint.sh/docs/lessons/coin

Command to initialize the state and perform mint and send operations sequentially.

```bash
quint -r coin.qnt::coin 'init' 'mint(minter, "bob", 2023)' 'send("bob", "eve", 1024)' 'state'
```

--------------------------------

### Display quint run help

Source: https://quint.sh/docs/quint

View the available options and configuration parameters for the quint run command.

```bash
$ quint run --help
quint run <input>
 
Simulate a Quint specification and (optionally) check invariants
 
Options:
  --help         Show help                                             [boolean]
  --version      Show version number                                   [boolean]
  --out          output file (suppresses all console output)            [string]
  --main         name of the main module (by default, computed from filename)
                                                                        [string]
  --out-itf      output the trace in the Informal Trace Format to file, e.g.,
                 out_{seq}.itf.json where {seq} is the trace sequence number
                                                                        [string]
  --max-samples  the maximum number of runs to attempt before giving up
                                                       [number] [default: 10000]
  --n-traces     how many traces to generate (only affects output to out-itf)
                                                           [number] [default: 1]
  --max-steps    the maximum on the number of steps in every trace
                                                          [number] [default: 20]
  --init         name of the initializer action       [string] [default: "init"]
  --step         name of the step action              [string] [default: "step"]
  --invariants   space separated list of invariants to check (definition names).
                 When specified, all invariants are combined with AND and
                 checked together, with detailed reporting of which ones were
                 violated                                  [array] [default: []]
  --invariant    invariant to check: a definition name or an expression. Can be
                 used together with --invariants      [string] [default: "true"]
  --witnesses    space separated list of witnesses to report on (counting for
                 how many traces the witness is true)      [array] [default: []]
  --hide         space separated list of variable names to hide from the terminal
                 output (does not affect ITF output)       [array] [default: []]
  --seed         random seed to use for non-deterministic choice        [string]
  --verbosity    control how much output is produced (0 to 5)
                                                           [number] [default: 2]
  --mbt          (experimental) whether to produce metadata to be used by
                 model-based testing                  [boolean] [default: false]
  --backend      the backend to use for simulation
                [string] [choices: "typescript", "rust"] [default: "typescript"]
```

--------------------------------

### Record Projection Operation

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Example of a record projection operation using scoped labels.

```text
(_.l) :: ∀r α. (l|r) ⇒ {l :: α | r } → α
```

--------------------------------

### Execute a test in the Quint REPL

Source: https://quint.sh/docs/lessons/hello

Demonstrates loading a module and evaluating a test run within the interactive REPL environment.

```bash
$ quint -r hello.qnt
Quint REPL v0.0.3
Type ".exit" to exit, or ".help" for more information
>>> import hello.*
 
>>> writeReadTest
true
```

--------------------------------

### Represent Effect Scheme Instance

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

Example representation of an effect scheme with quantified variables.

```javascript
{
  effect: ...,
  effectVariables: new Set(['e25']),
  entityVariables: new Set(['v22']),
}
```

--------------------------------

### Represent Concrete Effect Instance

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

Example representation of a specific Read and Update effect.

```javascript
{
  kind: 'concrete',
  components: [
    { kind: 'read', entity: { kind: 'concrete', stateVariables: [{ name: 'x', reference: 1n }, { name: 'y', reference: 2n }] } },
    { kind: 'update', entity: { kind: 'variable', name: 'v' } },
  ],
}
```

--------------------------------

### View verify command help

Source: https://quint.sh/docs/quint

Displays the help menu for the quint verify command, listing all available options and flags.

```bash
$  quint verify --help
```

--------------------------------

### Initialize System Extensions

Source: https://quint.sh/docs/choreo/custom-effects-extensions

Set the initial state of the extensions during the system initialization phase.

```Choreo
pure val initial_bookkeeping = {
  evidence_propose: Set(),
  evidence_prevote: Set(),
  evidence_precommit: Set(),
}
 
action init = choreo::init({
  system: NODES.mapBy(n => initialize_process(n)),
  messages: NODES.mapBy(n => Set(initial_message).union(byzantine_messages_1)),
  events: NODES.mapBy(n => Set()),
  extensions: initial_bookkeeping  // Global state accessible by all processes
})
```

--------------------------------

### Rust Elimination Syntax

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Examples of accessing struct fields and matching on enum variants in Rust.

```rust
let two = p.snd
let four = s match {
    Either::Left(_) => 4,
    Either::Right(_) => 4
}
```

--------------------------------

### View Quint test help

Source: https://quint.sh/docs/quint

Displays the command-line options and usage information for the quint test command.

```bash
$ quint test --help
quint test <input>
 
Run tests against a Quint specification
 
Options:
  --help       Show help                                               [boolean]
  --version    Show version number                                     [boolean]
  --main       name of the main module (by default, computed from filename)
                                                                        [string]
  --out        output file (suppresses all console output)              [string]
  --max-samples  the maximum number of successful runs to try for every
                 randomized test                       [number] [default: 10000]
  --seed       random seed to use for non-deterministic choice          [string]
  --verbosity  control how much output is produced (0 to 5)[number] [default: 2]
  --match      a string or regex that selects names to use as tests     [string]
  --backend    backend to run tests [choices: "typescript", "rust"] [default: "typescript"]
```

--------------------------------

### Evaluate integer multiplication expressions

Source: https://quint.sh/docs/lessons/integers

Examples of multiplying integers and verifying commutativity and associativity laws.

```quint
quint "2^32 * 2^32 == 2^64"
```

```quint
quint "11 * 17 == 17 * 11"
```

```quint
quint "(11 * 17) * 19 == 11 * (17 * 19)"
```

--------------------------------

### Evaluate integer subtraction expressions

Source: https://quint.sh/docs/lessons/integers

Examples of subtracting integers and demonstrating left-to-right evaluation priority.

```quint
quint "2022 - 2023"
```

```quint
quint "11 + 13 - 17"
```

--------------------------------

### Import all names

Source: https://quint.sh/docs/lang

Use the * wildcard to import all names from a module.

```quint
module Math {
  def sqr(x) = x * x
  def pow(x, y) = x^y
}
 
module ImportAll {
  // import all names from Math
  import Math.*
 
  // access 'pow' and 'sqr' of Math
  def poly(x) = pow(x, 3) + sqr(x) + x
}
```

--------------------------------

### Append definitions to file

Source: https://quint.sh/docs/repl

Use four leading spaces to append definitions to the kettle.qnt file instead of evaluating them in the REPL.

```Quint

    // an example of a definition
    val isThisMyFirstDefinition = true
```

--------------------------------

### Define a Quint module

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr006-modules.lit

Example of a basic module definition containing pure function declarations.

```quint
module fun {
  pure def dec(i) = i - 1
  pure def inc(i) = i + 1
}
```

--------------------------------

### Define an action with multiple updates

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

An example of an action that attempts to update the same variable 'x' twice.

```quint
module foo {
  var x: int
 
  action bar = all {
    x' = 1,
    x' = 2,
  }
}
```

--------------------------------

### Module Instance Grammar

Source: https://quint.sh/docs/lang

The formal grammar rule for importing module instances.

```text
"import"
  <identifier> "("
    [<identifier> "=" <identifier> ("," <identifier> "=" <identifier>)*] ["," "*"] ["as" <identifier>] ["from" <string>]
  ")"
```

--------------------------------

### Reduce list elements

Source: https://quint.sh/docs/builtin

Reduces a list from the left using a starting value and a binary function.

```text
pure val sum = List(1, 2, 3, 4).foldl(0, (x, y) => x + y)
assert(sum == 10)
pure val l = List(1, 2, 3, 4).foldl(List(), (l, e) => l.append(e))
assert(l == List(1, 2, 3, 4))
```

--------------------------------

### Evaluate delayed assignment in an action

Source: https://quint.sh/docs/lang

Example showing how delayed assignment behaves within an action block.

```quint
all {
  x' = 4,
  x + 1 > 0
}
```

--------------------------------

### Sample Bank Specification

Source: https://quint.sh/docs/getting-started

A basic Quint module defining state variables, actions, and an invariant for a bank account system.

```quint
module bank {
  /// A state variable to store the balance of each account
  var balances: str -> int
 
  pure val ADDRESSES = Set("alice", "bob", "charlie")
 
  action deposit(account, amount) = {
    // Increment balance of account by amount
    balances' = balances.setBy(account, curr => curr + amount)
  }
 
  action withdraw(account, amount) = {
    // Decrement balance of account by amount
    balances' = balances.setBy(account, curr => curr - amount)
  }
 
  action init = {
    // At the initial state, all balances are zero
    balances' = ADDRESSES.mapBy(_ => 0)
  }
 
  action step = {
    // Non-deterministically pick an address and an amount
    nondet account = ADDRESSES.oneOf()
    nondet amount = 1.to(100).oneOf()
    // Non-deterministically choose to either deposit or withdraw
    any {
      deposit(account, amount),
      withdraw(account, amount),
    }
  }
 
  /// An invariant stating that all accounts should have a non-negative balance
  val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0)
}
```

--------------------------------

### Report lookup error

Source: https://quint.sh/docs/lang

Example of the error message generated when a name is not found due to lack of re-export.

```text
error: [QNT404] Name 'greeting' not found
12:   def greet(name) = [ greeting, name ]
                          ^^^^^^^^
```

--------------------------------

### Run Specification and Tests

Source: https://quint.sh/docs/choreo/tutorial

Commands to execute the Quint specification and run defined tests.

```Bash
quint run two_phase_commit.qnt --invariant consistency
```

```Bash
[ok] No violation found (7045ms at 1419 traces/second).
Trace length statistics: max=8, min=5, average=6.49
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x12954db3ea62c1 to reproduce.
```

```Bash
quint test two_phase_commit.qnt --match commitTest
```

```Bash
  two_phase_commit
    ok commitTest passed 1 test(s)
 
  1 passing (16ms)
```

--------------------------------

### Configure Protocol Nodes

Source: https://quint.sh/docs/choreo/tutorial

Sets up the coordinator and participant nodes for the protocol.

```Quint
   // =============================================================================
   // PROTOCOL CONFIGURATION
   // =============================================================================
 
-  // TODO: Define your process set
-  pure val NODES = Set("n1", "n2", "n3")  // Replace with your node set
+  pure val COORDINATOR: Node = "c"
+  pure val PARTICIPANTS: Set[Node] = Set("p1", "p2", "p3")
+  pure val NODES = PARTICIPANTS.union(Set(COORDINATOR))
```

--------------------------------

### Represent Apalache SMT constraints

Source: https://quint.sh/docs/model-checkers

Example of the SMT constraints generated by Apalache for a 2-step execution sequence.

```text
x0 = 0 // initial state
x1 = x0 + 1 // first transition
x2 = x1 + 1 // second transition
x2 = 2 // negated invariant
```

--------------------------------

### Simulator output for multiple invariant violations

Source: https://quint.sh/docs/checking-properties

Example output identifying which specific invariants were violated during execution.

```text
An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> -63, "bob" -> 0, "charlie" -> 0) }
 
[violation] Found an issue (44ms).
  ❌ no_negatives
  ❌ total_positive
Use --verbosity=3 to show executions.
Use --seed=0x4e85b3a53f7ef to reproduce.
error: Invariant violated
```

--------------------------------

### Simulator output for invariant violation

Source: https://quint.sh/docs/checking-properties

Example output showing a state trace where the negated invariant is violated.

```text
An example execution:
 
[State 0] { balances: Map("alice" -> 0, "bob" -> 0, "charlie" -> 0) }
 
[State 1] { balances: Map("alice" -> 9, "bob" -> 0, "charlie" -> 0) }
 
[violation] Found an issue (8ms).
Use --verbosity=3 to show executions.
Use --seed=0xa0bbf64f2c03 to reproduce.
error: Invariant violated
```

--------------------------------

### Retrieve map value with get

Source: https://quint.sh/docs/builtin

Fetches the value associated with a key. Behavior is undefined if the key is missing.

```text

pure val m = Map(1 -> true, 2 -> false)
assert(m.get(1) == true)
```

--------------------------------

### Sum Type Construction

Source: https://quint.sh/docs/development-docs/rfcs/rfc001-sum-types

Demonstrates the syntax for creating instances of sum types and records.

```quint

let s = left(4)
let p = {
    fst: 4,
    snd: "Two"
}
```

--------------------------------

### Define nested operators and constants

Source: https://quint.sh/docs/lang

Examples of defining nested operators, constants, and non-deterministic values within Quint.

```quint
def double(x) =
  // a nested operator
  def plus(a, b) = a + b
 
  plus(x, x)
 
def pow4(x) =
  // a nested constant
  val x2 = x * x
 
  x2 * x2
 
def triple(x) =
  // if you want to write a definition and use it on the same line, use a semicolon
  def add(n) = n + x; add(x, add(x, x))
 
// a state variable to define "next"
var n: int
 
action next = {
  // non-deterministically choose i from the set 0.to(10)
  nondet i = oneOf(0.to(10))
  all {
    i > n,
    n' = i,
  }
}
 
temporal my_prop =
  // a nested temporal formula
  temporal A = eventually(x > 3)
  // a nested temporal formula
  temporal B = always(eventually(y = 0))
 
  A implies B
```

--------------------------------

### Initialize State Variables

Source: https://quint.sh/docs/lessons/coin

Assigns the minter address and initializes all balances to zero.

```quint

        all {
            minter' = sender,
            balances' = ADDR.mapBy(a => 0)
        }
    }
```

--------------------------------

### Apply weak fairness

Source: https://quint.sh/docs/builtin

Example demonstrating the weakFair operator to ensure an action eventually occurs if it remains enabled.

```TLA+

var x: int
action Init = x' = 0
action Next = any {
  x' = x + 1,
  x' = x,
}
 
temporal Property = Next.weakFair(Set(x)).implies(eventually(x == 10))
```

--------------------------------

### quint run

Source: https://quint.sh/docs/quint

Simulate a Quint specification and optionally check invariants.

```APIDOC
## quint run <input>

### Description
Simulate a Quint specification and (optionally) check invariants. If no critical errors occur, the simulator attempts to find a trace that violates the specified invariant.

### Parameters
#### Options
- **--out** (string) - Optional - Output file path (suppresses console output).
- **--main** (string) - Optional - Name of the main module.
- **--out-itf** (string) - Optional - Output the trace in the Informal Trace Format to a file.
- **--max-samples** (number) - Optional - Maximum number of runs to attempt (default: 10000).
- **--n-traces** (number) - Optional - Number of traces to generate (default: 1).
- **--max-steps** (number) - Optional - Maximum number of steps in every trace (default: 20).
- **--init** (string) - Optional - Name of the initializer action (default: "init").
- **--step** (string) - Optional - Name of the step action (default: "step").
- **--invariants** (array) - Optional - Space separated list of invariants to check.
- **--invariant** (string) - Optional - Invariant to check (definition name or expression).
- **--witnesses** (array) - Optional - Space separated list of witnesses to report on.
- **--hide** (array) - Optional - Space separated list of variable names to hide from terminal output.
- **--seed** (string) - Optional - Random seed for non-deterministic choice.
- **--verbosity** (number) - Optional - Output verbosity level (0 to 5, default: 2).
- **--mbt** (boolean) - Optional - Enable metadata for model-based testing (experimental).
- **--backend** (string) - Optional - Backend to use for simulation ("typescript" or "rust", default: "typescript").

### Error Response
{
  "stage": "running",
  "errors": [ "<errors>" ]
}
```

--------------------------------

### View saved expression format

Source: https://quint.sh/docs/repl

Example of how previously typed expressions are stored within comments in the saved file.

```text
/*! (heatingOn, temperature, beeping) !*/
```

--------------------------------

### Execute Minting in REPL

Source: https://quint.sh/docs/lessons/coin

Command to initialize the state and perform a minting operation in the REPL.

```bash

quint -r coin.qnt::coin 'init' 'mint(minter, "bob", 2023)' 'state'
```

--------------------------------

### Generate Model-Based Testing Traces

Source: https://quint.sh/docs/model-based-testing

Executes the Quint simulator to generate traces with MBT metadata, outputting them to JSON files.

```bash
quint run bank.qnt --mbt --n-traces=10000 --out-itf=traces/out.itf.json
```

--------------------------------

### Define an operator with an invalid mode

Source: https://quint.sh/docs/development-docs/architecture-decision-records/adr004-effect-system

An example of a 'def' operator attempting to perform an update, which violates mode constraints.

```quint
module foo {
  var x: int
 
  def bar(y) = x' = y
}
```

--------------------------------

### Define module structure

Source: https://quint.sh/docs/repl

Template for the kettle.qnt module structure used throughout the tutorial.

```Quint

// -*- mode: Bluespec; -*-
// The example from the REPL tutorial
module kettle {
<<<definitions>>>
}
```
Tokens:
Raw