The engine behind Layer 1's callback wrappers. Not called directly.
Everything here is reached from code ExTLA.Invariant's @before_compile emitted into
the instrumented module, and the division of labour between the two is deliberate:
anything decidable at compile time is decided there. The callbacks: option is
resolved when the wrapper is generated, so a hot callback checking two of a module's
nine invariants calls this with two names rather than nine and a filter.
Telemetry
[:extla, :invariant, :violated] and its three siblings fire whenever one does, if
:telemetry is available — it is an optional dependency, and whether it was there is
decided when ExTLA compiles rather than on every check.
Success events are opt-in (config :extla, telemetry: :verbose) and unemitted
otherwise, because :telemetry.execute/3 costs about a microsecond even with no
handlers attached and a single transition can fire four of them. Violations are rare and
worth their cost; successes are the hot path.
"Unemitted" is why each check has two arities. The wrapper calls the three-argument form
unless the module compiled under :verbose, and that form contains no timing and no
success event to skip — not a branch that declines to fire one.
Summary
Functions
Check the named action properties over a transition.
The same, under :verbose.
Check the invariants of a state an Agent was read at, and return it.
Check a transition that no wrapper produced: an Agent update.
Check the named invariants against the state an init/1 produced, if it produced one.
The same, under :verbose.
Check the named invariants against a state.
The same, timing each check and emitting a :checked event. Called only from a module
compiled under config :extla, telemetry: :verbose.
Check every postcondition whose pattern matches message.
The same, under :verbose. A :no_match fires nothing, for the reason on
check_preconditions!/5.
Check every precondition whose pattern matches message.
The same, timing each check that RAN and emitting a :checked event. Called only from a
module compiled under config :extla, telemetry: :verbose.
The post-state carried by a callback's return value.
The post-state carried by a :gen_statem callback's return value.
The first state an init/1 produced, or :none.
The same for a :gen_statem, whose init/1 returns {:ok, state_name, data}.
Functions
Check the named action properties over a transition.
The same, under :verbose.
Check the invariants of a state an Agent was read at, and return it.
A read is a stuttering step: nothing moved, so there is no action property to check, but the invariants must still hold — the same reason a GenServer callback that returns its state unchanged is still checked.
Check a transition that no wrapper produced: an Agent update.
An Agent's transitions are functions its callers pass in, so there is no callback to
wrap and no compile-time place to resolve callbacks: — which is why this takes every
declared name and why callbacks: is documented as meaningless for an Agent
(§03 §Supported OTP Behaviors). Returns the new state, so it can stand in the middle of
the Agent.update/3 function it is called from.
Check the named invariants against the state an init/1 produced, if it produced one.
The tag test lives here rather than in the emitted wrapper for a reason worth recording:
inside a particular module, super(arg) has a known return type, so a case on
initial_state/1's tag has a clause the compiler can prove unreachable — and Elixir's
type system says so, as a warning, in the user's module, about code the user did not
write. Behind a function taking term() there is nothing to prove.
The same, under :verbose.
Check the named invariants against a state.
The names come from the wrapper, already filtered by callbacks:.
The same, timing each check and emitting a :checked event. Called only from a module
compiled under config :extla, telemetry: :verbose.
Check every postcondition whose pattern matches message.
The same, under :verbose. A :no_match fires nothing, for the reason on
check_preconditions!/5.
Check every precondition whose pattern matches message.
A message no pattern matches has no preconditions and passes — :no_match is the
generated clause's way of saying "this declaration is not about this message", which is
a different thing from a predicate that returned false.
The same, timing each check that RAN and emitting a :checked event. Called only from a
module compiled under config :extla, telemetry: :verbose.
A :no_match fires nothing. The generated clause answers :no_match without evaluating
the predicate — the declaration is not about this message — so an event saying a check
happened would be a measurement of a check that did not occur, and its duration would
be the cost of a pattern match reported as the cost of a precondition.
The post-state carried by a callback's return value.
pre_state is the fallback because not every return carries one: {:stop, reason, reply, state} does, a bare {:stop, reason} from handle_info does not, and :ignore
from init/1 does not. Treating those as stuttering is right — nothing moved — and it
keeps the wrapper from having to know which callback it is wrapping.
The post-state carried by a :gen_statem callback's return value.
A state machine's state is the {state_name, data} pair, so pre is both the fallback
and the source of the name a :keep_state return leaves alone. This cannot be more
clauses on extract_state/2: {:stop, reason, new_data} is a :gen_statem return
carrying DATA, and the identically shaped {:stop, reason, state} is a GenServer return
carrying the whole state. One function cannot answer both.
:gen_statem's :state_functions callback mode is not instrumented — its transitions
live in functions named after the states, which @on_definition cannot recognise. §03
specifies handle_event/4, which is the :handle_event_function mode.
The first state an init/1 produced, or :none.
:ignore and a bare {:stop, reason} are refusals to start: there is no first state,
and an invariant checked against its absence would report a violation of a predicate
that was never given anything to be about. The init/1 wrapper checks nothing in that
case — which is why this returns a tag rather than a state and a fallback.
The same for a :gen_statem, whose init/1 returns {:ok, state_name, data}.
A module is read as a state machine when it defines handle_event/4. Without this the
shared initial_state/1 would take {:ok, :red, data} for {:ok, state, extra} and
check the invariants against the state NAME — which is not the state, and which a
declaration written as {name, data} = state would refuse with a MatchError naming
neither the invariant nor the reason.