Shrink and replay failing cases

Counterexample Shrinking & Replay

Use this skill when a property-based or stateful model test finds a failure, or when designing generators and test runners so failures shrink cleanly and replay deterministically.

Minimal Counterexample Discipline (Zeller & Hughes)

1. Shrink Both Data and Operation Sequences:
   • A raw failing run may involve 40 operations, 12 accounts, and arbitrary 9-digit amounts. Let the shrinking engine reduce:
     • Sequence length: Prune unrelated operations that do not contribute to the invariant violation.
     • Entity count: Reduce multi-user/multi-item sets to the smallest number of actors and records needed (often 1–2 actors and 1–2 items).
     • Scalar values: Shrink amounts, timestamps, and strings toward $0$, $1$, or the exact threshold where the rule breaks.
2. Verify the Shrunk Case Preserves the Exact Failure:
   • Confirm that the minimized counterexample triggers the same invariant violation or exception—not a secondary error caused by an invalid shrunk input. If shrinking produces an illegal domain value, fix the generator's structural constraints so the shrink tree stays within the valid domain.
3. Bound Shrinking Time and Steps:
   • Cap shrinking iterations/time (interruptAfterTimeLimit, maxShrinks) so slow integration targets never hang the test runner indefinitely.

Deterministic Replay Metadata

Every reported failure and test output must capture complete replay coordinates:

• Seed & Path: Record the exact PRNG seed and shrink path (e.g., fc.assert(prop, { seed: -1294812, path: "4:1:0" }) or @reproduce_failure / @example in Hypothesis).
• Serialized Counterexample: Log the human-readable minimized inputs and ordered command trace ([Credit(100), Reserve(60, key="a"), Capture(60, key="a"), RetryCapture(60, key="a")]).
• Environment & Versions: Record the runtime version, PBT library version, timezone/clock setting, and exact test command.

Triaging the Failure: Product vs. Specification vs. Test Bug

Before filing a defect, classify the counterexample into one of three categories:

1. Product Bug: The input is valid, the invariant reflects an approved rule, and the system violated the rule.
2. Specification Gap / Ambiguity: The counterexample exposes an edge case where two business rules conflict or the specification is silent (e.g., rounding remainder on a 3-way split after a partial refund). Escalate with the concrete example to clarify the rule.
3. Test / Generator / Model Bug: The generator produced an impossible initial state, or the shadow model omitted a valid business rule. Fix the test rather than the product.

Permanent Regression Locking

• Convert every confirmed product counterexample into a permanent, deterministic regression test (either a dedicated unit/integration test or an explicit pinned example such as examples: [[minimalCase]] / @example(...)) alongside the property test so CI always runs that exact failure case first.

Checklist

• Is the counterexample shrunk to the smallest sequence of operations and simplest scalar values that still reproduce the invariant violation?
• Are the exact seed, shrink path, command trace, and CLI replay command recorded?
• Has the failure been classified as a product defect, specification ambiguity, or test/model flaw?
• Is the minimal counterexample locked in as a permanent deterministic regression case?