# 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. A sequence is like a list in any other language. You write it like `<<a, b, c>>`

, and the elements can be any other values (including other sequences).
Check the related section on sequences.

- Seq(set)
The set of all sequences where the values are all elements of

`set`

. TLC has special code to check if you’re testing membership, this is not memory/cpu intensive. Cannot be enumerated by TLC (used in a quantifier or a CHOOSE), but can be used for membership checking.<<a>> \in Seq({a, b}) <<a, b>> \in Seq({a, b}) <<a, b, b, a>> \in Seq({a, b}) \* in practice, the output is a set that contains all sequences made from 'a's and 'b's, \* so it also includes the sequence <<a, a, a, a, b, a, b>> for example. That's why it's nonenumerable.

- Len(seq)
Length of

`seq`

.Len(<<2, 4, 6>>) = 3

- Head(seq)
First element of

`seq`

.Head(<<1, 2, 3>>) = 1

- Tail(seq)
All but first element of

`seq`

.Tail(<<1, 2, 3>>) = <<2, 3>>

`seq1 \o seq2`

Concatenates two sequences.

<<1>> \o <<2 , 3>> = <<1, 2, 3>>

- Append(seq, e)
Append

`e`

at the end of`seq`

. Equivalent to`seq1 \o <<e>>`

.Append(<<1, 2>>, 3) = <<1, 2, 3>>

- SubSeq(seq, m, n)
Used to select the subsequence

`<<s[m], s[m+1], ... , s[n]>>`

in seq. Indices are inclusive. [taken from docs]SubSeq(<<7, 8, 9>>, 1, 2) = <<7, 8>>

- SelectSeq(seq, Op(_))
Sequence filter using Op.

IsEven(x) == x % 2 SelectSeq(<<1, 2, 3>>, IsEven) = <<2>>

## FiniteSets¶

- IsFiniteSet(set)
Tests if

`set`

is not an infinite set.IsFiniteSet({2, 5, 7}) = TRUE IsFiniteSet(Seq({1})) = FALSE IsFiniteSet(Nat) = FALSE

- Cardinality(set)
The number of elements in

`set`

.Cardinality({2, 5, 7}) = 3

## 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.IsABag([a |-> 3, b |-> 7]) = TRUE

- BagToSet(bag)
Equivalent to

`DOMAIN bag`

.BagToSet([a |-> 3, b |-> 7]) = {"a", "b"}

- SetToBag(set)
Equivalent to

`[x \in set |-> 1]`

.SetToBag({}) = <<>> SetToBag({"a","b"}) = [a |-> 1, b |-> 1] SetToBag({"a", "b", "a", "a"}) = [a |-> 1, b |-> 1]

- BagIn(e, bag)
Equivalent to

`e \in DOMAIN bag`

.BagIn("a", [a |-> 1, b |-> 1]) = TRUE BagIn("c", [a |-> 1, b |-> 1]) = FALSE

- EmptyBag
Equivalent to

`<<>>`

.EmptyBag = <<>>

`bag1 (+) bag2`

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

[a |-> 1, b |-> 3] (+) EmptyBag = [a |-> 1, b |-> 3] [a |-> 1, b |-> 3] (+) [a |-> 1] = [a |-> 2, b |-> 3] [a |-> 1, b |-> 3] (+) [c |-> 1] = [a |-> 1, b |-> 3, c |-> 1]

`bag1 (-) bag2`

Bad subtraction. If

`bag2[e] >= bag1[e]`

, then`e`

is dropped from the final bag’s keys.\* Nothing changes: [a |-> 1, b |-> 3] (-) EmptyBag = [a |-> 1, b |-> 3] \* a is removed from the bag: [a |-> 1, b |-> 3] (-) [a |-> 1] = [b |-> 3] \* a is decreased by the amount of the second bag: [a |-> 2, b |-> 3] (-) [a |-> 1] = [a |-> 1, b |-> 3] \* c is not in the domain of the bag on the left, hence nothing changes: [a |-> 1, b |-> 3] (-) [c |-> 1] = [a |-> 1, b |-> 3]

- BagUnion(set)
Equivalent to

`bag1 (+) bag2 (+) ...`

, where`set = {bag1, bag2, ...}`

.BagUnion({}) = <<>> BagUnion({[a |-> 2]}) = [a |-> 2] BagUnion({[a |-> 2], [b |-> 3]}) = [a |-> 2, b |-> 3]

`B1 \sqsubseteq B2`

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

[a |-> 2, b |-> 3] \sqsubseteq [b |-> 2] = FALSE [a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 2] = FALSE [a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 3] = TRUE \* it doesn't matter if B2 has "c |-> 1", because has enough copies of a and b. [a |-> 2, b |-> 3] \sqsubseteq [a |-> 2, b |-> 3, c |-> 1] = TRUE [a |-> 2, b |-> 3] \sqsubseteq [a |-> 5, b |-> 3, c |-> 1] = TRUE

- SubBag(bag)
The set of all subbags of

`bag`

.SubBag(EmptyBag) = {<<>>} SubBag([a |-> 2]) = {<<>>, [a |-> 1], [a |-> 2]}

- BagOfAll(Op(_), bag)
If

`bag[e] = x`

, then`out[Op(e)] = x`

. egb == <<1, 3, 5>> >>> BagOfAll(LAMBDA x: x^2, b) (1 :> 1 @@ 4 :> 3 @@ 9 :> 5)

- BagCardinality(bag)
The sum of all values in

`bag`

.BagCardinality(EmptyBag) = 0 BagCardinality([a |-> 2]) = 2 BagCardinality([a |-> 5, b |-> 3, c |-> 1]) = 9

- CopiesIn(e, bag)
If

`e`

is in`bag`

, then`bag[e]`

, otherwise 0.CopiesIn("a", EmptyBag) = 0 CopiesIn("a", [a |-> 5, b |-> 3]) = 5

## 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)`

.- Any
`x \in Any`

for*any*value`x`

. Don’t use this as part of a`Spec`

, but it’s occasionally useful for modeling properties.- 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.

`TLCGet("level")`

can be used to bound an unbound model.- 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.

## Randomization¶

This module defines operators for choosing pseudo-random subsets of a set. If you use this, **TLC will not check all possible states.** For example, consider the spec

```
EXTENDS Integers, TLC, Randomization
VARIABLE x
Init ==
/\ x = 0
Next ==
\/ /\ x = 0
/\ x' \in {1, 2, 3}
\/ /\ PrintT(x)
/\ UNCHANGED x
\* Magic magic magic
Spec == Init /\ [][Next]_x
```

Running this will print the numbers {0, 1, 2, 3}. If we replace `{1, 2, 3}`

with `RandomSubset(2, {1, 2, 3})`

, then it will only print two of those three numbers, and *which two* may change from run to run. This makes `Randomization`

useful for optimization, but you need to be careful.

- RandomSubset(k, S)
Returns a random size-k subset of S.

RandomSubset(1, {"a"}) = {"a"} \* Running multiple times will yield different subsets RandomSubset(2, {"a", "b", "c"}) = {"b", "c"} RandomSubset(2, {"a", "b", "c"}) = {"a", "c"}

- RandomSetOfSubsets(k, n, S)
Selects k random subsets of S, where each random subset has

*on average*n elements. Since this process may result in some duplicate subsets, the operator can potentially return fewer than k subsets. This can also potentially return the empty set.RandomSetOfSubsets(1, 1, {"a"}) = {{"a"}} \* Each element has a 3-in-5 chance of appearing in each subset RandomSetOfSubsets(2, 3, {"a", "b", "c", "d", "e"}) = {{"a", "d", "c"}, {"a", "b", "e", "c"}} RandomSetOfSubsets(2, 3, {"a", "b", "c", "d", "e"}) = {{"a", "e"}, {"d", "e", "b", "c"}} \* Fewer than 4 results because it generated a duplicate RandomSetOfSubsets(4, 1, {"a", "b"}) = {{}, {"b"}, {"a", "b"}}

- TestRandomSetOfSubsets(k, n, S)
Calls

`RandomSetOfSubsets(k, n, s)`

five times and returns the number of unique sets returned each time.TestRandomSetOfSubsets(1, 1, {"a"}) = <<1, 1, 1, 1, 1>> \* Different executions will yield different results: TestRandomSetOfSubsets(3, 4, {"a", "b", "c", "d", "e"}) = <<3, 3, 2, 2, 2>>