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

Layer 2 and Layer 3, checked against each other. See "What conformance checks" in
`guides/reference.md`.

They compute over the same specification and never look at one another. Layer 2 says
which states are reachable. Layer 3 runs a real GenServer and observes behaviour through
a refinement mapping. A trace the implementation produces that is **not a path in the
checker's graph** means one of three things:

  1. the implementation is wrong — the finding Layer 3 exists for;
  2. the refinement mapping is wrong — `ExTLA.Simulation`'s own stated catch, "a
     refinement mapping that is wrong in a state no test happened to reach";
  3. **the search missed a state** — a checker defect, found by running code.

A simulation alone considers only the first two, and the third is indistinguishable from
them. It is also the one nothing else finds: a running server explores paths driven by
real OTP scheduling rather than by the checker's own traversal code, so it can reach a
state the search missed.

## What is decidable here, and what is not

Given a step the graph does not contain, replaying it against the DSL semantics settles
**one** question completely: does the spec permit it?

  * **it does**, and the graph lacks it — the search missed something. `:checker`, and
    the finding this module exists to make.
  * **it does not** — the implementation did something the spec forbids, *or* the
    mapping described the step wrongly. `:not_a_step_of_the_spec`.

That last pair is not split, and not because it is hard: one of the two is wrong, and
which one is not something the checker can decide from the step. The same holds for a
`ExTLA.Replay`'s `:not_followed`, and a confident split would be a self-consistent wrong
answer. Layer 3's own
`check_step/5` runs during the simulation and reports its reading; this adds the
containment view beside it rather than overruling it.

## It declines to answer about a truncated graph

Past `max_states`, or under a `state_constraint`, absence from the graph is a fact about
the bound rather than about the search. Reporting that as a checker finding would
manufacture exactly the false positive that gets a check like this turned off, so the
run's status is a required argument and a bounded one is refused.

# `finding`

```elixir
@type finding() ::
  :ok
  | :nothing_observed
  | {:checker, map()}
  | {:absent_state, map()}
  | {:not_a_step_of_the_spec, map()}
```

What containment found. `:ok`, or the first divergence and its class.

# `against_graph`

Is every state of `behaviour` a node of `graph`, and every step an edge?

`status` is the run's own status, and it is required rather than optional: only a
complete run can be audited this way, and a caller who has not thought about that is a
caller about to get a false finding.

    ExTLA.Conformance.against_graph(graph, behaviour, status: result.status)

# `explain`

A finding rendered for a person, saying which of the three it is and why that matters.

---

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