Types

Primitive types

Range types

L..H — integers from L to H inclusive.

var count: 0..10        // values 0, 1, 2, ..., 10
var phase: 0..3         // values 0, 1, 2, 3
const N: 1..5           // N can be 1 through 5

Ranges can use constants:

const N: Int
var index: 0..N         // depends on the value of N at check time

Range expressions in parameters cannot use arithmetic. Use a constant instead:

// Invalid
action Act(i: 0..N+1) { ... }

// Valid
const LIMIT: Int
action Act(i: 0..LIMIT) { ... }

Compound types

Set[T]

Finite sets.

var voters: Set[Int]
init { voters = {} }                          // empty set
init { voters = {1, 2, 3} }                   // literal
init { voters = {x in 0..N if active[x]} }    // comprehension

Seq[T]

Ordered sequences (0-indexed).

var log: Seq[Int]
init { log = [] }                  // empty
init { log = [1, 2, 3] }          // literal

Dict[K, V]

Maps from keys to values. The primary data structure for modelling per-process state.

var role: Dict[Int, Int]
init { role = {p: 0 for p in 0..N} }    // comprehension

See the dedicated Dicts page for full details.

Option[T]

Optional values.

var leader: Option[Int]
init { leader = None }

action Elect(i: 0..N) {
    leader = Some(i)
}

(T1, T2) — Tuples

var pair: (Int, Bool)
init { pair = (0, true) }

Type aliases

Give a name to a type expression for readability:

type NodeId = 0..N
type Role = 0..2
type Log = Seq[Int]

var currentTerm: Dict[NodeId, Nat]
var role: Dict[NodeId, Role]
var log: Dict[NodeId, Log]