[−][src]Trait stateright::actor::system::System

pub trait System: Sized {
    type Actor: Actor;
    type History: Clone + Debug + Default + Hash;
    fn actors(&self) -> Vec<Self::Actor>;

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

    fn init_network(&self) -> Vec<Envelope<<Self::Actor as Actor>::Msg>> { ... }

    fn lossy_network(&self) -> LossyNetwork { ... }

    fn duplicating_network(&self) -> DuplicatingNetwork { ... }

    fn record_msg_in(
        &self, 
        history: &Self::History, 
        src: Id, 
        dst: Id, 
        msg: &<Self::Actor as Actor>::Msg
    ) -> Option<Self::History> { ... }

    fn record_msg_out(
        &self, 
        history: &Self::History, 
        src: Id, 
        dst: Id, 
        msg: &<Self::Actor as Actor>::Msg
    ) -> Option<Self::History> { ... }

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

    fn into_model(self) -> SystemModel<Self> { ... }
}

Represents a system of actors that communicate over a network. Usage: let checker = my_system.into_model().checker().

Associated Types

type Actor: Actor

The type of actor for this system.

type History: Clone + Debug + Default + Hash

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.

Loading content...

Required methods

fn actors(&self) -> Vec<Self::Actor>

Defines the actors.

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

Generates the expected properties for this model.

Loading content...

Provided methods

fn init_network(&self) -> Vec<Envelope<<Self::Actor as Actor>::Msg>>

Defines the initial network.

fn lossy_network(&self) -> LossyNetwork

Defines whether the network loses messages or not.

fn duplicating_network(&self) -> DuplicatingNetwork

Defines whether the network duplicates messages or not.

fn record_msg_in(
    &self,
    history: &Self::History,
    src: Id,
    dst: Id,
    msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>

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

fn record_msg_out(
    &self,
    history: &Self::History,
    src: Id,
    dst: Id,
    msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>

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

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

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

fn into_model(self) -> SystemModel<Self>

Converts this system into a model that can be checked.

Loading content...

Implementors

impl<A, I> System for RegisterTestSystem<A, I> where
    A: Actor<Msg = RegisterMsg<TestRequestId, TestValue, I>> + Clone,
    I: Clone + Debug + Eq + Hash, [src]

type Actor = A

type History = RegisterHistory<TestRequestId, TestValue>

fn init_network(&self) -> Vec<Envelope<<Self::Actor as Actor>::Msg>>[src]

The following code sets up the network based on the requested put and get counts. Each operation has a unique request ID and network source, while puts also have a unique value. We derive all three from the same unique ID.

Loading content...