[−][src]Trait stateright::Model

pub trait Model: Sized {
    type State;
    type Action;
    pub fn init_states(&self) -> Vec<Self::State>;

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

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

    pub fn display_outcome(
        &self, 
        last_state: &Self::State, 
        action: Self::Action
    ) -> Option<String>
    where
        Self::State: Debug,
    { ... }

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

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

    pub fn next_states(&self, last_state: &Self::State) -> Vec<Self::State> { ... }

    pub fn properties(&self) -> Vec<Property<Self>> { ... }

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

    pub fn within_boundary(&self, _state: &Self::State) -> bool { ... }

    pub 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 implement actor::Actor and actor::System.

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

Associated Types

type State[src]

The type of state upon which this model operates.

type Action[src]

The type of action that transitions between states.

Loading content...

Required methods

pub fn init_states(&self) -> Vec<Self::State>[src]

Returns the initial possible states.

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

Collects the subsequent possible actions based on a previous state.

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

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

Loading content...

Provided methods

pub fn display_outcome(
    &self,
    last_state: &Self::State,
    action: Self::Action
) -> Option<String> where
    Self::State: Debug, [src]

Summarizes the outcome of taking a step.

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

Returns an SVG representation of a Path for this model.

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

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

pub fn next_states(&self, last_state: &Self::State) -> Vec<Self::State>[src]

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

pub fn properties(&self) -> Vec<Property<Self>>[src]

Generates the expected properties for this model.

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

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

pub fn within_boundary(&self, _state: &Self::State) -> bool[src]

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

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

Instantiates a CheckerBuilder for this model.

Loading content...

Implementors

impl<S: System> Model for SystemModel<S>[src]

type State = SystemState<S>

type Action = SystemAction<<S::Actor as Actor>::Msg>

pub fn as_svg(&self, path: Path<Self::State, Self::Action>) -> Option<String>[src]

Draws a sequence diagram for the actor system.

Loading content...