The refinement mapping applied, against the memoized compiled spec.

ExTLA.Refinement.abstract!/3 takes the compiled struct rather than the module, because it checks the mapping's result against the spec's declared variables. The wrapper has only the module — so it comes through here, where the compiled spec is already resolved for the process rather than rebuilt per callback.

The same, returning the finding instead of raising it.

Check the spec's action properties against an abstract transition.

The same, returning the finding instead of raising it.

Check the spec's invariants against an abstract state.

The refinement check, returning the finding instead of raising it.

THE refinement check. Applies the named spec action to pre and compares the result with what the implementation produced.

params may be PARTIAL. An implementation frequently resolves the spec's nondeterminism itself — it pops its own queue, picks its own message — so the binding is not in the message and abstract_action/1 cannot supply it. Every binding of the action's params that extends the given ones is a candidate, and the step is legal if any enabled candidate reproduces post. That is still refinement: the spec permits the step via that binding.

Fails :not_enabled when no candidate binding has a true guard, and :diverged when one does and none reproduces the post-state — with a variable-by-variable diff against the closest candidate.

The same, returning the finding instead of raising it.

Assert that an :unmapped message left the abstract state unchanged.

:unmapped is a positive claim rather than an absence of one: a message with no spec counterpart must not move the abstract state, and a mapping that is merely incomplete is caught here rather than passing silently.

Check the spec's temporal properties against an accumulated trace. Called at the end of a simulation run, not per transition.

A finite trace can refute always(P) and can satisfy eventually(P), and can do neither the other way round, so the verdicts are :holds | :violated | :inconclusive. A real trace has no lasso — nothing says the process would have repeated that cycle forever — so the properties that need one are :inconclusive by construction rather than by accident.

The same, returning the finding instead of raising it.

Every check in this module has this pair, and the reason is ExTLA.Replay: a replay reports which step failed and carries on being a value, which is not something that can be built out of an exception without catching one. So the checks return findings and the ! forms raise them — the wrapper needs the raise, the report needs the value, and neither is derived from the other by rescuing.

One transition, checked: the step against the action the mapping names, or the stuttering claim :unmapped makes.

The dispatch is here rather than in the emitted wrapper for the same reason the init/1 tag test is. In a module whose messages the compiler can enumerate — a server with one callback clause — refinement.abstract_action(msg) has a known return, and one arm of the case is then provably unreachable. That is a warning in the user's module about code the user did not write. Behind a module() argument there is nothing to infer.

Retrieve another process's accumulated behaviour trace.

Asks the process itself, through :sys, rather than reaching into its dictionary — for the same reason record_transition!/4 takes no pid. The function runs inside the target and returns its state unchanged; only the trace travels back.

The first abstract state: mapped, checked against the spec's invariants, and recorded.

Takes the raw init/1 return rather than a state, for the reason ExTLA.Invariant.Runtime.check_initial_invariants!/4 does: :ignore and a bare {:stop, reason} produce no state, and a case on that tag in the emitted wrapper has a clause the compiler can prove unreachable — a warning in the user's module about code the user did not write.

There is no step to check. A first state is not a transition, and the trace has to start at it: a temporal property over a behaviour that begins at the second state is a property of a different behaviour.

It SEEDS the trace rather than recording a transition into it. Recording the initial state as a transition would put it in the buffer twice, and every recorded behaviour would open with a step from a state to itself. That step never happened, and ExTLA.Conformance.against_graph/3 would classify it as forbidden unless the spec happens to carry a self-loop at its initial state.

Record a transition in the CALLING process's behaviour trace.

There is no pid argument. A process dictionary is writable only by its own process, and the wrapper runs inside the GenServer, so recording is always a self-write.

The buffer is bounded (config :extla, trace_buffer: n, default 1000) and drops oldest-first: an unbounded per-process trace is a memory leak in any long-lived GenServer, which is most of them.

The behaviour recorded by THIS process: %{states: [...], dropped: n}, oldest state first.

dropped is part of the value because the states alone cannot carry it. A truncated list looks exactly like a short one. Once the buffer has dropped the behaviour's first state, the head of states is an arbitrary mid-behaviour state, and a bare predicate settled against it could report violated for a behaviour that did start where the property says. check_temporal_properties/2 reads dropped and answers :inconclusive for such a predicate instead.