Trait stateright::StateMachine[−][src]

pub trait StateMachine: Sized {
    type State;
    fn init(&self, results: &mut StepVec<Self::State>);
    fn next(&self, state: &Self::State, results: &mut StepVec<Self::State>);

    fn checker<I>(
        &self, 
        keep_paths: KeepPaths, 
        invariant: I
    ) -> Checker<Self, I>
    where
        Self::State: Hash,
        I: Fn(&Self, &Self::State) -> bool,
    { ... }
}

Defines how a state begins and evolves, possibly nondeterministically.

Associated Types

`type State`

The type of state upon which this machine operates.

Required Methods

`fn init(&self, results: &mut StepVec<Self::State>)`

Collects the initial possible action-state pairs.

`fn next(&self, state: &Self::State, results: &mut StepVec<Self::State>)`

Collects the subsequent possible action-state pairs based on a previous state.

Provided Methods

`fn checker<I>(&self, keep_paths: KeepPaths, invariant: I) -> Checker<Self, I> where Self::State: Hash, I: Fn(&Self, &Self::State) -> bool,`

Initializes a fresh checker for a state machine.

Implementors

impl<A: Actor<ModelId>> StateMachine for ActorSystem<A> where A::Msg: Clone + Ord, A::State: Clone, type State = ActorSystemSnapshot<A::Msg, A::State>;
[src]