TLX.Sets
(TLX v0.5.2)
Copy Markdown
Set operation constructors for use in TLA+ expressions.
These functions build tagged tuples that the emitters translate to TLA+ set syntax.
union(a, b) # a \union b
intersect(a, b) # a \intersect b
difference(a, b) # a \ b
subset(a, b) # a \subseteq b
cardinality(s) # Cardinality(s)
set_of([e1, e2]) # {e1, e2}
in_set(elem, s) # elem \in s
set_map(:x, :set, expr) # {expr : x \in set}
power_set(s) # SUBSET s
distributed_union(s) # UNION sSummary
Functions
Set cardinality: Cardinality(s)
Set difference: a \ b (elements in a but not in b)
Distributed union: UNION s — flatten a set of sets.
Set comprehension (filter): {var \in set : expr} in TLA+.
Set membership test: elem \in s
Set intersection: a \intersect b
Power set: SUBSET s — the set of all subsets of s.
Set image/map: {expr : var \in set} in TLA+.
Set literal: {e1, e2, ...}
Subset relation: a \subseteq b
Set union: a \union b
Functions
Set cardinality: Cardinality(s)
Set difference: a \ b (elements in a but not in b)
Distributed union: UNION s — flatten a set of sets.
Set comprehension (filter): {var \in set : expr} in TLA+.
Set membership test: elem \in s
Set intersection: a \intersect b
Power set: SUBSET s — the set of all subsets of s.
Set image/map: {expr : var \in set} in TLA+.
Set literal: {e1, e2, ...}
Subset relation: a \subseteq b
Set union: a \union b