[−][src]Trait stateright::Model

pub trait Model: Sized {
    type State;
    type Action;
    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>;

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

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

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

    fn follow_fingerprints(
        &self, 
        init_states: Vec<Self::State>, 
        fingerprints: Vec<Fingerprint>
    ) -> Option<Self::State>
    where
        Self::State: Hash,
    { ... }

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

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

    fn checker(self) -> Checker<Self> { ... }

    fn checker_with_threads(self, thread_count: usize) -> Checker<Self> { ... }
}

Models a possibly nondeterministic system's evolution. See Checker.

Associated Types

type State

The type of state upon which this model operates.

type Action

The type of action that transitions between states.

Loading content...

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.

Loading content...

Provided methods

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

Summarizes the outcome of taking a step.

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

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 next_steps and projecting out the states.

fn follow_fingerprints(
    &self,
    init_states: Vec<Self::State>,
    fingerprints: Vec<Fingerprint>
) -> Option<Self::State> where
    Self::State: Hash, 

Determines the final state associated with a particular fingerprint path.

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

Generates the expected properties for this model.

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) -> Checker<Self>

Initializes a single threaded model checker.

fn checker_with_threads(self, thread_count: usize) -> Checker<Self>

Initializes a model checker. The visitation order will be nondeterministic if thread_count > 1.

Loading content...

Implementors

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

type State = SystemState<S::Actor>

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

Loading content...