Struct ClaimModel 

#[non_exhaustive]
pub struct ClaimModel {
    pub workflow: ClaimWorkflow,
}

The exploration model of the claim workflow.

Every value comes from a fixed table and the proposals are two constants, so the reachable state space is finite and identical on every run. The model deliberately offers a refused command in each phase, since the explorer checks that a refusal changes nothing.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

workflow: ClaimWorkflow

The definition transitions are applied through.

Implementations

impl ClaimModel

pub const fn new() -> Self

Builds the model.

Trait Implementations

impl Clone for ClaimModel

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for ClaimModel

impl Debug for ClaimModel

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ClaimModel

fn default() -> Self

Returns the “default value” for a type.

impl WorkflowModel<ClaimWorkflow> for ClaimModel

fn initial_states(&self) -> Vec<Option<ClaimState>>

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.

fn candidate_commands(&self, state: Option<&ClaimState>) -> Vec<ClaimCommand>

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.

fn simulate( &self, state: Option<&ClaimState>, command: &ClaimCommand, ) -> SimulatedTransition<ClaimState, ClaimEvent>

Applies one candidate command purely.

fn declared_outcomes(&self) -> Vec<ClaimOutcome>

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.