CompactionCoverage

constructor(runs: Int = 0, postMergeRunsWithCompaction: Int = 0, postMergeMaxDroppedInOneStep: Int = 0, preMergeRunsWithTwoOrMoreCompacting: Int = 0)

Parameters

runs

LatticeLawHarness.run calls made with a compactor bound.

postMergeRunsWithCompaction

runs in which the post-merge phase performed at least one state-changing compaction. Guards V1 — "the hook never fires".

postMergeMaxDroppedInOneStep

the largest single compaction step seen, in ids. Guards V2 — "it fires, but too small to discriminate": a Compact carrying one id has exactly one key order and a one-element dropped-dot set has exactly one element order, so no ordering defect is detectable at size 1. This is the metric that a floor phrased as "compaction happened" misses.

preMergeRunsWithTwoOrMoreCompacting

runs in which two or more replicas each compacted alone before the merge. One is not enough: the pre-merge phase exists to vary the merge of already-compacted states, and with a single compacted operand there is nothing to merge it with. This is the count that pins MovableTree.compactedDots, which the post-merge phase cannot see at all (see LatticeLawHarness.run).