# `ExTLA.GenServer.Runtime`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/gen_server/runtime.ex#L1)

The engine behind Layer 3's callback wrappers. Not called directly.

`check_step!/5` is the refinement check, and it is what makes the layer a conformance
check rather than an invariant check on a projection: an implementation can reach a
state every invariant admits by a route the specification forbids, and only comparing
the *step* against the spec's action catches that (see "What conformance checks" in
`guides/reference.md`).

## The compiled spec and the constants are memoized per process

Both are needed on every transition. `__tla_spec__/0` builds its struct on each call and
the constants come from application config, so each would be re-derived per callback.
They are resolved once per process and kept in the process dictionary beside the trace —
which is where a GenServer's per-process state belongs, and the wrapper always runs
inside the server.

# `finding`

```elixir
@type finding() :: :ok | {:violation, ExTLA.GenServer.Violation.t()}
```

What a check found: nothing, or the violation it would have raised.

# `abstract!`

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.

# `check_action_properties`

The same, returning the finding instead of raising it.

# `check_action_properties!`

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

# `check_spec_invariants`

The same, returning the finding instead of raising it.

# `check_spec_invariants!`

Check the spec's invariants against an abstract state.

# `check_step`

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

# `check_step!`

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.

# `check_stuttering`

The same, returning the finding instead of raising it.

# `check_stuttering!`

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_temporal_properties`

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.

# `check_transition`

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.

# `check_transition!`

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.

# `get_trace`

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.

# `record_initial!`

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_transition!`

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.

# `trace`

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*