Module explore 

Bounded workflow exploration (spec §8.5).

Fixtures prove that the states you thought of behave. Exploration proves something else: that every state reachable from them still satisfies the Flow Map invariants. You give the explorer a WorkflowModel — the initial states, the commands worth trying and a pure simulation of each — and it walks the reachable states breadth-first, projecting each one and checking the §8.4 rules on it.

Because the search is breadth-first and states are deduplicated by their canonical JSON, a violation is reported with the shortest command path that reaches it, which is usually the smallest reproduction you can get.

One of the rules is a position rather than a mechanical check: a case’s identity outlives its content, so an absent state means not yet and never no longer. A projector that gives an absent state a terminal phase or an outcome, or a model that answers a command by dropping the case, is describing a case that ends by disappearing, and the explorer reports both. See ExplorationViolationKind::CaseEndsByDisappearing.

use turnframe_test::explore::{ExplorationLimits, explore};
use turnframe_test::workflows::trip::{TripModel, TripWorkflow};

let report = explore(
    &TripWorkflow::default(),
    &TripModel::default(),
    ExplorationLimits::smoke(),
);
assert!(report.is_clean(), "{}", report.describe());
assert!(report.states_explored > 1);

Structs

ExplorationLimits

Bounds on a breadth-first exploration (spec §8.5).

ExplorationReport

Everything one bounded exploration observed.

ExplorationViolation

A violation together with where it was found.

Enums

ExplorationViolationKind

One rule an explored state or transition broke.

SimulatedTransition

The result of applying one candidate command to one state (spec §8.5).

Constants

EXPLORATION_CASE_ID

Case identifier every explored projection is made against. Exploration never touches a store, so the identifier only has to be stable.

EXPLORATION_REVISIONS

The case revisions exploration projects at, cycled by visit order.

Traits

WorkflowModel

The transition model of a workflow, used for bounded exploration (spec §8.5).

Functions

explore

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

reachable_states

Walks the model and returns every reachable state, in visit order.