Standard Modules

This only includes models that are usable by TLC. Reals and RealTime are not covered.

Naturals

Defines + - * ^ % < > <= >= as well as

Nat

The set {0, 1, ...}. Cannot be enumerated by TLC (used in a quantifier or a CHOOSE), but can be used for membership checking.

a..b

The set {a, a + 1, ..., b}.

a \div b

Floor division: 10 \div 3 = 3.

Integers

Defines everything in Naturals as well as

Int

The set of all integers. Cannot be enumerated by TLC (used in a quantifier or a CHOOSE), but can be used for membership checking.

-a

Negative numbers.

Sequences

Required for pluscal procedures.

Seq(set)

The set of all sequences where the values are all elements of set. Cannot be enumerated by TLC (used in a quantifier or a CHOOSE), but can be used for membership checking.

Len(seq)

Length of seq.

Head(seq)

First element of seq.

Tail(seq)

All but first element of seq.

seq1 \o seq2

Sequence concatination.

Append(seq, e)

Equivalent to seq1 \o <<e>>.

SubSeq(seq, m, n)

The sequence <<s[m], s[m+1], ... , s[n]>>. [taken from docs]

SelectSeq(seq, Op(_))

Sequence filter.

FiniteSets

IsFiniteSet(set)

Tests if set is not an infinite set.

Cardinality(set)

The number of elements in set.

Bags

Also known as multisets. Bags are functions items to “counts” of items. IE the struct [a |-> 1, b |-> 2] is a bag. The values of a bag must be positive integers.

IsABag(func)

Tests if func is a bag.

BagToSet(bag)

Equivalent to DOMAIN bag.

SetToBag(set)

Equivalent to [x \in set |-> 1].

BagIn(e, bag)

Equivalent to e \in DOMAIN bag.

EmptyBag

Equivalent to <<>>.

bag1 (+) bag2

Bag addition. Creates a new bag where each key is the sum of the values of that key in each bag.

bag1 (-) bag2

Bad subtraction. If bag2[e] >= bag1[e], then e is dropped from the final bag’s keys.

BagUnion(set)

Equivalent to bag1 (+) bag2 (+) ..., where set = {bag1, bag2, ...}.

B1 \sqsubseteq B2

B1 sqsubseteq B2 iff, for all e, bag B2 has at least as many copies of e as bag B1 does. [taken from docs]

SubBag(bag)

The set of all subbags of bag.

BagOfAll(Op(_), bag)

If bag[e] = x, then out[Op(e)] = x. eg

b == <<1, 3, 5>>
>>> BagOfAll(LAMBDA x: x^2, b)

(1 :> 1 @@ 4 :> 3 @@ 9 :> 5)
BagCardinality(bag)

The sum of all values in bag.

CopiesIn(e, bag)

If e is in bag, then bag[e], otherwise 0.

TLC

Required for PlusCal assert. Many of the operators in TLC break core assumptions about TLA+, such as referential transparency. Use with caution!

a :> b

The function [x \in {a} |-> b].

func1 @@ func2

Function merge. If two functions share the same key, uses the value from func1 (NOT func2).

Permutations(set)

The set of all functions that act as permutations of set. eg

>>> Permutations({"a", "b"})

{[b |-> "b", a |-> "a"],
 [b |-> "a", a |-> "b"]}
SortSeq(seq, Op(_, _))

Sorts the sequence with comparator Op.

ToString(val)

String conversion.

JavaTime

The current epoch time.

Print(val, out)

Prints ToString(val), and evaluates to out as an expression.

PrintT(val)

Equivalent to Print(val, TRUE).

Assert(bool, errmsg)

If bool is false, then terminates model checking with errmsg. Otherwise, evaluates to TRUE.

RandomElement(set)

Randomly pulls an element from set. The value can be different on different runs!

TLCEval(v)

Evaluates the expression v and caches the result. Can be used to speed up recursive definitions.

TLCGet(val)

val can be either an integer or a string. If an integer, retrieves the value from the corresponding TLCSet. If a string, retrieves statistics from the current model run. The following strings are valid:

  • “queue”

  • “generated”

  • “distinct”

  • “duration”: number of seconds elapsed since the beginning of model checking

  • “level”: the length of the current behavior

  • “diameter”: the length of the longest global behavior

  • “stats”: all of the global stats (everything excluding “level”), as a struct.

TLCSet(i, val)

Sets the value for TLCGet(i). i must be a positive integer. TLCSet can be called multiple times in the same step.

Note

Each TLC worker thread carries a distinct “cache” for the values of TLCGet(i). As such, it’s generally inadvisable to use TLCSet to profile information that lasts beyond a single step.

TLCSet statements evaluated during the initial state, however, will be propagated to all workers.

TLCExt

AssertEq(a, b)

Equivalent to a = b, except that if a # b, it also prints the values of a and b. This does not terminate model checking!

AssertError(str, exp)

True if exp doesn’t throw an error, or if exp throws an error that exactly matches str. False otherwise.

Note

AssertError catches the thrown error, meaning model checking will continue.

Trace

Returns the “history” of the current behavior, as a sequence of structs.

TLCModelValue(str)

Creates a new model value with name str. Can only be used in constant definitions, as part of an ordinary assignment.

CONSTANT Threads <- {
  TLCModelValue(ToString(i)): i \in 1..3
}

Json

ToJson(val)

Converts val to a JSON string. Sets and sequences are encoded as arrays, functions are encoded as objects with string keys.

>>> ToJson(1..3)
"[1,2,3]"

>>> ToJson([x \in 0..2 |-> x^2])

"{\"0\":0,\"1\":1,\"2\":4}"

Multi-arity functions are encoded with keys that use the TLA+ tuple notation.

>>> ToJson([p, q \in BOOLEAN |-> p => q])

"{\"<<FALSE, FALSE>>\":true,
  \"<<TRUE, FALSE>>\":false,
  \* ...
JsonSerialize(absoluteFilename, value)

Exports value as a JSON object to a file.

JsonDeserialize(absoluteFilename)

Imports a JSON object from a file.