Function explore 

pub fn explore<W, M>(
    definition: &W,
    model: &M,
    limits: ExplorationLimits,
) -> ExplorationReport
where
    W: WorkflowDefinition,
    M: WorkflowModel<W> + ?Sized,

Explores the states reachable from model’s initial states and checks the projection invariants of spec §8.4 on every one of them.

The search is breadth-first, so the path reported with a violation is the shortest sequence of commands that reaches the offending state. States are deduplicated by the canonical JSON of the state, which is why a model must derive identifiers deterministically.

Checked on every reachable state:

• check_view passes — one phase, obligation identifiers unique, a user-owned phase carries a blocking requirement, a terminal phase carries none and does carry an outcome, no outcome while obligations remain;
• two projections of the same state produce the same obligation identifiers and the same erased view (I2);
• projecting the same state at another case revision produces the same view once the case reference itself is set aside, so the map cannot depend on how often the case was written (see EXPLORATION_REVISIONS);
• the blocking requirement, when there is one, builds into a card that can actually be answered (InteractionSpec::validate), so a user-owned phase really does derive an interaction (spec §27.3);
• the state is not a dead end: it is terminal, or it offers a candidate command, or it carries a blocking interaction;
• an absent state does not project to a terminal phase or an outcome. A case’s identity outlives its content, so removal is a status and an absent state means not yet, never no longer (ExplorationViolationKind::CaseEndsByDisappearing).

Checked on every simulated transition:

• a refused command leaves the state it was given untouched;
• a command WorkflowDefinition::validate_command refuses is not applied by the model;
• an applied command does not drop the case it was given (ExplorationViolationKind::TransitionRemovesCase), which is the same rule seen from the model instead of from the projector.

Checked once at the end, and only when the search was not truncated: every outcome WorkflowModel::declared_outcomes declares was projected somewhere. A truncated search cannot prove that an outcome is out of reach, only that it did not get there within the limits, so the check is skipped rather than reported as a violation.