Struct stateright::actor::SystemModel

pub struct SystemModel<S: System> {
    pub actors: Vec<S::Actor>,
    pub init_network: Vec<Envelope<<S::Actor as Actor>::Msg>>,
    pub lossy_network: LossyNetwork,
    pub duplicating_network: DuplicatingNetwork,
    pub system: S,
}

A model of an actor system.

Fields

actors: Vec<S::Actor>

init_network: Vec<Envelope<<S::Actor as Actor>::Msg>>

lossy_network: LossyNetwork

duplicating_network: DuplicatingNetwork

system: S

Trait Implementations

impl<S: Clone + System> Clone for SystemModel<S> where
    S::Actor: Clone,
    S::Actor: Clone, 

pub fn clone(&self) -> SystemModel<S>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<S: System> Model for SystemModel<S>

type State = SystemState<S>

The type of state upon which this model operates.

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

The type of action that transitions between states.

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

Returns the initial possible states.

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

Collects the subsequent possible actions based on a previous state.

pub fn next_state(
    &self,
    last_sys_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.

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

Summarizes the outcome of taking a step.

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

Draws a sequence diagram for the actor system.

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

Generates the expected properties for this model.

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

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

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

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

pub 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.

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

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

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

Instantiates a CheckerBuilder for this model.