How does a behaviour model act as the oracle, and what does a passing generated run actually prove?

## What the word oracle means here An oracle is the thing that decides whether observed behaviour is wrong. Every test has one, explicit or not: a hard-coded expected value, a stored approved output, a crash signal, a human looking at the screen. The distinguishing feature of model-based testing is that the oracle and the case source are the *same artefact*. The model both chooses what to do and says what should happen, which is why one model edit can change hundreds of predictions at once. ## The lockstep loop A run proceeds in steps, and each step has four moves. 1. **Select**: the harness asks the model for the next action on the path, together with the state the model says the system should reach. 2. **Act**: the adapter performs that action against the real system. 3. **Observe and project**: the adapter reads what it can from the system and projects it onto the model's vocabulary. This is the subtle move. The model's states are abstractions — a billing run in `Disputed` — while the system holds rows, flags and timestamps. The projection is a function from real observable state onto a model state name, and it must be written by hand. 4. **Compare**: predicted state against projected state. Equal, continue; different, stop and report a **conformance failure** with the path prefix that produced it. The oracle is usually **partial** in two directions. It checks only the concepts the model names, and it checks them only at the granularity the projection can see. A well-built projection also asserts a few invariants that hold in a given state — in `Settled`, the outstanding balance is zero — which strengthens the oracle without enlarging the state space. ## Triaging a mismatch The reflex is to log a defect against the system. In practice a mismatch has three possible causes and the split is not one-sided. - **The system is wrong.** The genuine find: an action led somewhere the specification does not allow, or was accepted when the model forbids it. - **The model is wrong.** The model is code, written from the same documents and often by the same people, and it carries its own faults: a guard misread, a transition drawn from the wrong source state, an action added to the product and never modelled. - **The projection is wrong.** The action succeeded and the state is correct, but the adapter read the system too early, or mapped two distinct real states onto one model name. An early model-based effort tends to run at roughly one genuine system fault for every two or three model and adapter faults, and that ratio is the honest thing to say in an interview. It improves as the model stabilises. Mature teams keep the triage explicit, tagging each failure by culprit, because the trend across those tags is what tells them whether the technique is paying. ## What a green run does and does not prove It proves that over the generated paths, at the granularity the projection can see, the system agreed with the model. Four gaps follow directly. **Unmodelled behaviour is invisible.** A 4-person team maintaining a utility billing run had a green model-based suite for six weeks. The model described nine states and every legal transition faithfully, and conformance was perfect. Then the month-end run for a bulk of 12,400 accounts died part-way through: each cancel-then-reissue cycle left an open handle to the invoice-document store, and after roughly 3,900 cycles the run hit a resource exhaustion and stopped. The suite had exercised that exact transition pair hundreds of times and reported green every time, because the model described *which state comes next* and said nothing about resources released on the way. The oracle can only be as broad as the model's vocabulary. **Data inside a transition is invisible** unless projected. The model says the run reaches `Invoiced`; whether the invoice total is correct to the penny is a separate check the projection must be told to make. **Shared misunderstanding passes silently.** If the same engineer derives model and implementation from the same misreading of a tariff rule, the two agree and the suite is green. This is the deepest limitation and the reason mature teams treat the model as a reviewable artefact in its own right — walked through with the analyst or the domain owner, ideally derived by someone other than the implementer. **Only the generated paths were checked.** Paths outside the criterion's set say nothing at all. ## What to say in an interview Describe the lockstep loop, name the projection as the piece people forget, give the three-way triage, and be explicit that conformance is agreement with a fallible artefact rather than correctness. Then name what your model does not describe — that list is the honest statement of the suite's blind spot, and having one ready is the difference between a candidate who has run this and one who has read about it.