Summary of Quint

Revision	Date	Author
32	19.01.2023	Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani

This document presents language constructs in the same order as the summary of TLA+.

Table of Contents

Summary of Quint

Identifiers and strings

Identifiers are defined exactly as in TLA+:

identifier ::=
    <string matching regex [a-zA-Z_]([a-zA-Z0-9_])*>

String literals are written as follows:

"hello, world!"

You cannot do much with strings. They can be compared for equality and inequality, and they can be stored in sets, maps, lists, tuples, and records. In this sense, strings are just more liberal identifiers.

Comments

Single-line comments:

// this is a one-line comment
some code // this is also a one-line comment

Multi-line comments:

/*
 This is a multi-line comment.
 We are writing comments like in:
 C, C++, Go, Java, Scala, Rust, JavaScript, CSS, etc.

 This is the principle of the least surprise.
 */

Types

Quint is a typed language. All variables and constants must be assigned a type. Other definitions may be annotated with types. If the type checker is able to infer the type of a definition, then its type may be omitted.

Discussion. In the earlier versions of Quint, we allowed the user to omit types altogether. In retrospect, we find this to be a bad idea. Hence, we require that every definition is either type-annotated (variables and constants), or can be assigned a type via type checking (operators and expressions).

Type System 1.2

This is the same type system as in Apalache, except we have added discriminated unions:

A type is one of the following:

Basic type: bool, int, str.
Uninterpreted type or type name: IDENTIFIER_IN_CAPS.
Type variable (parameter): a, ..., z.
Set: Set[T] for a type T.
List: List[T] for a type T.
Tuple: (T_1, T_2, ..., T_n) for n >= 2 types T_1, ..., T_n.
Record: { name_1: T_1, name_2: T_2, ..., name_n: T_n } for n >= 1 types T_1, ..., T_n.
Function: T1 -> T2 for types T1 and T2.
Operator: (T_1, ..., T_n) => R for n >= 0 argument types T_1, ..., T_n and result type R.

Discriminated union:

   | { tag: string_1, <ident>: T_1_1, ..., <ident>: T_1_n_1}
   ...
   | { tag: string_k, <ident>: T_k_1, ..., <ident>: T_k_n_k}

for n >= 1 types T_1_1, ..., T_k_n_k.

Type in parentheses: (T) for a type T.

It is often convenient to declare a type alias. You can use type to define an alias inside a module definition. For instance:

type STR_OPTION =
    | { tag: "none" }
    | { tag: "some", value: str }

A type identifier can also introduce an uninterpreted type by defining a type without any constructors for values of that type:

type MY_TYPE

Modes

TLA+ does not make a clear distinction between constant expressions, state expressions, actions, and temporal formulas. They are all written as logic formulas. Such a distinction appears only in the discussion of TLA+ semantics, when Leslie Lamport introduces levels of TLA+ formulas. We have found that the lack of such a clear separation causes lots of confusion. To this end, we introduce "modes", which are similar in spirit to TLA+ levels, but more refined.

We define the following modes:

Stateless mode.
State mode.
Non-determinism mode.
Action mode.
Run mode.
Temporal mode.

Every Quint expression and definition is assigned a mode. In the following, we will specify which modes are supported by certain operators and definitions. The following table defines the subsumption rules on modes (the partial order <m). As a general rule, if an operator or a definition accepts an argument of mode M, then it can also accept an argument of a less general mode K <m M.

More general mode	Less general modes
Stateless	n/a
State	Stateless
Non-determinism	Stateless, State
Action	Stateless, State
Run	Stateless, State, Action
Action	Non-determinism, Stateless, State
Temporal	Stateless, State

As can be seen from the table, action mode and temporal mode are incomparable. This is intentional: We do not want to mix actions with temporal formulas.

Module-level constructs

Module definition

A module definition is introduced like follows:

module Foo {
  // module definitions

  module Bar {
    // definitions of the nested module

    module Baz {
      // Yet another level of nesting.
      // More definitions.
    }
  }
}

Grammar:

"module" <identifier> "{"
  <definitions>
"}"

A single file should contain one top-level module, though there is no limit on the number of nested modules and their depth of nesting. To ease module lookup, the name of the top-level module should match the file name. For example, a file Orange.tla should contain module Orange { ... }. This is not a strict requirement. You have to follow it only, if you are using multiple files.

There is another way to define a module, see Instances.

WARNING: We are redesigning nested modules, see #496. If you are starting with the language, wait a bit before using nested modules.

Constant declarations

Introduce a single constant parameter (rigid variable in TLA+)

  const N: int
  const Proc: Set[str]

Grammar:

  "const" <identifier> ":" <type>

Mode: Stateless

Assumptions

Given a constant predicate P and a name, we can write an assumption P over the constants that is associated with this name.

Example:

assume AtLeast4 = N >= 4

This is exactly the same as the following assumption in TLA+:

ASSUME AtLeast4 == N >= 4

Grammar:

"assume" <identifier> "=" <expr>

Similar to TLA+, you can have an anonymous assumption, by simply using _ for the name:

assume _ = Proc.size() > 0

Mode: Stateless

Variable definitions

Introduce a single variable (flexible variable in TLA+)

  var name: str
  var timer: int
  var isArmed: bool

Grammar:

  "var" <identifier> ":" <type>

Mode: State

Operator definitions

Introduce a user-defined operator. The order of definitions is not important. The operator names should not clash with the names of other definitions in the module scope. Importantly, there are no recursive operators (though you can fold over a list or a set, see below).

// 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, y): ((a, b) => a) =
    x

// the maximum operator
pure def max(x, y): (int, 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, x): ((a => b, 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) =
    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) =
    // 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)

Grammar:

("val" | "def" | "pure" "val" | "pure" "def" | "action" | "temporal")
    <identifier>["(" <identifier> ("," ..."," <identifier>)* ")"] [":" <type>]
      "=" <expr> [";"]

Mode: The mode depends on the mode of the expression in the right-hand side. The following table defines this precisely.

Qualifier	Mode of `expr`	Mode of definition
`pure val`, `pure def`	Stateless	Stateless
`val`, `def`	State	State
`action`	Action	Action
`temporal`	Stateless, State, Temporal	Temporal

No recursive functions and operators

We've decided against having recursive operators and functions in the language. The practical use cases can be expressed with map, filter, and fold.

Module instances

Similar to INSTANCE in TLA+, we can define module instances.

Example:

// an instance of Voting that has the name "V"
module V = Voting(Value = Set(0, 1))

// the names of V are accessed via "."
val MyValues = V.Value

Grammar:

"module" <identifier> "="
  <identifier> "("
    [<identifier> "=" <identifier> ("," <identifier> "=" <identifier>)*] ["," "*"]
  ")"

This is an advanced topic. For details, see Instances.

We do not allow for parameterized instances. They are only needed for reasoning about variable hiding and refinement proofs. In this case, you would be better off with TLA+ and TLAPS.

Type aliases

As discussed above, you can define a type alias, by following the grammar rule:

"type" <IDENTIFIER_IN_CAPS> "=" <type>

Discussion: We could introduce type aliases at any level. Hence, we can move them to the expression syntax.

Theorems

There are no theorems. You can write them in TLA+ and prove them with TLAPS.

Imports

See Namespaces and imports.

Namespaces and imports

The topic of modules, namespaces, and instances is extremely obfuscated in TLA+, for no obvious reason. In Quint, we follow a simple approach that would not surprise anyone, who knows modern programming languages.

We are using Quint expressions in the examples in this section. It is probably a good idea to skip this section on the first read and read about Quint expression syntax first.

Stateless and stateful modules

We distinguish between stateless and stateful modules. A stateful module has at least one constant or variable declaration. All other modules are stateless. This is an important distinction. Definitions of stateless modules may be accessed via the dot-notation and imported, whereas stateful modules must be instantiated before they can be accessed.

Namespaces

Every module has a namespace associated with it. Consider the example:

module Foo {
  const N: int
  var x: int

  action Init =
    x' = 0

  action Next =
    x' = x + N
}

In our example, module Foo has four names in its namespace: N, x, Init, and Next.

A nested module defines its own namespace, which extends the namespace of the outer module:

module Outer {
  var x: int

  def xPlus(z) = x + z

  module Inner {
    val x2 = x + x
  }

  val inv =
    (Inner.x2 - x == x)
}

In the above example, the module Outer has the following names in its name space: x, xPlus, inv, and Inner, whereas the module Inner contains the names x2 and the names defined in its parent modules: x, xPlus, and inv. The module Inner is stateless, so the module Outer may access the definitions of Inner via the dot-notation, e.g., Inner.x2.

WARNING: We are redesigning nested modules, see #496. If you are starting with the language, wait a bit before using nested modules.

No collisions. There must be no name collisions between child modules and parent modules. Shadowing of a name is not allowed. For example:

module OS {
  var clock: int

  module Process {
    var clock: int
    //  ^^^^^ error: 'clock' is already defined in 'OS'
  }
}

One solution to the above problem is to define both modules OS and Process at the same level, either in separate files, or inside another module.

No order. In contrast to TLA+, namespaces are not ordered. It is perfectly fine to write out-of-order definitions, like in many programming languages:

module outOfOrder {
  def positive(x) = max(x, 0)

  def max(x, y) = x > y ? x : y
}

As a specification author, you and your peers have to decide on your style, whereas your text editor should help you in finding definitions. Quint is not Fashion Police.

Imports

As it may be tedious to access definitions via the dot-notation, Quint supports name imports:

module Imports {
  module Math {
    def sqr(x) = x * x
    def pow(x, y) = x^y
  }

  // import 'pow' from Math
  import Math.pow

  def cube(x) = pow(x, 3)
}

In the above example, the name pow is imported in the scope of the module Imports. As a result, definitions in Imports may refer to pow, which is just a short-hand for Math.pow. As you would expect, imports are not allowed to introduce name collisions.

To avoid writing too many import statements, you can use *. For example:

module ImportAll {
  module Math {
    def sqr(x) = x * x
    def pow(x, y) = x^y
  }

  // import all names from Math
  import Math.*

  // access 'pow' and 'sqr' of Math
  def poly(x) = pow(x, 3) + sqr(x) + x
}

No export. It is important to know that import does not introduce any definitions in the module that uses import. Hence, the following example produces a lookup error:

module NoExport {
  module MiddleMan {
    module English {
      val greeting = "hello"
    }

    import English.*
  }

  def greet(name) = [ MiddleMan.greeting, name ]
  //                  ^^^^^^^^^^^^^^^^^^ error: 'MiddleMan.greeting' not found in 'NoExport'
}

Hence, import English.* is working similar to LOCAL INSTANCE English of TLA+.

No hiding. TLA allows the user to add LOCAL in front of an operator definition or an instance. Here is a TLA+ example:

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

In the above example, the definition F is auxiliary to G. In Quint, we do not hide definitions. If you want to indicate to the users of your module, if there are any, that they should not access some private definitions, you may hide those definitions in a nested module that start with the underscore:

module Local {
  var y: int
  def G(x) = Set(_local.F(x))

  module _local {
    def F(x) = Set(x, y)
  }
}

By convention, a module should not access a submodule of another module, if the name of the submodule starts with an underscore. This is only a convention. If you do that, a Quint parser may issue a warning, but it will not crash.

Quint expression syntax

Literals

Boolean literals are written as follows:

// FALSE in TLA+
false
// TRUE in TLA+
true
// BOOLEAN = { FALSE, TRUE } in TLA+
Bool

Integer literals are written as follows:

0
1
2
1024
// integer literals can be really big
340282366920938463463374607431768211456
// similar to Solidity, one can separate digits with '_'
100_000_000
// hexadecimal notation is also supported, including '_'
0xabcdef
0xAbCdEf
0xAB_CD_EF
...

The set of all integers is written as Int and the set of all naturals is written as Nat.

Names

Like in many programming languages, names are a basic building block of expressions. To see this, consider the following example:

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
  }
}

Here is the list of names that are normally used in expressions:

Names of the operators, for example myMul in the definition of sqr.
Names of the operator arguments, e.g., i and j in the definition of myMul, that also appear in anonymous operators (lambdas).
Names of constants, e.g., acceleration in the definition of distance.
Names of state variables, e.g., clock in the definitions of distance, init, and next.

Braces and parentheses

You can wrap an expression e in braces: { e }. The expression { e } is always in the Action mode. Recall that applying an expression of the Action mode in another mode is not allowed. If you wrap an expression e of a mode that is less general than the Action mode, the parser should issue a warning.

Alternatively, you can wrap an expression e in parentheses: (e). In this case, e is not allowed to be in the Action-mode. If e is in the Action mode, the parser must issue an error.

Lambdas (aka Anonymous Operators)

As noted when we introduced types and operator definitions, the type of operators is specified using the syntax (a_1, ..., a_n) => b, for an operator that takes arguments of types a_1 to a_n to an expression of type b. Anonymous operators expressions, known in TLA+ as "lambdas", can be constructed with the corresponding syntax.

In Quint, (x_1, ..., x_n) => e is an anonymous operator which, when applied to expressions e_1 to e_n, reduces to the expression e[e_1/x_1, ..., e_n/x_n] (that is, every parameter x_i is substituted with the expression e_i, for 1 <= i <= n). Two important comments are in order:

When n = 1, we can write x => e instead of (x) => e.
The case of n = 0 is not allowed.

Compare this to the TLA+2 syntax:

LAMBDA x_1, ..., x_n: e

As is common, we can skip parameter names, if we don't need them:

_ => e
(_) => e
(_, ..., _) => e

Note that lambdas can be only passed as arguments to other operators. They cannot be freely assigned to values or returned as a result of an operator.

Two forms of operator application

Quint is flexible with respect to operator applications. It supports two call styles that are familiar from popular languages. Given an operator called f and expressions e_1, ..., e_n, the operator f can be applied to the expressions e_1, ..., e_n as follows:

Quint normal form: f(e_1, ..., e_n).
UFCS: e_1.f(e_2, ..., e_n)

These forms always require parentheses, even if the number of arguments in parentheses is zero. That is, f() and e_1.g() are the right ways to apply operators f and g in the normal form and UFCS, respectively. The form without parentheses is reserved for field access of tuples and records as well as accessing namespaces.

The Quint normal form is especially convenient for programs, so they should communicate in this form. People may communicate in any form.

A reserved class of built-in operators can only be called via infix form. These operators have conventional names that stem from mathematics and thus are not written as identifiers. For instance, you must write 1 + 3 in the infix form; You cannot write +(1, 3) or 1.+(3). The normal form for these operators can be achieved by using the mnemonic names, such as iadd instead of the infix symbol. E.g., you may write iadd(1, 3) or 1.iadd(3) in place of 1 + 3. A small number of operators are exceptional in this sense. We list the alternative names when introducing operators. We don't expect humans to write expressions like the ones above. This notation is more convenient for programs, so Quint tooling should use the Quint normal form.

Like in every programming language, several operators are special in the sense that they have non-standard priorities. The good news is that we keep the number of such operators to the bare minimum, in contrast to TLA+. If you are using the infix form, it is good to know the operator priorities. Here is the table of operator priorities, the ones in the top have the higher priority:

Operators	Comments
`e_1.F(e_2, ..., e_n)`	Call via dot has the highest priority
`F(e_1, ..., e_n)`	The normal form of operator application
`l[i]`	List access via index
`i^j`	Integer power (right associative)
`-i`	Unary minus
`i * j`, `i / j`, `i % j`	Integer multiplication, division, modulo
`i + j`, `i - j`	Integer addition and subtraction
`i > j`, `i < j`, `i >= j`, `i <= j`, `i == j`, `i != j`	Integer comparisons, general equality/inequality
`x' = e`	Delayed assignment
`and { ... }`	braced 'and'
`p and q`	infix 'and'
`or { ... }`	braced 'or'
`p or q`	infix 'or'
`p iff q`	Boolean equivalence (if and only if)
`p implies q`	Boolean implication: `not(p) or q`
all { ... }	braced action 'all'
any { ... }	braced action 'any'
k -> v	a pair
all forms with `(..)`, `{..}`, and `[..]`	the lowest priority

Boolean operators and equality

The following are the standard Boolean operators (higher priority first).

// equality: e1 = e2 in TLA+
e1 == e2
e1.eq(e2)
eq(e1, e2)
// inequality (same priority as '='): e1 /= e2, e1 # e2 in TLA+
e1 != e2
e1.neq(e2)
neq(e1, e2)
// logical not: ~p in TLA+
not(p)
p.not()
// Logical "and".
// In TLA+: p /\ q
p and q
p.and(q)
and(p, q)
// The logical "and" is n-ary:
and(p1, p2, p3)
and(p1, p2, p3, p4)
// Logical "or".
// In TLA+: p \/ q
p or q
p.or(q)
or(p, q)
// The logical "or" is n-ary
or(p1, p2, p3)
or(p1, p2, p3, p4)
// logical equivalence: p <=> q in TLA+
p iff q
p.iff(q)
iff(p, q)
// implication: p => q in TLA+
p implies q
p.implies(q)
implies(p, q)

Note that the operator not(p) needs parentheses around its argument. Actually, not is treated as a general operator. We keep the number of special syntax forms to a minimum.

Mode: Stateless, State, Temporal.

Block disjunctions

The following expression can be written in the action mode:

any {
  a_1,
  a_2,
  ...
  a_n,
}

Mode: Action.

The trailing comma next to a_n is optional, and n must be positive.

This operator is written as actionAny(p_1, ..., p_n) in its normal form. It evaluates the actions a_1, ..., a_n in isolation (that is, ignoring the side effects introduced by assignments in the actions) and then non-deterministically executes one of the enabled actions. The operator returns true, if it has evaluated one of the actions to true. If no such action exists, it returns false.

Since the syntax of the above operator is convenient, we have introduced a similar syntax form in the non-action modes:

or {
  p_1,
  p_2,
  ...
  p_n,
}

This is simply the syntax sugar for or(p_1, ..., p_n).

Mode: Non-action.

Block conjunctions

The following expression can be written in the action mode:

all {
  p_1,
  p_2,
  ...
  p_n,
}

Mode: Action.

The trailing comma next to a_n is optional, and n must be positive.

This operator is written as actionAll(p_1, ..., p_n) in its normal form. It evaluates the actions a_1, ..., a_n one-by-one lazily. As soon as one of the actions a_i evaluates to false, it returns false. In this case, all side effects (lazy assignments) produced by a_1, ..., a_{i+1} are erased, and the operator returns false. If all actions evaluate to true, all their side effects are applied, and the operator returns true.

Since the syntax of the above operator is convenient, we have introduced a similar syntax form in the non-action modes:

and {
  p_1,
  p_2,
  ...
  p_n,
}

This is simply the syntax sugar for and(p_1, ..., p_n).

Mode: Non-action.

Flow operators

Condition

  if (p) e1 else e2

This operator is translated to TLA+ as:

  IF p THEN e1 ELSE e2

The normal form of this operator is ite(p, e1, e2).

Mode: Stateless, State, Action, Temporal.

Cases (removed)

After discussing this language feature, we have decided to remove case. The action-mode semantics of CASE in TLA+ is redundant in the presence of disjunctions. The expression-mode semantics of CASE in TLA+ does what the users do not expect: If two branches are evaluated to TRUE in the same state, then one of them is deterministically chosen with CHOOSE (there is no predefined way of telling which one is chosen). For all these reasons, we do not introduce CASE in Quint. Use series of if-else if-else expressions.

Case enumeration with the default case:

case (
  | p_1 -> e_1
  | p_2 -> e_2
  ...
  | p_n -> e_n
  | _   -> e
)

Compare it to TLA+:

CASE
     p_1 -> e_1
  [] p_2 -> e_2
  ...
  [] p_n -> e_n
  OTHER -> e_def

The normal form of the case operator with the default option is:

caseBlock(p_1, e_1, ..., p_n, e_n, e_def)

Note that this operator simply has 2*n + 1 arguments. We do not group the guards and effect expressions into pairs. The normal form is meant for the tools.

Mode: Stateless, State. Other modes are not allowed.

Discussion: TLA+ allows for expressions x' = e inside CASE. We have found the use of this feature to be extremely rare and confusing. It can be easily rewritten with disjunctions and conjunctions, which should be preferred to case in the Action mode.

TLA+ allows for CASE without the default option. This construct is error-prone, as it easily leads to incomplete case enumeration. In contrast to many programming languages, it does not suffice to perform a syntax test or a type test, in order to see, whether all cases are covered. For this reason, we do not support case expressions without the default arm.

Sets

Set constructor

One way to construct a set is by enumerating its elements:

// the python-style constructor
Set(e_1, ..., e_n)

This is exactly as { e_1, ..., e_n } in TLA+. However, we prefer not to sacrifice {...} for this only operator. That is why a set is constructed with Set(...) in Quint. In practice, this operator does not appear too often, so our notation would not distract you too much.

Mode: Stateless, State. Other modes are not allowed.

Discussion. The earlier versions contained an alternative syntax '{ e_1, ..., e_n }. After receiving the feedback, we have left just one constructor.

Non-deterministic choice

In contrast to TLA+, we introduce a special syntax form for non-deterministic choice, which is normally written with \E x \in S: P in TLA+ actions.

The syntax form is as follows:

nondet name = oneOf(expr1)
expr2

The semantics of the above form is as follows. The operator oneOf(expr1) non-deterministically picks one element of expr1 (which should be a non-empty set). The picked element is bound to the name name. This name can be used in the nested action expr2.

Example:

val x: int

action nextSquare = {
  nondet i = oneOf(Int)
  all {
    Int.exists(j => i * i = j),
    i > x,
    x' = i,
  }
}

In the above example, i is a non-deterministically chosen integer. The further action below nondet i = ... requires the value of i to be a square of an integer j. In addition to that, it requires i to increase in comparison to x. Finally, the picked value of i is assigned to x.

Mode: The modes of oneOf and nondet are defined in the following table:

Operator	Argument mode	Output mode
`oneOf`	Stateless, State	Non-determinism
`nondet x = e1; e2`	e1: Nondet, e2: Action	Action

Discussion. Although according to the semantics of oneOf, a value is chosen non-deterministically, practical implementations may prefer to choose an element in a way that is not entirely non-deterministic. For instance, a random simulator may implement the operator oneOf(S) as a random choice of an element from the set S. Further, an interactive simulator may ask the user to choose an element of S. Non-determinism is only important to us when reasoning exhaustively about all executions, e.g., in a model checker or a theorem prover.

Other set operators

The other operators are introduced and explained in code directly.

// \E x \in S: P
S.exists(x => P)
exists(S, (x => P))
// \A x \in S: P
S.forall(x => P)
forall(S, (x => P))
// set membership: e \in S
e.in(S)
in(e, S)
S.contains(e)
contains(S, e)
// set non-membership: e \notin S
e.notin(S)
notin(e, S)
// union: S \union T
S.union(T)
union(S, T)
// intersection: S \intersect T
S.intersect(T)
intersect(S, T)
// difference: S \ T
S.exclude(T)
exclude(S, T)
// S is a subset of T (proper or not): S \subseteq T
S.subseteq(T)
subseteq(S, T)
// set comprehension (map): { e: x \in S }
S.map(x => e)
map(S, (x => e))
// set comprehension (filter): { x \in S: P }
S.filter(x => P)
filter(S, (x => P))
// set folding: you can write such a recursive operator in TLA+
S.fold(init, (v, x => e))
fold(S, init, (v, x => e))
// SUBSET S
S.powerset()
powerset(S)
// UNION S
S.flatten()
flatten(S)
// Seq(S): the set of all lists of elements in S
S.allLists()
allLists(S)
// CHOOSE x \in S: TRUE
// The operator name is deliberately made long, so it would not be the user's default choice.
S.chooseSome()
// There is no special syntax for CHOOSE x \in S: P
// Instead, you can filter a set and then pick an element of it.
S.filter(x => P).chooseSome

These operators are defined in the module FiniteSets in TLA+. Quint has these two operators in the kernel:

// Test a set for finiteness.
// TLA+ equivalent: IsFiniteSet(S)
S.isFinite()
isFinite(S)
// Set cardinality for finite sets.
// TLA+ equivalent: Cardinality(S)
S.size()
size(S)

Mode: Stateless, State. Other modes are not allowed.

Maps (aka Functions)

// Map application.
// In TLA+: f[e]
f.get(e)
get(f, e)
// Map domain.
// In TLA+: DOMAIN f
f.keys()
keys(f)
// Map constructor via evaluation.
// In TLA+: [ x \in S |-> e ]
S.mapBy(x => e)
mapBy(S, (x => e))
// Map constructor via enumeration.
Map()
Map(k_1 -> v_1)
Map(k_1 -> v_1, k_2 -> v_2)
Map(k_1 -> v_1, k_2 -> v_2, k_3 -> v_3)
...
// Convert a set of pairs to a map.
// In TLA+: [ x \in { a: <<a, b>> \in S } |-> (CHOOSE p \in S: p[1] = x)[2]]
Set((1, true), (2, false)).setToMap()
setToMap(Set((1, true), (2, false)))
// A set of maps.
// In TLA+: [ S -> T ]
S.setOfMaps(T)
setOfMaps(S, T)
// Update a map at given key.
// In TLA+: [f EXCEPT ![e1] = e2]
f.set(e1, e2)
set(f, e1, e2)
// Multi-point update can be done via multiple applications.
// In TLA+: [f EXCEPT ![e1] = e2, ![e3] = e4]
f.set(e1, e2).set(e3, e4)
// Update by using the old value.
// In TLA+: [f EXCEPT ![e1] = @ + y]
f.setBy(e1, (old => old + y))
setBy(f, e1, (old => old + y))
//
// In TLA+ (when using TLC): (k :> v) @@ f
f.put(k, v)
put(f, k, v)

Mode: Stateless, State. Other modes are not allowed.

Records

// record constructor: [ f_1 |-> e_1, ..., f_n |-> e_n ]
// Warning: n >= 1
{ f_1: e_1, ..., f_n: e_n }
Rec(f_1, e_1, ..., f_n, e_n)
// Set of records: [ f_1: S_1, ..., f_n: S_n ].
// No operator for it. Use a set comprehension:
tuples(S_1, ..., S_n).map(a_1, ..., a_n => { f_1: a_1, ..., f_n: a_n })
// access a record field: r.fld
r.fld           // both r and fld are identifiers
field(r, "fld") // r is an identifier, "fld" is a string literal
// the set of field names: DOMAIN r
r.fieldNames()
fieldNames(r)
// record update: [r EXCEPT !.f = e]
r.with(f, e)
with(r, f, e)

Note that we are using the syntax { name_1: value_1, ..., name_n: value_n } for records, similar to Python and JavaScript. We have removed the syntax for sets of records: (1) It often confuses beginners, (2) It can be expressed with map and a record constructor. Moreover, sets of records do not combine well with discriminated unions.

Mode: Stateless, State. Other modes are not allowed.

Discriminated unions

WARNING: We are redesigning discriminated unions, see #539. As they are not fully implemented, please avoid using discriminated unions for now.

Quint has provides the user with special syntax for constructing and destructing discriminated unions. For the type syntax of discriminated unions, see Types.

Constructors. Construct a tagged record by using the record syntax, e.g.:

  { tag: "Cat", name: "Ours", year: 2019 }

Note that the above record has the field tag. Hence, this record is assigned a union type of one element:

type CAT_TYPE =
  | { tag: "Cat", name: str, year: int }

Records of different union types may be mixed in a single set. For example:

val Entries =
  Set(
    { tag: "Cat", name: "Ours", year: 2019  },
    { tag: "Cat", name: "Murka", year: 1950 },
    { tag: "Date", day: 16, month: 11, year: 2021 }
  )

In the above example, the set elements have the following union type:

type ENTRY_TYPE =
  | { tag: "Cat", name: str, year: int }
  | { tag: "Date", day: int, month: int, year: int }

When we construct the individual records, they still have singleton union types. For instance, the entry { tag: "Date", day: 16, month: 11, year: 2021 } has the type:

type DATE_TYPE =
  { tag: "Date", day: int, month: int, year: int }

Set filters. The most common pattern over discriminated union is to filter set elements by their tag. Using the above definition of Entries, we can filter it as follows:

Entries.filter(e => e.tag == "Cat")

As expected from the semantics of filter, the above set is equal to:

Set(
  { tag: "Cat", name: "Ours", year: 2019  },
  { tag: "Cat", name: "Murka", year: 1950 }
)

Importantly, its elements have the type:

type CAT_TYPE =
  | { tag: "Cat", name: str, year: int }

Destructors. Sometimes, we have a value of a union type that is not stored in a set. For this case, Quint has the union destructor syntax. For example, given an entry from Entries, we can compute the predicate isValid by case distinction over tags:

pure def isValid(entry): ENTRY_TYPE => bool =
  entry match
     | "Cat": cat =>
       name != "" and cat.year > 0
     | "Date": date =>
       date.day.in(1 to 31) and date.month.in(1.to(12)) and date.year > 0

In the above example, the names cat and date have the singleton union types of CAT_TYPE and DATE_TYPE, respectively. Note that the expressions after the tag name (e.g., "Cat": and "Date":) follow the syntax of single-argument lambda expressions. As a result, we can use _ as a name, which means that the name is omitted.

Match expressions require all possible values of tag to be enumerated. This is ensured by the type checker.

We do not introduce parentheses in the syntax of match. If you feel uncomfortable about it, wrap the whole match-expression with (...).

Grammar:

  expr "match" ("|" string ":" (identifier | "_") "=>" expr)+

Normal form: Consider the match operator:

  ex match
    | tag_1: x_1 => ex_1
    ...
    | tag_n: x_n => ex_n

Its normal form is unionMatch(ex, tag_1, (x_1 => ex_1), ..., (x_n => ex_n)).

Mode: Stateless, State. Other modes are not allowed.

Discussion. In TLA+, there is no separation between discriminated unions and records. It is common to use tagged records to distinguish between different cases of records. Quint makes this pattern explicit.

Tuples

In contrast to TLA+, Quint tuples have length of at least 2. If you need lists, use lists.

// Tuple constructor: << e_1, ..., e_n >>
// Warning: n >= 2
(e_1, ..., e_n)
Tup(e_1, ..., e_n)
// t[1], t[2], t[3], t[4], ... , t[50]
t._1
t._2
t._3
t._4
...
t._50
item(t, idx)  // t is an identifier, idx is an integer literal
// Cartesian products
// S_1 \X S_2 \X ... \X S_n
tuples(S_1, S_2, ..., S_n)

What about DOMAIN t on tuples? We don't think it makes sense to have it.

What about [ t EXCEPT ![i] = e ]? Just define a new tuple that contains the new field. It is not likely that you will have tuples that have a lot of items.

Mode: Stateless, State. Other modes are not allowed.

Lists (aka Sequences)

In contrast to TLA+, there is no special module for lists. They are built in the kernel of Quint. A parser can compute, whether operators on lists are used in the spec.

Remember: lists in Quint are 0-indexed, in contrast to TLA+, where sequences are 1-indexed.

// List constructor.
// Equivalent to <<e_1, ..., e_n>> in TLA+.
[ e_1, ..., e_n ]
List(e_1, ..., e_n)
// List range: `start` is inclusive, whereas `end` is exclusive.
// Equivalent to [start, start + 1, ..., end - 1]
// There is no equivalent in TLA+,
// but it could be defined via a recursive operator.
range(start, end)
// Append e to the end of s.
// Equivalent to Append(s, e) in TLA+.
l.append(e)
append(l, e)
// Concatenate s and t.
// Equivalent to s \circ t in TLA+.
s.concat(t)
concat(s, t)
// List head.
// Equivalent to Head(s) in TLA+.
l.head()
head(l)
// List tail.
// Equivalent to Tail(s) in TLA+.
// It is up to the interpreter/analyzer to define the behavior of tail([]).
// The simulator shows an error message in this case.
l.tail()
tail(l)
// The length of a list.
// Equivalent to Len(s) in TLA.
l.length()
length(l)
// Sequence element at nth position (starting with 0).
// Equivalent to s[i + 1] in TLA+.
l[i]
l.nth(i)
nth(l, i)
// The set of list indices (starting with 0).
// Equivalent to { i \in DOMAIN s: i - 1 } in TLA+.
l.indices()
indices(l)
// Update the list at element i.
// Equivalent to [ s EXCEPT ![i + 1] = e ] in TLA+.
l.replaceAt(i, e)
replaceAt(l, start, end)
// Slice a list from `start` until `end`.
// Equivalent to SubSeq(lst, start + 1, end) in TLA+.
// Like in many PLs, `start` is inclusive, whereas `end` is exclusive.
// For the following cases, it is up to the interpreter/analyzer to define
// the behavior for the following cases:
//  - start < 0,
//  - start >= length(ls),
//  - end > length(ls),
//  - end < start.
// The simulator shows an error message in these cases.
l.slice(start, end)
slice(l, start, end)
// Filter a list.
// Equivalent to SelectSeq(s, Test) in TLA+.
select(l, Test)
// in particular, we can use anonymous operators
l.select(e => P)
// Left fold. There is no standard operator for that in TLA+,
// but you can define it with a recursive operator.
l.foldl(init, ((accumulator, v) => e))
foldl(l, init, ((accumulator, v) => e))
// Right fold. There is no standard operator for that in TLA+,
// but you can define it with a recursive operator.
l.foldr(init, ((v, accumulator) => e))
foldr(l, init, ((v, accumulator) => e))

Mode: Stateless, State. Other modes are not allowed.

Integers

In contrast to TLA+, there is no special module for integers. They are built in the kernel of Quint. The module Naturals does not exist either. A parser can compute, whether integer operators are used in the spec.

Moreover, there is no module Reals. If you really need Reals, most likely, you should switch directly to TLA+.

// like m + n in TLA+
m + n
m.iadd(n)
iadd(m, n)
// like m - n in TLA+
m - n
m.isub(n)
isub(m, n)
// like -m in TLA+
-m
iuminus(m)
m.uminus()
// like m * n in TLA+
m * n
m.imul(n)
imul(m, n)
// integer division, lik m \div n in TLA+
m / n
m.idiv(n)
idiv(m, n)
// like m % n in TLA+
m % n
m.imod(n)
imod(m, n)
// like m^n in TLA+
m^n
m.ipow(n)
ipow(m, n)
// like m < n in TLA+
m < n
m.ilt(n)
ilt(m, n)
// like m > n in TLA+
m > n
m.igt(n)
igt(m, n)
// like m <= n in TLA+
m <= n
m.ilte(n)
ilte(m, n)
// like m >= n in TLA+
m >= n
m.igte(n)
igte(m, n)
// like Int and Nat in TLA+
Int
Nat
// like m..n in TLA+
m.to(n)
to(m, n)

Mode: Stateless, State. Other modes are not allowed.

Nested operator definitions

They are almost identical to the top-level operators, except that they are visible only to the containing top-level operator. Nested operator definitions may contain nested operator definitions too. There is one important addition in nested definitions: non-deterministic values (nondet values).

Examples:

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

Grammar:

("pure" "val" | "val" | "def" | "pure" "def" | "nondet" | "action" | "temporal")
  <identifier>[ "(" <identifier> ("," ..."," <identifier>)* ")" ] [ ":" <type>]
    "=" <expr> [";"]
<expr>

It is nice to separate an operator definition from its application. Usually, we use a line break or two to do this. If you want to define an operator and use it on the same line, you can use a semicolon ; as a separator. We do not recommend using both a semicolon and a line break at the same time.

Mode: The modes are defined as in the case of the top-level operators. As expected, the mode of an inner operator should not be more general then the mode of the outer operator.

Operators on actions

In comparison to TLA+, Quint has a tiny set of action operators. The other action operators of TLA+ were moved to the temporal operators, because they are required only in temporal reasoning.

Delayed assignment

This operator is carefully avoided in TLA+. Quint allows you to assign a value to the state variable x in a next state:

x' = e
assign(x, e)
x.assign(e)

The operator x' = e is equivalent to x' = e of TLA+ under specific conditions. In contrast to the assignments in programming languages, Quint assignment is delayed by one step. It only becomes effective in a successor state of the state that is being evaluated. The notation x' = e is meant to warn the user that the value e is "sent" to x, and it will only arrive at x in a next state. Hence, in the following expression, expression x + 1 may evaluate to a value that is different from 5:

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

Every state variable x must be assigned via x' = e at most once in every step.

Discussion. TLA+ does not have a notion of assignment. Instead, one simply writes an equality x' = e. In general, one can write an arbitrary predicate over x'. We find it hard to reason about such pure equalities, which may occur in multiple places. Hence, we introduce assignments. However, our assignments are slightly different from assignments in imperative (stack-based) languages.

Mode. Action. Other modes are not allowed.

Non-deterministic choice

See the discussion in: Non-deterministic choice.

Assert

The operator assert has the following syntax:

assert(condition)

This operator always evaluates to condition, and it does not change the state variables. If condition evaluates to false in a state, then the user should receive a message about a runtime error. How exactly this is reported depends on the tool.

Mode: Action.

Runs

A run represents a finite execution. In the simplest case, it represents one concrete execution that is allowed by the specification. In general, it is a sequence of actions, which prescribe how to produce one or more concrete executions, if such executions exist.

Discussion. We have found that TLA+ lacks a programmatic way of describing examples of system executions. Indeed, TLA+ has the notion of a behaviour (simply put, a sequence of states starting with Init and connected via Next). However, it is relatively hard to present a sequence of steps in TLA+ itself. For instance, counterexamples produced by TLC and Apalache are not first-class TLA+ citizens. In theory, TLA+ has the operator \cdot, representing the sequential composition of two actions. However, we have never seen this operator being used in practice.

Then

The operator then has the following syntax:

A.then(B)
then(A, B)

The semantics of this operator is as follows. When A.then(B) is applied to a state s_1, the operator computes a next state s_2 of s_1 by applying action A, if such a state exists. If A returns true, then the operator A.then(B) computes a next state s_3 of s_2 by applying action B, if such a state exists. If B returns true, then the operator A.then(B) returns true, the old state is equal to s_1, and the new state is equal to s_3. In all other cases, the operator returns false.

This operator is equivalent to A \cdot B of TLA+.

Example. Consider the specification counters:

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)
}

The definition run1 captures the execution that contains five states, in which the variable n receives the values 1, 2, 3, 6, and 3, respectively. If we look carefully at the definition of run2, it produces exactly the same sequence of states as run1, but it does via evaluation of the actions Init, Positive, Positive, ByThree, and Even, in that order.

Note that a run does not have to describe exactly one sequence of states: in general a run describes a sequence of constraints over a sequence of states. For example, run3 captures all executions of the specification counters that start with Init and evaluate Next four times in a row.

Mode: Run.

Repeated

The operator repeated has the following syntax:

A.repeated(n)
repeated(A, n)

The semantics of this operator is as follows:

When n <= 0, this operator is equivalent to unchanged.
When n = 1, a.repeated(n) is equivalent to a.
When n > 1, a.repeated(a), is equivalent to a.then(a.repeated(n - 1)).

Note that the operator A.repeated(n) applies A exactly n times (when n is non-negative). If you want to repeat A from i to j times, you can combine it with orKeep as follows:

a.repeated(i).then((a.orKeep(vars)).repeated(j - i))

See the description of orKeep below.

Mode: Run.

Fail

The operator fail has the following syntax:

A.fail()
fail(A)

This operator returns true if and only if action A returns false. The operator fail is useful for writing runs that expect an action to be disabled.

Mode: Run.

Temporal operators

Temporal operators describe infinite executions.

Always

This is equivalent to [] P of TLA+:

always(P)
P.always

Mode: Temporal.

Eventually

This is equivalent to <> P of TLA+:

eventually(P)
P.eventually

Mode: Temporal.

Expression next(e) is equivalent to e' of TLA+. More precisely, if f is the translation of a Quint expression e to TLA+, then f' is the translation of e' to TLA+. In contrast to TLA+, we restrict next to the Temporal mode. Hence, we cannot use next in actions. In actions, we should only use x' = e.

Mode: Temporal.

Unchanged (removed)

For a state variable x, the following expression is like UNCHANGED x of TLA+:

unchanged(x)
x.unchanged

In a more general case, you can write unchanged(e) for an expression e. However, you can also write next(e) = e, so there is no real reason for keeping this operator.

Discussion. After introducing modes, we have realized that it became easy to identify assignments in actions. We introduced Unchanged only in the Temporal mode, which is needed for refinements.

OrKeep

The following operator is similar to [A]_x of TLA+:

orKeep(A, x)
A.orKeep(x)

The arguments to orKeep are as follows:

A is an expression in the Action mode,
x is a variable or a tuple of variables.

Mode: Temporal, Run. This operator converts an action (in the Action mode) to a temporal property or a run.

MustChange

The following operator is similar to <A>_x of TLA+:

mustChange(A, x)
A.mustChange(x)

The arguments to mustChange are as follows:

A is an expression in the Action mode,
x is a variable or a tuple of variables.

Mode: Temporal. This operator converts an action (in the Action mode) to a temporal property.

Enabled

This operator is written as follows:

enabled(A)
A.enabled

Similar to the operator ENABLED of TLA+, the operator enabled is a very special operator. It accepts an expression A in the action mode, whereas enabled(A) is an expression in the Temporal mode.

Expression enabled(A) is equivalent to ENABLED A of TLA+. More precisely, if B is the translation of a Quint expression A to TLA+, then ENABLED B is the translation of enabled(A) to TLA+.

Mode: Temporal. The argument A must be in the Action mode.

Fairness

This is equivalent to WF_e(A) of TLA+:

weakFair(A, e)
A.weakFair(e)

This is equivalent to SF_e(A) of TLA+:

strongFair(A, e)
A.strongFair(e)

The second argument e is either a name, or a tuple of names, as in unchanged.

Mode: Temporal. The argument A must be in the Action mode.

Other temporal operators

We omit P \leadsto Q, as it can be written as:

always(P implies eventually(Q))

TLA+ contains an interesting operator "guarantees", that is written as P -+-> Q. For completeness, we introduce its syntactic version in Quint:

guarantees(P, Q)
P.guarantees(Q)

The operators \EE and \AA are almost never used, so there are no equivalents in Quint. If you have reached this level, you should (automatically) translate your Quint spec into TLA+ and use your tools, e.g., TLAPS.

Unbounded quantifiers

TLA+ has three operators that bind a variable without providing a set:

\E x: P
\A x: P
CHOOSE x: P

These operators are supported neither by TLC, nor by Apalache. So the chance that you will use them is very low. However, for the sake of completeness we introduce their counterparts in Quint:

existsConst(x => P)
forallConst(x => P)
chooseConst(x => P)

We add the suffix "const" to the operator names to stress the fact that these operators quantify over the constants of the first-order universe.

Mode: Stateless, State, Temporal. No Action mode.

Instances

WARNING: Instances are not supported yet. See #528 and #237.

Given a stateful module M, we can turn M into another module I by rewriting constants and variables of M. In this case, module I is called an instance of M.

Common case 1

The most common example is shown below:

// in Voting.qnt
  module Voting {
    const Value: Set[int]
    const Acceptor: Set[str]
    const Quorum: Set[Set[str]]
    // no const, no var below
    // ...
    val chosen = Value.filter(v => Ballot exists (b => ChosenAt(b, v)))
    // ...
  }

// in MC.qnt
  module MC {
    val Acceptor = Set("p1", "p2", "p3")
    val Quorum = MC_Acceptor.powerset.filter(Q => Q.size > 1)

    // an instance of Voting that has the name "V"
    module V = Voting(Value = Set(0, 1), Acceptor = Acceptor, Quorum = Quorum)
    // ...
  }

In the above example, module V is produced from the module Voting by replacing every occurrence of Value, Acceptor, and Quorum with Set(0, 1), Acceptor, and Quorum, respectively.

We can shorten identity substitutions Acceptor = Acceptor and Quorum = Quorum by writing:

    module V = Voting(Value = Set(0, 1), *)

Common case 2

Another common example is to rename variables:

module root {
  module XY {
    var x: int
    var y: int

    action Init = all {
      x' = 0,
      y' = 0
    }

    action Next = all {
      x' = x + 1,
      y' = y + 2
    }
  }

  var a: int
  var b: int

  module AB = XY(x = a, y = b)
}

In this case, our substitution is a bijection: No two variables are mapped on the same variable. Hence, the module AB will look like follows:

  module AB = {
    action Init = all {
      a' = 0,
      b' = 0
    }

    action Next = all {
      a' = a + 1,
      b' = b + 2
    }
  }

The general case

We may instantiate a module by substituting state variables with expressions over other variables. Consider the following example:

module root {
  module Counters {
    var x: int
    var y: int

    action Init = all {
      x' = 1,
      y' = 0
    }

    action Next = all {
      x' = x + 1,
      y' = x
    }
  }

  module MyCounters {
    var x: int

    module C = Counters(x = x, y = x - 1)
  }
}

In the above example, we produce the stateless module C from the stateful module Counters by replacing x with x and y with x - 1. How is that even possible in the presence of updates? Here is how module C would look like after instantiation:

module C = {
  temporal Init =
    (x == 1) and (x - 1 == 0)

  temporal Next =
    (next(x) == x + 1) and (next(x - 1) == x)
}

The trick here is that since an expression like x - 1 = x does not have meaningful semantics, we upgrade all actions to temporal formulas and use next(e1) = e2 instead of e1 = e2. At this point, we are in the realm of expressions that look very much like TLA+ formulas, just using a slightly different syntax. Most likely, we just want to get C transpiled into TLA+ and write some proofs in TLAPS.

No anonymous instances

TLA+ allows one to instantiate a module and inject its definitions directly in the namespace of another module, e.g.:

------ MODULE Bar -------
VARIABLE x
A(y) == x + y
=========================

------- MODULE Foo ------
VARIABLE z
INSTANCE Bar WITH x = z
=========================

Quint does not provide syntax sugar for doing that. If you want to achieve something similar in Quint, then you can use import as follows:

// Bar.qnt
module Bar {
  var x: int
  def A(y) = x + y
}

// Foo.qnt
module Foo {
  var z: int

  module _FooBar = Bar(x = z)
  import _FooBar.*
}

Our solution is not exactly equivalent to the TLA+ specification: We had to explicitly introduce the name _FooBar for the module. By convention, other modules should not access names that start with underscore (_). Should this happen, a Quint parser may issue a warning.

Discussion

There are two ways to load definitions in TLA+: by writing EXTENDS and by writing INSTANCE (anonymous or named). See Specifying Systems (Ch. 11.1). Apparently, EXTENDS and anonymous instances are needed to define fancy operators, e.g.:

---- MODULE Foo ----
x (+) y == { x, y }
====================

---- MODULE Bar ----
INSTANCE Foo

G == 1 (+) 2
====================

We could use a named instance:

---- MODULE Baz ----
F == INSTANCE Foo

G == F!(+)(1, 2)
====================

Obviously, the expression in Baz!G is not as visually appealing as the expression in Bar!G. Another issue is that anonymous instance do not allow for duplication of definitions, even if those definitions are equivalent. For this reason, one has to use LOCAL INSTANCE or EXTENDS.

There is probably some history behind EXTENDS, anonymous INSTANCE, and LOCAL INSTANCE in TLA+. A yet another use of EXTENDS in TLA+ is to define the module Integers that extends the operators of the module Naturals. Quint does not have this issue, as integers are simply built-in in the language. We do not have the bearing of history in Quint and thus we can simplify namespaces and instances.

Files

lang.md

Latest commit

History

lang.md

File metadata and controls

Summary of Quint

Identifiers and strings

Comments

Types

Type System 1.2

Modes

Module-level constructs

Module definition

Constant declarations

Assumptions

Variable definitions

Operator definitions

No recursive functions and operators

Module instances

Type aliases

Theorems

Imports

Namespaces and imports

Stateless and stateful modules

Namespaces

Imports

Quint expression syntax

Literals

Names

Braces and parentheses

Lambdas (aka Anonymous Operators)

Two forms of operator application

Boolean operators and equality

Block disjunctions

Block conjunctions

Flow operators

Condition

Cases (removed)

Sets

Set constructor

Non-deterministic choice

Other set operators

Maps (aka Functions)

Records

Discriminated unions

Tuples

Lists (aka Sequences)

Integers

Nested operator definitions

Operators on actions

Delayed assignment

Non-deterministic choice

Assert

Runs

Then

Repeated

Fail

Temporal operators

Always

Eventually

Next

Unchanged (removed)

OrKeep

MustChange

Enabled

Fairness

Other temporal operators

Unbounded quantifiers

Instances

Common case 1

Common case 2

The general case

No anonymous instances

Discussion