A collection of various TLA+ examples and helper functions for learning.
Use Print operator defined in standard module TLC.
EXTENDS TLC
/\ Print(<<"Hello world">>, TRUE)Result:
<<"Hello world">>Create a set.
/\ {1, 2, 3, 3, 4}Result:
{1, 2, 3, 4}N..M is set of all numbers between N and M.
EXTENDS Integers
/\ 1..5Result:
1..5Check if set S contains value x with x \in S.
EXTENDS Integers
/\ 2 \in {1, 2, 3}
/\ 4 \in 1..3Result:
TRUE
FALSE{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}{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}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:
7Get 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:
4Get the difference of two sets.
EXTENDS Integers
VARIABLE S, T
/\ S = (10..20)
/\ T = (1..14)
/\ S \ T{15, 16, 17, 18, 19, 20}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
FALSECreate a sequence.
/\ <<1, 2, 3>>Append to a sequence.
EXTENDS Sequences
VARIABLE S
/\ S = <<1>>
/\ S \o <<2>>Result:
<<1, 2>>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:
6Add local definitions to an expression.
EXTENDS Integers
/\ LET x == 1
y == 2
z == 3
IN <<x + y + z>>Result:
6True is value is even.
EXTENDS Integers
IsEven(x) == x % 2 = 0
/\ IsEven(2)Result:
TRUETrue is value is odd.
EXTENDS Integers
IsOdd(x) == x % 2 = 1
/\ IsOdd(2)Result:
TRUEGet a random integer within a range.
EXTENDS Integers
/\ RandomElement(1..100)Result:
56Pull requests are welcome!
For contributions please create a new branch and submit a pull request for review.