CHOOSE x ∈ S : P(x) — deterministic selection.

Returns the least satisfying element in Erlang term order. TLA+ requires only that CHOOSE be a function of its arguments, not that it pick any particular element, so any total order will do — but it must be an order that does not depend on how the set was built or which OTP release is running. Enumeration order is not such an order, and a CHOOSE that varied between runs would make the reachable state graph, and every result read from it, vary between runs.

Raises ArgumentError if no element satisfies the predicate; CHOOSE over an empty set is undefined in TLA+ and silently returning nil would put an unspecified value into a state variable.

iex> ExTLA.Set.choose(MapSet.new([3, 1, 2]))
1

iex> ExTLA.Set.choose(MapSet.new([3, 1, 2]), &(&1 > 1))
2

S1 \X S2 — Cartesian product. The set of all tuples {a, b} where a ∈ S1 and b ∈ S2.

iex> ExTLA.Set.cross(MapSet.new([1, 2]), MapSet.new([:a]))
MapSet.new([{1, :a}, {2, :a}])

N-ary Cartesian product: S1 \X S2 \X ... \X Sn.

The product of no sets is the set containing the empty tuple, not the empty set. The empty tuple is the identity of the product: appending the factors one at a time has to start from one empty combination, or nothing is ever built. The empty set is what any empty factor gives.

This is the independent product, a fixed list of sets. ExTLA.ModelChecker.bindings/3 is a different operation: each parameter's values may depend on the state and on the parameters bound before it.

iex> ExTLA.Set.cross_many([MapSet.new([1, 2]), MapSet.new([:a, :b])]) |> MapSet.size()
4

iex> ExTLA.Set.cross_many([])
MapSet.new([{}])

UNION S — distributed union. Flattens a set of sets.

iex> ExTLA.Set.distributed_union(MapSet.new([MapSet.new([1, 2]), MapSet.new([2, 3])]))
MapSet.new([1, 2, 3])

\E x \in S : P(x) — check if the predicate holds for at least one element.

False for the empty set.

iex> ExTLA.Set.exists?(MapSet.new([1, 2]), &(&1 > 1))
true

Set filtering: {x ∈ S : P(x)}.

iex> ExTLA.Set.filter(MapSet.new([1, 2, 3, 4]), &(rem(&1, 2) == 0))
MapSet.new([2, 4])

\A x \in S : P(x) — check if the predicate holds for all elements.

Vacuously true for the empty set.

iex> ExTLA.Set.for_all?(MapSet.new([2, 4]), &(rem(&1, 2) == 0))
true

Set mapping: {f(x) : x ∈ S}.

The result may be smaller than the input — a non-injective f collapses elements, exactly as in TLA+.

iex> ExTLA.Set.map(MapSet.new([1, 2, 3]), &rem(&1, 2))
MapSet.new([0, 1])

SUBSET S — the power set (set of all subsets).

Warning: exponential in |S|. Use with small sets only — a 20-element set has a million subsets, and each one is a MapSet.

iex> ExTLA.Set.powerset(MapSet.new([1, 2])) |> Enum.sort_by(&MapSet.size/1)
[MapSet.new([]), MapSet.new([1]), MapSet.new([2]), MapSet.new([1, 2])]

Integer range as a MapSet: a..b.

Empty when a > b, as in TLA+.

iex> ExTLA.Set.range(1, 3)
MapSet.new([1, 2, 3])

iex> ExTLA.Set.range(3, 1)
MapSet.new([])