Delta-debugging a failing trace down to one a human can read — Phase 4 of the DST framework (design: docs/design.md).

A run that finds a violation hands back the trace that produced it, and for a real system that is not a bug report: a three-member registry cluster produces around 1900 entries, of which almost all are heartbeats and unrelated members making progress. Shrinking searches for the shortest trace that still fails.

#{outcome := {violation, _}, trace := Trace} = eta_run:run(my_sut, #{seed => 3}),
#{trace := Minimal} = eta_shrink:shrink(my_sut, Trace, #{seed => 3}).

The oracle has three answers, not two

This is the part that decides whether a shrinker is any good.

A candidate trace is tested by replaying it, and the result is one of:

Conflating the last two is the classic way to build a shrinker that appears to work and quietly discards the minimal case: a candidate that diverges gets recorded as "still fails? no", so a removal that was in fact safe is reverted.

Here divergence is avoided rather than classified. eta_run:replay/3 runs candidates in lenient mode, where a step naming a process that is not currently runnable is skipped instead of reported. That matters because entries are not independent: removing an operation necessarily strands the steps belonging to the process it spawned, so under a strict replay nearly every candidate would diverge and the search would learn nothing.

Why the result is re-recorded

A lenient replay is not a faithful one — it silently dropped entries — so the shrunk candidate is not a trace anyone should be handed. What the run actually executed is, and eta_run records exactly that. So the last step of a shrink is to take the surviving candidate's own recorded trace and verify it strictly: a minimal trace that does not replay is not a repro.

That verification is not a formality. It is the only thing standing between this and a shrinker that reports a beautifully small trace nobody can reproduce.

What it shrinks, and what it cannot

Both dimensions at once, since both are entries in the same list: operations disappear entirely, and so do scheduling decisions. Removing an operation is the larger win and usually happens first because ddmin works coarse-to-fine; what survives at the end is close to a minimal interleaving.

A shrunk trace is not an explanation, and this doc used to claim otherwise. It said the result was "nearly a proof sketch of the defect", which is true for somebody who already knows the protocol and how ids were assigned, and false for everybody else. {step, 8} names a position, not a process, and says nothing about what that process did. Reading one means reconstructing every mailbox state by hand.

Pinning ids fixed which process an entry names, and that is not the same as saying what it did — {step, 8} is a stable name and still a number. What shrinking gives you is a trace short enough to be worth narrating. eta_log is what narrates it, and the order matters:

#{trace := Minimal} = eta_shrink:shrink(Mod, Trace, Opts),
eta_run:replay(Mod, Minimal, Opts),
eta_log:analyze().

The replay is not optional. eta_log collection restarts with every run, and a shrink has just performed several hundred of them, so the log currently holds whatever its last candidate did. Replaying the surviving trace is what puts your failure in the log and nothing else.

It cannot shrink below what the system needs to reach the violation at all, and it does not try to simplify the contents of an operation (a smaller name, fewer participants). That is a separate axis and the one now worth doing next.

Ids used to be positional, and that used to bound the whole search

An id named a process by counting — "the Nth process this run adopted" — so deleting an operation renumbered every process created after it and the surviving {step, Id} entries stopped naming what they named. The oracle then read a clean run and concluded the removal mattered, when all that had happened was arithmetic. It was the single largest thing holding results back, and it is closed: eta_run records on each entry the ids that entry created, and eta_sched:pin/2 hands them back on replay instead of recounting. An id now means "the process the trace called 7", which no deletion elsewhere can change.

Measured by deleting a trace's leading operation and counting how many of the steps behind it still ran — 76/105, 84/96 and 73/107 on three 2PC seeds before, 101/105, 94/96 and 100/107 after. End to end over 30 failing 2PC seeds: mean result 9.4 entries down to 7.6, the worst seed from 22 entries to 7, and the max_tests budget went from binding on one seed to binding on none, the hungriest search now using 336 of its 500.

Not every seed improved — one went from 7 entries to 8. ddmin's path through the partitions depends on the oracle's answers, so answering more of them correctly can still land somewhere marginally worse; nothing about that is unsound, and the result is verified either way.

What remains is the real bound, and it is smaller. Removing an operation still strands the steps belonging to the processes it created, because those processes genuinely never exist — no naming scheme fixes that, and it is the correct behaviour. So minimality is still approximate; it is now approximate for a reason that is about causality rather than about counting.

This documentation is LLM-generated. See the AI disclosure in README.md.