Functions available inside action, init, invariant, terminal and
action_property blocks. use ExTLA.Spec imports this module whole, so this list
is a spec body's vocabulary.
Two kinds of name live here, and the difference is the point.
Thin wrappers over a standard Elixir function. set/1, put/2, union/2,
len/1, sum/1 and the rest are one-line covers over MapSet and Enum.
They exist for readability rather than capability — len(buffer) and
sum(values(balances)) read as the TLA+ they translate, and a spec author
writing MapSet.size/1 directly gets the same result.
Delegations to the foundation. Every set-theoretic and function operator
ExTLA provides is reachable from a spec body unqualified, and every one of
them is a defdelegate to ExTLA.Set or ExTLA.Function. This module holds no
second implementation of any of them, so a spec body and code calling those
modules directly cannot get different answers.
Every one of these is total and deterministic, which is the whole design: an
action body must be a pure deterministic function of (pre_state, params)
(02-dsl-semantics.md §3), so nothing here may branch the search, read the
clock, or depend on anything but its arguments.
Where a name would silently produce a wrong answer on a missing key, it
raises instead: update/3, head/1 and tail/1 all fail loudly. A nil
standing in for a value that is not there would flow into guards and states
and let the checker explore states the spec does not describe.
Summary
Functions
TLA+: Append(s, e).
TLA+: f[x] — function application, which is what f[x] compiles to inside
every spec block (02-dsl-semantics.md §1.6).
CHOOSE x \\in S : P(x) — deterministically select an element satisfying the
predicate. Returns the same element for the same set and predicate; raises if
none satisfies it.
TLA+: S1 \\X S2 — the Cartesian product.
TLA+: S1 \\X S2 \\X ... \\X Sn, over a list of sets.
TLA+: S \\ {e}.
TLA+: S \\ T.
TLA+: UNION S — the distributed union of a set of sets.
TLA+: DOMAIN f, as a set.
TLA+: [f EXCEPT ![a] = v, ![b] = w] — several points at once.
TLA+: \\E x \\in S : P(x). False for the empty set.
TLA+: \\A x \\in S : P(x). Vacuously true for the empty set.
TLA+: [x \\in S |-> f(x)] — ExTLA.Function.construct/2 under the name a spec
body uses.
TLA+: [S -> T] — the set of all total functions from S to T.
|T|^|S| elements; see ExTLA.Function.function_set/2.
TLA+: Head(s). Raises on the empty sequence, where Head is undefined.
TLA+: S \\cap T.
TLA+: IsFiniteSet(S) — here, whether the term is a set at all.
The keys of a function, as a list.
TLA+: Len(s).
TLA+: e \\in S.
TLA+: SUBSET S — the power set. Exponential in |S|; see ExTLA.Set.powerset/1.
TLA+: S \\cup {e}.
TLA+: a..b as a set. Empty when a > b.
TLA+: [field1: S1, field2: S2] — the set of all such records.
The empty sequence. TLA+: <<>>.
A sequence from a list. TLA+: <<a, b, c>>.
The empty set. TLA+: {}.
A set from an enumerable. TLA+: {a, b, c}.
TLA+: {x \\in S : P(x)} — set filtering.
TLA+: {f(x) : x \\in S} — set mapping. The result may be smaller than the
input, exactly as in TLA+: a non-injective f collapses elements.
TLA+: Cardinality(S).
TLA+: SubSeq(s, m, n) — elements m through n inclusive, 1-indexed.
TLA+: S \\subseteq T.
The sum of an enumerable of numbers; 0 when empty.
The sum of f over an enumerable.
TLA+: Tail(s). Raises on the empty sequence, where Tail is undefined.
TLA+: S \\cup T.
TLA+: [f EXCEPT ![k] = g(@)] — ExTLA.Function.except_with/3 under the name a
spec body uses.
The values of a function, as a list.
Functions
TLA+: Append(s, e).
TLA+: f[x] — function application, which is what f[x] compiles to inside
every spec block (02-dsl-semantics.md §1.6).
A TLA+ function is undefined outside its domain, and a sequence is a function
on 1..Len(s), so both raise here rather than returning nil:
iex> ExTLA.Spec.Helpers.at(%{alice: 3, bob: 0}, :alice)
3
iex> ExTLA.Spec.Helpers.at([:a, :b, :c], 2)
:bAccess.get/2, which f[x] compiles to in ordinary Elixir, returns nil
outside the domain instead — and nil >= amount is true under Erlang term
order, so a guard reading a key it does not have would silently enable its
action and the checker would explore a state space the spec does not describe.
at/2, plus the source text of the collection expression for the message. The
rewriter has that text; a spec author calling at/2 by hand does not.
CHOOSE x \\in S : P(x) — deterministically select an element satisfying the
predicate. Returns the same element for the same set and predicate; raises if
none satisfies it.
It does NOT branch. Nondeterminism comes from params: only
(02-dsl-semantics.md §3): CHOOSE in TLA+ is a function of its arguments,
and a function returning one element cannot produce several successors.
Delegates to ExTLA.Set.choose/2, which fixes the choice as the least satisfying
element in Erlang term order.
iex> ExTLA.Spec.Helpers.choose(MapSet.new([3, 1, 2]), &(&1 > 1))
2TLA+: S1 \\X S2 — the Cartesian product.
TLA+: S1 \\X S2 \\X ... \\X Sn, over a list of sets.
TLA+: S \\ {e}.
TLA+: S \\ T.
TLA+: UNION S — the distributed union of a set of sets.
TLA+: DOMAIN f, as a set.
A sequence is a function on 1..Len(s) — that is what at/2 applies it as — so its
domain is that range.
iex> ExTLA.Spec.Helpers.domain(%{a: 1, b: 2})
MapSet.new([:a, :b])
iex> ExTLA.Spec.Helpers.domain([:x, :y, :z])
MapSet.new([1, 2, 3])TLA+: [f EXCEPT ![a] = v, ![b] = w] — several points at once.
TLA+: \\E x \\in S : P(x). False for the empty set.
TLA+: \\A x \\in S : P(x). Vacuously true for the empty set.
TLA+: [x \\in S |-> f(x)] — ExTLA.Function.construct/2 under the name a spec
body uses.
iex> ExTLA.Spec.Helpers.for_each(MapSet.new([:a, :b]), fn _ -> 0 end)
%{a: 0, b: 0}S is a set: a list is a sequence, and building a function over one would
silently deduplicate it, so it is refused by name.
TLA+: [S -> T] — the set of all total functions from S to T.
|T|^|S| elements; see ExTLA.Function.function_set/2.
TLA+: Head(s). Raises on the empty sequence, where Head is undefined.
TLA+: S \\cap T.
TLA+: IsFiniteSet(S) — here, whether the term is a set at all.
The keys of a function, as a list.
TLA+: Len(s).
TLA+: e \\in S.
TLA+: SUBSET S — the power set. Exponential in |S|; see ExTLA.Set.powerset/1.
TLA+: S \\cup {e}.
TLA+: a..b as a set. Empty when a > b.
TLA+: [field1: S1, field2: S2] — the set of all such records.
The empty sequence. TLA+: <<>>.
A sequence from a list. TLA+: <<a, b, c>>.
The empty set. TLA+: {}.
A set from an enumerable. TLA+: {a, b, c}.
TLA+: {x \\in S : P(x)} — set filtering.
TLA+: {f(x) : x \\in S} — set mapping. The result may be smaller than the
input, exactly as in TLA+: a non-injective f collapses elements.
TLA+: Cardinality(S).
TLA+: SubSeq(s, m, n) — elements m through n inclusive, 1-indexed.
iex> ExTLA.Spec.Helpers.subseq([:a, :b, :c, :d], 2, 3)
[:b, :c]n < m is the empty sequence, whatever m and n are — TLC's SubSeq(s, 2, 0) is <<>>
even for an empty s. Otherwise both bounds must lie in 1..Len(s), and one outside raises
ExTLA.Spec.DomainError the way at/2 does for the same off-by-one.
The indices are TLA+'s, not Elixir's: a zero or negative m does not wrap or count from the
end. Elixir's slice semantics would turn an off-by-one in a spec into a valid sequence that
is not the one the author wrote, silently — the exact shape at/2 refuses.
iex> ExTLA.Spec.Helpers.subseq([:a, :b, :c], 3, 2)
[]TLA+: S \\subseteq T.
The sum of an enumerable of numbers; 0 when empty.
The sum of f over an enumerable.
iex> ExTLA.Spec.Helpers.sum([{:a, 1}, {:b, 2}], fn {_, n} -> n end)
3TLA+: Tail(s). Raises on the empty sequence, where Tail is undefined.
TLA+: S \\cup T.
TLA+: [f EXCEPT ![k] = g(@)] — ExTLA.Function.except_with/3 under the name a
spec body uses.
Raises on a key outside the domain — see ExTLA.Function for why extending it
instead would be worse than failing.
The values of a function, as a list.