Read a witness as an explanation rather than a measurement
The history control presents three fixed complete histories. It does not accept arbitrary database traces. In Read after success, the write finishes at time 3 and the read starts at time 4. The checker must place the write first, then verify that the read returns 1. In Stale read after success, the intervals impose the same order but the read returns 0. The specification rejects that result. In Read overlaps write, a read returning 0 fits before the write, even though the write was invoked first. Choosing a preset replaces the whole history rather than sending messages to a simulated cluster.
The checker searches candidate orders by maintaining a current register value, initially 0. It may choose an operation next only when no remaining operation must precede it in real time. A write updates the current value. A read is eligible only when its recorded result equals that value. If a branch gets stuck, the search tries another eligible order. Reaching the end supplies the displayed witness. This is an exhaustive search for the bounded input, not a probabilistic judgment that an execution looks plausible. The underlying model limits histories to eight distinct complete operations.
A witness states that at least one permitted sequential explanation exists. Several explanations may exist when operations overlap. The first one found is not evidence that the system internally used that order. Conversely, failure to find a witness refutes linearizability for this supplied complete register history, assuming its intervals and results are accurate. It does not diagnose whether the cause was stale routing, an application bug, a bad trace, or a failed replication rule. Those explanations need observations from the implementation. The control deliberately isolates specification checking from protocol diagnosis.
For guided exploration, predict each preset's answer before selecting it, then identify the exact precedence relationship responsible. On paper, extend the overlapping preset with a second read that starts after the first read finishes but still before the write responds. Give the first read result 1 and the second result 0. Try every possible position for the write relative to those reads. The earlier read requires the write before it, while the later read requires the write after it. Their nonoverlap makes those requirements incompatible. This extension is a reasoning case, not an extra preset or an editable feature of the control.
Incomplete operations require a different treatment. If a write times out without a recorded response, it may still have taken effect. A linearizability analysis can sometimes complete such an operation with an imagined response and include it, or omit an operation that never took effect, subject to the formal history rules. Simply deleting every timed-out write can turn a legal read into an apparent unexplained value. Simply counting every invocation as a completed write can impose effects that never occurred. The displayed checker avoids this issue by handling complete operations only. Its bounded result does not certify a storage system under arbitrary failures.