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

Layer 3: a GenServer checked against the specification it claims to refine.

    defmodule Counter do
      use GenServer
      use ExTLA.GenServer, spec: Specs.Counter, refinement: __MODULE__.Refinement

      defmodule Refinement do
        use ExTLA.Refinement

        def abstract(%{value: v, status: s}), do: %{count: v, status: s}
        def abstract_action({:increment, _}), do: {:increment, %{}}
        def abstract_action(_), do: :unmapped
        def concrete_message(:increment, _), do: {:increment, 1}
      end

      # ... ordinary GenServer callbacks
    end

Every transition is mapped through the refinement, and then four things happen:

1. the **step** is checked against the spec's action — the guard must have held, and the
   spec's transition must reproduce the abstract post-state;
2. an `:unmapped` message must not have moved the abstract state;
3. the spec's invariants and action properties are checked on the abstract states; and
4. the transition is appended to the process's bounded behaviour trace.

Step 1 is the point. Without it the layer verifies that a projection of the state
satisfies some predicates, which passes every implementation bug that reaches a
legal-looking state by an illegal route (see "What conformance checks" in
`guides/reference.md`). Example 4 in `07-examples.md` is exactly that bug: an `increment`
that also does `done`'s work leaves `count` in bounds, so every invariant holds and only
the step check refuses it.

## Layer 1 comes with it

`use ExTLA.GenServer` implies `use ExTLA.Invariant`, so a module may declare `invariant`,
`action_property`, `precondition` and `postcondition` on its *concrete* state alongside
the spec's on its abstract one. The two hooks wrap the same callbacks independently and
nest: neither renames anything, both use `defoverridable` and `super`.

## `validate!/3` runs at compile time

A mapping that does not cover the spec's variables or actions fails the build rather
than producing misleading passes at runtime. What it cannot decide — the two rules that
need a concrete state — it names in the deferred list, and `ExTLA.Refinement.abstract!/3`
checks those on every mapping instead.

## `:disabled` emits nothing

As in Layer 1, and for the same reason: the mode is resolved where the instrumented
module compiles, and under `:disabled` the module compiles exactly as written — no
wrapper, no `defoverridable`, and no compile-time validation of a mapping that will
never run.

---

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