TLA+ function operations. In TLA+, a function maps every element of its domain to a value. Elixir maps serve as the implementation.
"Total over its domain" is the property that matters, and it is why except/2
and except_with/3 raise on a point outside the domain rather than adding it:
[f EXCEPT ![a] = v] where a ∉ DOMAIN f is undefined in TLA+, and quietly
extending the domain would produce a state that no reachable spec behavior can
produce — while still being fingerprinted as if it were one.
This module holds the only implementation of each of these operators.
ExTLA.Spec.Helpers, which a spec body imports, delegates to it and defines
nothing of its own, so a spec body and direct callers always get the same
answer.
Summary
Functions
Construct a function: [x ∈ S ↦ expr(x)].
DOMAIN f — the domain of a function, as a set.
EXCEPT — update a function at specific points:
[f EXCEPT ![a] = v, ![b] = w].
EXCEPT with self-reference — update using the old value:
[f EXCEPT ![a] = @ + 1].
Function set: [S → T] — all total functions from S to T.
Record set: [field1: S1, field2: S2] — all records with fields drawn from the
respective sets.
Functions
Construct a function: [x ∈ S ↦ expr(x)].
iex> ExTLA.Function.construct(MapSet.new([1, 2]), &(&1 * 10))
%{1 => 10, 2 => 20}S is a set — a MapSet or a range. A list is a sequence, which is a
function on 1..Len(s) already, and building a function over one would
silently deduplicate it; a map is a function already. Both are refused by name,
the way ExTLA.Spec.Helpers.at/2 refuses a term that is neither. A spec body
spells this operator for_each/2, which is the name the message uses.
DOMAIN f — the domain of a function, as a set.
iex> ExTLA.Function.domain(%{a: 1, b: 2})
MapSet.new([:a, :b])A sequence is a function on 1..Len(s) — that is what ExTLA.Spec.Helpers.at/2
applies it as — so its domain is that range:
iex> ExTLA.Function.domain([:x, :y, :z])
MapSet.new([1, 2, 3])Anything else is refused by name rather than answered. A MapSet is a struct
and therefore a map, so taking its keys would answer a set with the struct's
own field names — a wrong answer that looks like an answer.
EXCEPT — update a function at specific points:
[f EXCEPT ![a] = v, ![b] = w].
Raises KeyError on a point outside the domain — see the module documentation.
iex> ExTLA.Function.except(%{a: 1, b: 2}, a: 9)
%{a: 9, b: 2}EXCEPT with self-reference — update using the old value:
[f EXCEPT ![a] = @ + 1].
iex> ExTLA.Function.except_with(%{a: 1}, :a, &(&1 + 1))
%{a: 2}Function set: [S → T] — all total functions from S to T.
Warning: |T|^|S| elements. Use with small sets: three processes over four
states is 64 functions, but five over four is already 1024.
iex> ExTLA.Function.function_set(MapSet.new([:a]), MapSet.new([0, 1]))
MapSet.new([%{a: 0}, %{a: 1}])
iex> ExTLA.Function.function_set(MapSet.new([]), MapSet.new([0, 1]))
MapSet.new([%{}])Record set: [field1: S1, field2: S2] — all records with fields drawn from the
respective sets.
iex> ExTLA.Function.record_set(pc: MapSet.new([:idle, :busy]), n: MapSet.new([0]))
MapSet.new([%{pc: :idle, n: 0}, %{pc: :busy, n: 0}])