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

What each of *your* declarations cost, measured in reductions.

`ExTLA.Coverage` answers how often the checker asked a declaration. This answers how expensive
the answer was — the other half of the question a spec author has when a run is slow, and the
only half they can act on. "Invariant checking is 3.2%" is a fact about the checker;
"`quorum_agrees` cost 2,400 reductions each of 58,359 times" is a fact about the spec in front
of them.

## Why reductions and not milliseconds

A wall-clock number means nothing without the CPU model and the load average it was taken
under: the same model-checking run can swing by a quarter or more on machine load alone.

A reduction is the BEAM's own unit of work. The counter is incremented on function calls and
BIF work and consults neither the clock nor the CPU, so the count is a function of
`(OTP version, code, data)` and of nothing else. The same fixed workload under 32 competing
processes:

    wall       2,512 -> 5,032 µs, a 100.3% spread
    reductions 225,017 -> 225,017

## The floor is the measurement, and the total is not

Accumulating the deltas does *not* give a reproducible number. Eight runs of one spec under 32
competing processes, totals:

    invariant  19 reds/eval     3,819 -  4,839    26.7% spread
    invariant  34 reds/eval     6,834 -  7,249     6.1%
    guard       2 reds/eval       402 -    594    47.8%

The excursions are absolute — a reduction or five on some evaluations — so they are negligible
against an expensive declaration and total against a cheap one. Ranking on those totals gave
five different orders in ten runs.

The **per-evaluation minimum** has no such problem. Across the same eight loaded runs every
declaration's floor came back a single value — 3, 11, 20, 35, 80, 155, 305 — with zero
variance. That is the honest reading of what is happening: the floor is what the predicate
costs, and anything above it in a given evaluation is the scheduler getting in the way of the
measurement rather than the predicate doing more work.

So the reported cost is `floor x evaluations`. That is reproducible to within a small
**absolute** margin — two reductions per evaluation — and the margin does not grow with load.
A floor can only be pushed up, by an evaluation that never ran uninterrupted, so a short run on
a busy machine may miss the true minimum and land a reduction or two high; it cannot land low.
On a 304 reds/eval declaration that is 0.7%, and it is still two reductions at load 32, where
the same workload's wall time spread 100.3%. Evaluation counts are exact under any conditions —
they are a function of the search, not of the measurement.

**What the floor cannot see** is a predicate whose cost genuinely varies with the state — one
that short-circuits on most states and does the work on a few. Its floor is the cheap case, so
the reported cost understates it. That is why `observed` is kept beside it and why the report
flags a row whose observed total runs well above its attributed one: the gap is a finding, not
a defect, and averaging it away would hide the most interesting predicate in the spec.

## What this deliberately does not measure

**Garbage collection.** Reductions do not charge for it, so a predicate that allocates heavily
is slightly undercharged — measured at ~2% of wall on an allocation-heavy loop, against the 30%
the wall clock swings on load. The trade is worth it and is stated rather than hidden.

**The checker's own machinery.** Its phases are ETS and NIF work rather than user code, and
whether reductions describe those well is a question nobody has measured. This module wraps
the closures `ExTLA.Spec.Compiled` holds and nothing else.

## Where the window opens and closes, and why there is no `bounded_by` here

The window is the **search**, and only the search. The checker instruments a copy of the spec
for the search and stops counting when that copy stops being called; the state graph keeps the
*uninstrumented* spec, because everything that consults it runs after the search has stopped —
replay, which turns an `ExTLA.StateGraph.path_to/2` result back into states by applying
transitions. Regenerating a counterexample, or materializing every state so a liveness
predicate can be evaluated over it, is not work the spec's transitions did while exploring.
Counting it would charge a refuted run each trace step twice, and a `check_liveness: true` run
roughly a whole second search.

That boundary is what lets this module say something `ExTLA.Coverage` cannot. Coverage's
`bounded_by` exists because a halted search leaves the **state space** incompletely described:
its counts are a floor on a question about the spec. This module's counts are not a claim about
the state space at all — they are a census of **work performed**, and a search that halted
performed exactly the work it performed, its partial last expansion included. That number is
complete under every halt condition, so there is deliberately no `bounded_by` on a profile: it
would qualify a count that is not uncertain.

A reader who needs to know the run stopped early has `status` and `coverage.bounded_by` on the
same result struct, which is the honest place for it.

## Why the process dictionary

The closures are called from deep inside the checker's hot path — invariant checking, guard
evaluation, action application — and they return only their value. There is nothing to thread
an accumulator back through, short of changing the signature of every call site in the hot
path to carry one.

The dictionary is not merely the convenient answer, it is the *correct* boundary: it is
per-process, which is exactly what a worker's contribution is under `workers:` (each worker's
`ExTLA.Coverage` starts from zero for the same reason). A worker reads its own dictionary at
the end of its slice and hands back a struct, so `merge/2` composes the way
`ExTLA.Coverage.merge/2` does and no shared mutable state touches the expansion path.

Writes are confined to `bump/2` and reads to `collect/1`. Nothing else in the project reads
these keys.

# `entry`

```elixir
@type entry() :: %{
  evaluations: non_neg_integer(),
  reductions: non_neg_integer(),
  per_eval: non_neg_integer(),
  observed: non_neg_integer(),
  settled: boolean()
}
```

# `key`

```elixir
@type key() :: {kind(), atom()}
```

# `kind`

```elixir
@type kind() :: :invariant | :terminal | :action_property | :guard | :transition
```

# `t`

```elixir
@type t() :: %ExTLA.Profile{
  calibration: %{
    required(2) => non_neg_integer(),
    required(3) => non_neg_integer()
  },
  declarations: %{required(key()) => entry()},
  otp_version: String.t() | nil,
  run_reductions: non_neg_integer()
}
```

# `clear`

Remove this process's counters from its dictionary. `zero/1` does this on a worker's way
in; the coordinator calls it on its way out, so the keys do not outlive the run in
a long-lived process.

# `collect`

This process's contribution, read out of its dictionary.

Raw: the calibration is subtracted by `finalize/2`, after any merging, so the constant is
applied exactly once however many workers contributed.

# `finalize`

Subtract the instrumentation, turn the per-evaluation floor into a cost, and record what the
whole run spent.

`run_reductions` is the CALLER's bracket — the coordinator's — and is ADDED to whatever the
merged contributions already carry, which is every worker's own bracket. Overwriting it would
make the denominator the coordinator alone: on a single worker that is the whole run, but on
eight it is only the scheduling and the seed, and the same spec's shares would change with the
worker count.

**Called once, after any merging.** It is not idempotent — a second call would subtract the
calibration a second time — and that is why `collect/1` and `merge/2` leave the raw floor
alone. A worker collects, the coordinator merges, and this runs at the end.

Clamped at zero: a declaration cheaper than the two counter reads can measure below the
calibration floor by a reduction or two, and a negative cost is not a thing to report. It also
reads correctly — "too cheap to measure" is the honest answer for `invariant :always do true end`.

# `format`

Render for terminal output, in the shape `ExTLA.Coverage.format/2` uses.

# `init`

A zeroed accumulator for `spec`, with the instrumentation constant calibrated for this machine
and OTP release.

# `instrument`

`spec` with every declaration's closure wrapped in a counter.

Returns the spec unchanged in shape — same keys, same arities, same return values — so nothing
downstream can tell the difference except by counting. Also clears this process's accumulator,
which matters in a test suite where several runs share one process.

# `merge`

Sum two contributions. Both come from one `init/1`, so their key sets are identical and a key in
one and not the other would be a bug rather than a case to handle, as in
`ExTLA.Coverage.merge/2`.

# `reductions`

Every reduction this process has spent. The run brackets itself with two of these.

# `zero`

The same accumulator with every count back at zero, and this process's dictionary cleared.

What `ExTLA.ModelChecker.Parallel` hands a worker, for the reason it hands one a zeroed
`ExTLA.Coverage`: a worker given the coordinator's totals would return them plus its own, and
merging that counts the seed twice. Keeps the calibration and the OTP release, which are facts
about the machine rather than about the work, so a worker does not pay to recalibrate.

---

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