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

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

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

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

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

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

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

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

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

    pub 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[src]

The type of actor for this system.

type History: Clone + Debug + Default + Hash[src]

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

pub fn actors(&self) -> Vec<Self::Actor>[src]

Defines the actors.

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

Generates the expected properties for this model.

Loading content...

Provided methods

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

Defines the initial network.

pub fn lossy_network(&self) -> LossyNetwork[src]

Defines whether the network loses messages or not.

pub fn duplicating_network(&self) -> DuplicatingNetwork[src]

Defines whether the network duplicates messages or not.

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

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,
    history: &Self::History,
    src: Id,
    dst: Id,
    msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>[src]

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

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

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

pub fn into_model(self) -> SystemModel<Self>[src]

Converts this system into a model that can be checked.

Loading content...

Implementors

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

type Actor = RegisterActor<ServerActor>

type History = LinearizabilityTester<Id, Register<TestValue>>

Loading content...