Trait stateright::Model

pub trait Model: Sized {
    type State;
    type Action;

    // Required methods
    fn init_states(&self) -> Vec<Self::State>;
    fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>);
    fn next_state(
        &self,
        last_state: &Self::State,
        action: Self::Action
    ) -> Option<Self::State>;

    // Provided methods
    fn format_action(&self, action: &Self::Action) -> String
       where Self::Action: Debug { ... }
    fn format_step(
        &self,
        last_state: &Self::State,
        action: Self::Action
    ) -> Option<String>
       where Self::State: Debug { ... }
    fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String> { ... }
    fn next_steps(
        &self,
        last_state: &Self::State
    ) -> Vec<(Self::Action, Self::State)> { ... }
    fn next_states(&self, last_state: &Self::State) -> Vec<Self::State> { ... }
    fn properties(&self) -> Vec<Property<Self>> { ... }
    fn property(&self, name: &'static str) -> Property<Self> { ... }
    fn within_boundary(&self, _state: &Self::State) -> bool { ... }
    fn checker(self) -> CheckerBuilder<Self>
       where Self: Send + Sync + 'static,
             Self::State: Hash + Send + Sync { ... }
}

This is the primary abstraction for Stateright. Implementations model a nondeterministic system’s evolution. If you are using Stateright’s actor framework, then you do not need to implement this interface and can instead leverage actor::Actor and actor::ActorModel.

You can instantiate a model CheckerBuilder by calling Model::checker.

Required Associated Types

type State

The type of state upon which this model operates.

type Action

The type of action that transitions between states.

Required Methods

fn init_states(&self) -> Vec<Self::State>

Returns the initial possible states.

fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>)

Collects the subsequent possible actions based on a previous state.

fn next_state( &self, last_state: &Self::State, action: Self::Action ) -> Option<Self::State>

Converts a previous state and action to a resulting state. None indicates that the action does not change the state.

Provided Methods

fn format_action(&self, action: &Self::Action) -> Stringwhere Self::Action: Debug,

Converts an action of this model to a more intuitive representation (e.g. for Explorer).

fn format_step( &self, last_state: &Self::State, action: Self::Action ) -> Option<String>where Self::State: Debug,

Converts a step of this model to a more intuitive representation (e.g. for Explorer).

fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String>

Returns an SVG representation of a Path for this model.

fn next_steps( &self, last_state: &Self::State ) -> Vec<(Self::Action, Self::State)>

Indicates the steps (action-state pairs) that follow a particular state.

fn next_states(&self, last_state: &Self::State) -> Vec<Self::State>

Indicates the states that follow a particular state. Slightly more efficient than calling Model::next_steps and projecting out the states.

fn properties(&self) -> Vec<Property<Self>>

Generates the expected properties for this model.

fn property(&self, name: &'static str) -> Property<Self>

Looks up a property by name. Panics if the property does not exist.

fn within_boundary(&self, _state: &Self::State) -> bool

Indicates whether a state is within the state space that should be model checked.

fn checker(self) -> CheckerBuilder<Self>where Self: Send + Sync + 'static, Self::State: Hash + Send + Sync,

Instantiates a CheckerBuilder for this model.

Implementors

impl<A, C, H> Model for ActorModel<A, C, H>where A: Actor, H: Clone + Debug + Hash,

type State = ActorModelState<A, H>

type Action = ActorModelAction<<A as Actor>::Msg, <A as Actor>::Timer>