Expand description
Reducing a failing scenario to a smaller one that still fails.
This is the thing a deterministic simulator can do that a black-box fault injector cannot. A run here is a function of its inputs, so a candidate reduction can be run and the question “does it still fail?” answered rather than estimated.
§A reduced scenario is a different run, not the same one made smaller
Worth stating first, because it is what a reader is most likely to assume wrongly. Removing a step changes when every later message is drawn from the run’s generator, so the result does not replay a prefix of the original: it is a new run that also satisfies the predicate. The seed is held fixed so the reduction is reproducible, not because the stream is preserved — it is not.
Two things follow. Every candidate must be re-run rather than reasoned about, which is what this module does. And a reduction can legitimately land on a scenario that fails for a different reason than the original. The defence is the predicate: name the property, not the symptom, and the report says which predicate was used.
§What it reduces, and in what order
Cheapest and most informative first, then round again to a fixed point:
- The horizon, by binary search down to the earliest that still fails — the reduction that answers when, which is where a hand-written probe starts.
- Steps, by delta-debugging rather than one-at-a-time deletion. Faults here interact: a crash matters only with the partition that isolates its quorum, and removing either alone often stops the failure where removing both would not have been tried.
- Fault detail — a partition with fewer groups.
- Membership, last, because dropping a process changes quorum arithmetic. A bug that does not survive it is not a bug about that process; one that does is a much better counterexample.
Structs§
- Reduction
- What a reduction found, and what it cost.
- Size
- How large a scenario is, in the terms the search reduces.
Functions§
- shrink
- Search for a smaller scenario whose run still satisfies
predicate.