Struct stateright::actor::ActorModel

pub struct ActorModel<A, C = (), H = ()>where
    A: Actor,
    H: Clone + Debug + Hash,{
    pub actors: Vec<A>,
    pub cfg: C,
    pub init_history: H,
    pub init_network: Network<A::Msg>,
    pub lossy_network: LossyNetwork,
    pub max_crashes: usize,
    pub properties: Vec<Property<ActorModel<A, C, H>>>,
    pub record_msg_in: fn(cfg: &C, history: &H, envelope: Envelope<&A::Msg>) -> Option<H>,
    pub record_msg_out: fn(cfg: &C, history: &H, envelope: Envelope<&A::Msg>) -> Option<H>,
    pub within_boundary: fn(cfg: &C, state: &ActorModelState<A, H>) -> bool,
}

Represents a system of Actors that communicate over a network. H indicates the type of history to maintain as auxiliary state, if any. See Auxiliary Variables in TLA for a thorough introduction to that concept. Use () if history is not needed to define the relevant properties of this system.

Fields

actors: Vec<A>

cfg: C

init_history: H

init_network: Network<A::Msg>

lossy_network: LossyNetwork

max_crashes: usize

Maximum number of actors that can be contemporarily crashed

properties: Vec<Property<ActorModel<A, C, H>>>

record_msg_in: fn(cfg: &C, history: &H, envelope: Envelope<&A::Msg>) -> Option<H>

record_msg_out: fn(cfg: &C, history: &H, envelope: Envelope<&A::Msg>) -> Option<H>

within_boundary: fn(cfg: &C, state: &ActorModelState<A, H>) -> bool

Implementations

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

pub fn new(cfg: C, init_history: H) -> ActorModel<A, C, H>

Initializes an ActorModel with a specified configuration and history.

pub fn actor(self, actor: A) -> Self

Adds another Actor to this model.

pub fn actors(self, actors: impl IntoIterator<Item = A>) -> Self

Adds multiple Actors to this model.

pub fn init_network(self, init_network: Network<A::Msg>) -> Self

Defines the initial network.

pub fn lossy_network(self, lossy_network: LossyNetwork) -> Self

Defines whether the network loses messages or not.

pub fn max_crashes(self, max_crashes: usize) -> Self

Specifies the maximum number of actors that can be contemporarily crashed

pub fn property( self, expectation: Expectation, name: &'static str, condition: fn(_: &ActorModel<A, C, H>, _: &ActorModelState<A, H>) -> bool ) -> Self

Adds a Property to this model.

pub fn record_msg_in( self, record_msg_in: fn(cfg: &C, history: &H, _: Envelope<&A::Msg>) -> Option<H> ) -> Self

Defines whether/how an incoming message contributes to relevant history. Returning Some(new_history) updates the relevant history, while None does not.

pub fn record_msg_out( self, record_msg_out: fn(cfg: &C, history: &H, _: Envelope<&A::Msg>) -> Option<H> ) -> Self

Defines whether/how an outgoing message contributes to relevant history. Returning Some(new_history) updates the relevant history, while None does not.

pub fn within_boundary( self, within_boundary: fn(cfg: &C, state: &ActorModelState<A, H>) -> bool ) -> Self

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

Trait Implementations

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

fn clone(&self) -> ActorModel<A, C, H>

Returns a copy of the value.

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

Performs copy-assignment from source.

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

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

Draws a sequence diagram for the actor system.

type State = ActorModelState<A, H>

The type of state upon which this model operates.

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

The type of action that transitions between states.

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

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

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 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 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 property(&self, name: &'static str) -> Property<Self>

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