Sets are one of the most fundamental data structures in TLA+. Unlike programming languages, TLA+ is built on set theory.
{1, 2, 3} \* a set of numbers
{"a", "b", "c"} \* a set of strings
{} \* the empty set
x \in S \* x is a member of S
x \notin S \* x is NOT a member of S
| Operator | Meaning |
S \union T | Union — elements in S or T |
S \intersect T | Intersection — elements in both |
S \\ T | Set difference — elements in S but not T |
SUBSET S | Power set — all subsets of S |
S \subseteq T | S is a subset of T |
Cardinality(S) | Number of elements (needs FiniteSets) |
{x \in S : P(x)} \* elements of S satisfying predicate P
Example: {x \in 1..10 : x > 5} gives {6, 7, 8, 9, 10}
{f(x) : x \in S} \* apply f to each element of S
Example: {x * 2 : x \in 1..3} gives {2, 4, 6}
1..5 \* the set {1, 2, 3, 4, 5}The spec on the right demonstrates various set operations. Run TLC to verify the invariants.