ExTLA.GenServer (ExTLA v0.6.0)

Copy Markdown View Source

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.