A state is an immutable snapshot of all specification variables. A step is a pair of consecutive states (pre-state and post-state). A behavior is a (possibly infinite) sequence of states.
A state is a plain map, deliberately: it is the value the DSL's transitions
build and the value ExTLA.Fingerprint hashes, and wrapping it in a struct would
buy nothing but an extra field in every fingerprint.
Missing variables raise
get/2, unchanged?/2 and prime/3 all fail loudly on a variable the state
does not have. This is not defensiveness; it is the difference between a bug
and a wrong answer. A misspelled variable read through Map.get/2 returns
nil, nil compares unequal to whatever the guard expected, the action looks
disabled, and the checker explores a smaller state space and reports success.
Nothing in the output distinguishes that run from a sound one — the same
failure mode, a success reported over states never visited, that
ExTLA.Fingerprint prevents at the level below.
Summary
Functions
Return the set of variables that changed between states.
Return the value of a variable in the given state.
Create a new state from a keyword list or map of variable assignments.
Return a new state with the given variable updated.
Analogous to TLA+ primed variable assignment: x' = value.
Return a new state with multiple variables updated.
Check if two states are identical (stuttering step).
Assert that specified variables did NOT change between states.
Analogous to TLA+ UNCHANGED <<x, y, z>>.
Assert that every value in the state is deterministically serializable,
per 02-dsl-semantics.md §6.
Types
Functions
Return the set of variables that changed between states.
iex> ExTLA.State.changed_vars({%{x: 0, y: 1}, %{x: 2, y: 1}})
MapSet.new([:x])Return the value of a variable in the given state.
Raises KeyError if the variable is not in the state — see the note on
missing variables in the module documentation.
iex> ExTLA.State.get(%{x: 0}, :x)
0Create a new state from a keyword list or map of variable assignments.
iex> ExTLA.State.new(x: 0, y: 1)
%{x: 0, y: 1}Return a new state with the given variable updated.
Analogous to TLA+ primed variable assignment: x' = value.
Raises KeyError if the variable is not already in the state. A TLA+ spec's
variable set is fixed by its Init, so priming a variable that is not in the
state is a typo, and a typo that silently widens the state is one the
fingerprint would then faithfully preserve.
iex> ExTLA.State.prime(%{x: 0, y: 1}, :x, 2)
%{x: 2, y: 1}Return a new state with multiple variables updated.
iex> ExTLA.State.prime_many(%{x: 0, y: 1}, %{x: 2, y: 3})
%{x: 2, y: 3}Check if two states are identical (stuttering step).
iex> ExTLA.State.stuttering?({%{x: 0}, %{x: 0}})
trueAssert that specified variables did NOT change between states.
Analogous to TLA+ UNCHANGED <<x, y, z>>.
iex> ExTLA.State.unchanged?({%{x: 0, y: 1}, %{x: 2, y: 1}}, [:y])
trueAssert that every value in the state is deterministically serializable,
per 02-dsl-semantics.md §6.
Returns the state, so it can be threaded into a pipeline. Raises
ExTLA.State.InvalidTermError naming the variable and the position inside it.
Pids, references and ports have no stable identity across runs, and funs
serialize their defining module's version. Floats are excluded for a subtler
reason: 0.0 and -0.0 compare equal under == but encode differently, so
two states that a spec author would call equal would be explored twice — and
:nan never equals itself, so a state containing one is not even equal to
itself.
iex> ExTLA.State.validate!(%{x: 0, q: [:a, {1, "b"}]})
%{x: 0, q: [:a, {1, "b"}]}