**A minor line, and the patch number does not start at zero.** Two of the changes below move
the public surface in ways a patch number promises not to: `TLA.Coverage`'s `observe_action/5`
is gone, replaced by `observe_enabled/3` and `observe_generated/4`; and a `schema_version: 1`
JSON document, which `mix tla.check` wrote under v0.2.0, is now refused rather than read. Three
more are additions — `TLA.Trace.explore/3`, `mix tla.explore`, and `TLA.Profile` with
`mix tla.check --profile`. `RELEASING.md`'s bar is whether someone decides the public surface
moved, and it moved on five counts.

The `20` is the commit count since the last of those five landed (#135, `bf14e81`), not since
`v0.2.0`. Everything after it — #137 through #147 — is fixes and CI work that a patch number
describes correctly, so the version says both things at once: the line opened there, and twenty
commits of patch-level work followed. `v0.3.0` is tagged at `bf14e81` to mark the opening;
`RELEASING.md` §*The base tag is a marker* says why that tag has to exist.

- **`TLA.Trace.explore/3` — evaluate your own named expressions at every state of a
  counterexample** (#115, #120). A trace is nineteen raw variable dumps and the reader does the
  arithmetic; this puts named expressions down the rows and states across the columns, so the
  question a reader actually has ("when did quorum form?") is answered by looking rather than by
  counting.

  ```elixir
  TLA.Trace.explore(trace,
    waiting: &length(&1.waiting),
    holder:  & &1.holder,
    quorum?: &(map_size(&1.votes) * 2 > 3)
  )
  ```

  Three arguments rather than two, deliberately: options live in `opts`, so an expression named
  `:changed_only` stays representable and cannot silently become a flag. Rows render in the order
  given — the caller's order is information, so it is not sorted.

  **Columns are chunked to a width budget** (`width: 68`, matching `format/1`'s banners) with the
  name column repeated in each chunk, because the trace that motivated the feature does not fit on
  one screen and `changed_only: true` cannot be relied on to narrow it — an expression that moves
  at every step is exactly the case that stays wide.

  An expression that raises is reported **at the state it raised in**, carrying
  `Exception.message/1`; the rest of the table still renders. A failure that is displayed and
  attributed beats one swallowed into a blank cell. Lassos go through `to_behavior/1`, so the
  repeating columns are marked, and a `cycle: nil` lasso is not given a fabricated cycle.

- **`mix tla.explore` — the same table from the command line, over a saved counterexample**
  (#115, #121).

  ```
  mix tla.explore Specs.DistributedLock --trace counterexample.json \
    --expr "waiting: length(state.waiting)" \
    --expr "quorum?: map_size(state.votes) * 2 > 3" \
    --changed-only
  ```

  An expression is a function and cannot be written on a command line, so `--expr` is repeatable
  and each one is compiled with the state's variables in scope — the TLA+ Toolbox's approach, and
  it needs no DSL macro. Dropping the `name:` prefix uses the expression text as the row label. An
  `--expr` that does not compile fails with the text, the reason, and **which** of several `--expr`
  flags it was, rather than a bare `CompileError` from inside the task.

  It reads what `mix tla.check --format json` writes, in either shape — the whole document or a
  single trace lifted out of it — and lassos work. The `<module>` argument is required because
  `Trace.from_json!/1` resolves atoms through `String.to_existing_atom/1`, so the spec module has
  to be loaded before a saved trace can decode.

  Note the word: this explores a **saved counterexample**, not the state space.
  `TLA.ModelChecker.explore/2` is the other thing, and the task name is the one place `explore`
  appears unqualified.

- `TLA.Profile` and `mix tla.check --profile` — what each of *your* declarations cost, per
  invariant, action guard, transition, action property and terminal (#116, #130). `TLA.Coverage`
  says how often the checker asked; this says what the answer cost, which is the half a spec
  author can act on.

  **Measured in reductions, not milliseconds.** Every performance number this project had was
  caveated by a CPU model and a load average — `bench/search_profile.baseline.md` records a
  `raft` run swinging from 23.4 s to 30.5 s on machine load alone — and a ranking that changes
  with the load average is not a finding. Under 32 competing processes the same fixed workload
  spread 100.3% in wall time and not at all in reductions.

  The cost reported is the per-evaluation **floor** times the evaluations, not the accumulated
  total: accumulating gave spreads of 26.7% and 47.8% between identical runs, while every
  declaration's floor came back a single value across eight loaded runs. Anything above the floor
  in one evaluation is the scheduler, not the predicate. A predicate whose cost genuinely varies
  with the state is the one thing a floor cannot see, so it is flagged rather than averaged away.

  Off by default, and free when off — the closures `TLA.Spec.Compiled` already holds are wrapped
  only when a profile is asked for, so no macro work and no recompilation is involved.

  Correct under `--workers` (#131): reductions are per-process, so each task collects its own
  contribution and `TLA.ModelChecker.Parallel.merge/2` sums them beside `TLA.Coverage.merge/2`.
  Per-declaration evaluation counts under `--workers 8` are identical to the single-worker
  counts, which is the property a merge can silently break while leaving the totals plausible.

- **The profile counted counterexample regeneration and liveness evaluation as if they were
  search work, so per-declaration transition counts were too high** (#133). **The numbers change**
  — a profile taken before this version is not comparable with one taken after it, and the
  direction is always downward.

  Two paths, and the larger was not the one that raised the issue. A **refuted** run replays its
  counterexample to turn a path back into states, which applied each transition once more per
  appearance in the trace: `audit_log` reported `record` 4 times against a search that applied it
  twice. A **`check_liveness: true`** run rebuilds *every* state to evaluate predicates over it,
  which inflated by roughly a whole extra search — 10 against 5 on a six-state spec — with no
  violation and no counterexample involved.

  The cause was one value doing two jobs: the instrumented spec was handed both to the search and
  to `TLA.StateGraph`, and everything that consults the graph's spec runs *after* the search has
  stopped. The graph now keeps the uninstrumented copy. Only `{:transition, _}` entries were ever
  affected — replay applies transitions and nothing else, so guards, invariants and action
  properties were always right.

  Guarded by an identity rather than by fixtures (#139): for a profiled run the sum of transition
  evaluations equals `result.transitions`, since the graph's counter is incremented on the line
  after each application. Asserted across eleven configurations, including `--workers` and
  `verify_symmetry`.

- **`coverage.bounded_by` said the counts were partial when a completed search merely found a
  deadlock** (#136). A deadlock is detected after the frontier empties, so such a run has counted
  everything — but it reached the same `:violation` as a run that stopped mid-expansion on an
  invariant, and `TLA_COVERAGE.md` marked its sections `LOWER BOUNDS` with a `≥` on every count
  that was in fact exact. The value is now derived from the search's own outcome rather than
  from the verdict it produced, so a completed search reports `:none` whatever it found.

  No new value and no schema change: the field means *are these counts complete, and if not why*,
  and `status: :violation` with `bounded_by: :none` is the correct pair — a problem was found,
  and everything was searched. Four of the ten `LOWER BOUNDS` sections in the golden lose the
  marking; the six that were genuinely truncated keep it.

- **A run that halted mid-expansion reported the offending action as never enabled** (#128). A
  counterexample would name `compact` in its trace while the coverage report in the same result
  called it never enabled and warned that its guard was broken. `TLA.Coverage.observe_action/5`
  is replaced by `observe_enabled/3` and `observe_generated/4`, because *was this action enabled
  here* and *how many states did it generate* are different facts known at different moments:
  enablement is now recorded when the guard admits a binding, which is true whether or not the
  expansion finishes.

  It was an off-by-one for as long as the checker has existed and became a false claim only when
  the true count is one — `die_hard`'s actions are enabled in eleven or twelve states, so losing
  one left eleven and looked like nothing. `TLA_COVERAGE.md` moves accordingly: one action per
  violating spec gains the occurrence it had been losing.

  `--strict-coverage` no longer fails a build on an action that was never enabled in a run
  bounded by `max_states` or a `state_constraint`: such a run cannot tell an action whose guard
  is never true from one whose states it never reached. A **complete** run still accuses.

- **`spec/04-layer2-model-checker.md` now documents `mix tla.check`'s options correctly** (#132,
  #134). The spec denied that `--workers` was a flag — it has been one since Phase 4, and the same
  file documents `workers:` nine hundred lines earlier, so it disagreed with the code and with
  itself. Four of the nine switches were missing from the option lists (`--format`, `--max-states`,
  `--safety-only`, `--workers`), and the Usage block demonstrated two that have never existed
  (`--graph`, `--output`; `mix tla.visualize` is the task that draws graphs).

  No behaviour changes here — this is documentation catching up with the task. It is recorded
  because an example that cannot be run is worse than an absent one: a reader tries it and gets
  `OptionParser` refusing a flag the specification just showed them.

- **`mix tla.check --format json` is now `schema_version: 2`**, gaining a `profile` key that is
  `null` unless the run was profiled. Purely additive, and it bumps anyway: "additive changes do
  not count" is the reasoning that makes a version stop meaning anything, and this one exists so
  a reader can refuse a shape it does not know rather than misread it. `TLA.Mix.TraceFile`
  refuses a version-1 document naming both versions, and re-running `mix tla.check --format json`
  regenerates it.

23 commits since v0.3.0, merges included.
Tagged at 0a8c91b313ad.