Trait WorkflowModel

Source

pub trait WorkflowModel<W: WorkflowDefinition> {
    // Required methods
    fn initial_states(&self) -> Vec<Option<W::State>>;
    fn candidate_commands(&self, state: Option<&W::State>) -> Vec<W::Command>;
    fn simulate(
        &self,
        state: Option<&W::State>,
        command: &W::Command,
    ) -> SimulatedTransition<W::State, W::Event>;

    // Provided method
    fn declared_outcomes(&self) -> Vec<W::Outcome> { ... }
}

Expand description

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

A WorkflowDefinition says how state projects; a WorkflowModel says how state moves. Keeping them apart means the explorer never has to run an executor, a store or a clock.

Implementations must be deterministic and side-effect free: the explorer deduplicates states by their canonical JSON, so a model that mints a fresh identifier on every call turns a small workflow into an infinite one. Derive identifiers from the state instead (for example, the n-th line always gets the n-th identifier of a fixed table).

Required Methods§

Source

fn initial_states(&self) -> Vec<Option<W::State>>

The states exploration starts from. None means “the case does not exist yet”, which is where most workflows begin — and it never means “the case is over”, because a case’s identity outlives its content.

Source

fn candidate_commands(&self, state: Option<&W::State>) -> Vec<W::Command>

Commands worth trying in this state, in a stable order. Include commands you expect to be refused: the explorer checks that a refusal changes nothing.

Source

fn simulate( &self, state: Option<&W::State>, command: &W::Command, ) -> SimulatedTransition<W::State, W::Event>

Applies one candidate command purely.

Provided Methods§

Source

fn declared_outcomes(&self) -> Vec<W::Outcome>

Outcomes the workflow claims it can reach. The explorer reports every declared outcome no reachable state projects. The default is empty, which disables the check.