TLA+ Cookbook

A collection of various TLA+ examples and helper functions for learning.

Examples

Print

Use Print operator defined in standard module TLC.

EXTENDS TLC

/\ Print(<<"Hello world">>, TRUE)

Result:

<<"Hello world">>

Print.tla

Set

Create a set.

/\ {1, 2, 3, 3, 4}

Result:

{1, 2, 3, 4}

Range Set

N..M is set of all numbers between N and M.

EXTENDS Integers

/\ 1..5

Result:

1..5

RangeSet.tla

Set Contains

Check if set S contains value x with x \in S.

EXTENDS Integers

/\ 2 \in {1, 2, 3}
/\ 4 \in 1..3

Result:

TRUE
FALSE

SetContains.tla

Filter set

{v \in S : P} is the subset of S consising of all v satisfying P. P must resolve to a boolean.

EXTENDS Integers

/\ S = {1, 2, 3, 4, 5}
/\ {v \in S : v > 3}

Result:

{4, 5}

FilterSet.tla

Map set

{e : v \in S} is the set of all e for v in S. The function e is applied to every element in set.

EXTENDS Integers

/\ S = {1, 2, 3, 4, 5}
/\ {v^2: v \in S}

Result:

{1, 4, 9, 16, 25}

MapSet.tla

Largest number is Set

Get the largest element in set.

EXTENDS Integers

Maximum(S) == IF S = {} THEN -1 ELSE CHOOSE x \in S: \A y \in S: y <= x

/\ Maximum({4, 7, 5})

Result:

7

SetLargestNumber.tla

Smallest number is Set

Get the smallest element in set.

EXTENDS Integers

Maximum(S) == IF S = {} THEN -1 ELSE CHOOSE x \in S: \A y \in S: y <= x

/\ Maximum({4, 7, 5})

Result:

4

SetSmallestNumber.tla

Set difference

Get the difference of two sets.

EXTENDS Integers
VARIABLE S, T

/\ S = (10..20)
/\ T = (1..14)
/\ S \ T

{15, 16, 17, 18, 19, 20}

SetDifference.tla

Set common

Asserts that any two elements of T have an element in common.

VARIABLE T

/\ T = {{1, 2}, {1, 3}, {2, 3}}
/\ R = {{1, 1}, {1, 3}, {2, 3}}

/\ \A X, Y \in T : X \cap Y # {}
/\ \A X, Y \in R : X \cap Y # {}

Result:

TRUE
FALSE

SetCommon.tla

Sequences

Create a sequence.

/\ <<1, 2, 3>>

Append To Sequence

Append to a sequence.

EXTENDS Sequences
VARIABLE S

/\ S = <<1>>
/\ S \o <<2>>

Result:

<<1, 2>>

SequenceAppend.tla

Sum Sequence

Sum all values of a sequence.

EXTENDS Integers, Sequences

SumSeq(S) ==
  LET seq == S
    Sum[i \in 1..Len(seq)] == IF i = 1 THEN seq[i] ELSE seq[i] + Sum[i-1]
  IN IF seq = <<>> THEN 0 ELSE Sum[Len(seq)]

/\ SumSeq(<<1, 2, 3>>)

Result:

6

SumSequence.tla

Local variables

Add local definitions to an expression.

EXTENDS Integers

/\ LET x == 1
       y == 2
       z == 3
   IN <<x + y + z>>

Result:

6

LocalVariables.tla

Is even

True is value is even.

EXTENDS Integers

IsEven(x) == x % 2 = 0

/\ IsEven(2)

Result:

TRUE

IsEven.tla

Is odd

True is value is odd.

EXTENDS Integers

IsOdd(x) == x % 2 = 1

/\ IsOdd(2)

Result:

TRUE

IsOdd.tla

Random Integer

Get a random integer within a range.

EXTENDS Integers

/\ RandomElement(1..100)

Result:

56

RandomIntegers.tla

Contributing

Pull requests are welcome!

For contributions please create a new branch and submit a pull request for review.

License

MIT