Learn · All the Ways It Can Break

growing

The Checker Owns the Choices

Your model admits branches; the search strategy explores them and returns a path rather than a hunch.

formal-methods, stateright, breadth-first-search, counterexample, model-checking, learn

You will run breadth-first checking, distinguish a property discovery from a successful verification run, reconstruct a trace as state-action-state steps, and state the finite boundary required for termination.

Run both controls

The complete specimen ends with this executable test:

let buggy = Turnstile { require_payment: false }
    .checker()
    .spawn_bfs()
    .join();
buggy.assert_any_discovery("entry requires payment");

let fixed = Turnstile { require_payment: true }
    .checker()
    .spawn_bfs()
    .join();
fixed.assert_properties();

Run it with cargo test. The first assertion requires the negative control to fail its property. The second requires the repair to have no failing discovery over the explored graph.

Breadth-first search explores every path of length d before length d + 1. It therefore finds a shortest action path in an unweighted state graph. See the checker builder API.

Read paths, not snapshots

A violation state says what is false. Its path says how it became false. Read the initial state, then for each action write only the changed fields and the guard that admitted the action. For the bug:

State 0: paid = false, entries = 0, unpaid_entry = false
Action:  Enter
State 1: paid = false, entries = 1, unpaid_entry = true
Property: !unpaid_entry is false

The diagnosis is not “the assertion failed.” It is “=Enter= was enabled in the initial unpaid state.” That sentence points to the repaired action guard.

Search — identify the responsibility boundary.

Finite work needs a boundary

The turnstile reaches at most one entry, so its graph is finite. Real models often contain counters, queues, or retries that grow forever. Constrain them by a semantic boundary, such as maximum queue length or number of requests, and put that boundary in the result sentence. A depth cutoff alone can be useful for bug finding, but it proves only the absence of a witness in explored prefixes.

Parallel checker threads change throughput, not the model's meaning. They can also change which of several same-depth witnesses is reported. Preserve a concrete trace or a property-level oracle instead of depending on incidental discovery order.

Lessons

The model admits branches; BFS or DFS chooses their exploration order.
An Always discovery is a finite counterexample.
A paired negative control establishes that the evidence can see the known bug.
Diagnose the enabling guard from the full state-action path.
Search bounds and semantic capacity bounds belong in the verdict.

Practice

Retrieval. Why does breadth-first search help counterexample diagnosis?
Discrimination. Can switching to DFS reveal an action that actions never emits?
Transfer. Break the door model's lock guard, require a discovery, repair it, and explain the shortest path.

Worked answers

It reports a shortest path by action count, reducing irrelevant prehistory.
No. Search order cannot add transitions to the graph.
Open, Lock is enough when locking while open is admitted; guard Lock by the closed position and rerun both controls.

References

Stateright. Checking tutorial. — checker construction and discoveries
Stateright. Checker API for 0.31.0. — paths and property assertions

← Rust Can Be the Model Put the Network in the Model →

The model owns possibility; the checker owns order. actions must enumerate every choice under study. spawn_bfs then performs breadth-first exploration, which is useful when the shortest counterexample is the easiest diagnosis. spawn_dfs can reach deep behavior sooner with a different memory profile, but search order cannot recover a branch the model omitted. For an Always property, a discovery is a counterexample. The turnstile test expects such a discovery from the broken model and none from the repair. This paired polarity is stronger than running only the fixed model: it proves that the property and search can detect the known defect.