Trait stateright::actor::System [−][src]
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.
Required methods
fn actors(&self) -> Vec<Self::Actor>
[src]
Defines the actors.
fn properties(&self) -> Vec<Property<SystemModel<Self>>>
[src]
Generates the expected properties for this model.
Provided methods
fn init_network(&self) -> Vec<Envelope<<Self::Actor as Actor>::Msg>>
[src]
Defines the initial network.
fn lossy_network(&self) -> LossyNetwork
[src]
Defines whether the network loses messages or not.
fn duplicating_network(&self) -> DuplicatingNetwork
[src]
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>
[src]
&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>
[src]
&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
[src]
Indicates whether a state is within the state space that should be model checked.
fn into_model(self) -> SystemModel<Self>
[src]
Converts this system into a model that can be checked.
Implementors
impl<ServerActor, InternalMsg> System for RegisterTestSystem<ServerActor, InternalMsg> where
ServerActor: Actor<Msg = RegisterMsg<TestRequestId, TestValue, InternalMsg>> + Clone,
InternalMsg: Clone + Debug + Eq + Hash,
[src]
ServerActor: Actor<Msg = RegisterMsg<TestRequestId, TestValue, InternalMsg>> + Clone,
InternalMsg: Clone + Debug + Eq + Hash,
type Actor = RegisterActor<ServerActor>
type History = LinearizabilityTester<Id, Register<TestValue>>
fn actors(&self) -> Vec<Self::Actor>
[src]
fn lossy_network(&self) -> LossyNetwork
[src]
fn duplicating_network(&self) -> DuplicatingNetwork
[src]
fn record_msg_out(
&self,
history: &Self::History,
src: Id,
_dst: Id,
msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>
[src]
&self,
history: &Self::History,
src: Id,
_dst: Id,
msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>
fn record_msg_in(
&self,
history: &Self::History,
_src: Id,
dst: Id,
msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>
[src]
&self,
history: &Self::History,
_src: Id,
dst: Id,
msg: &<Self::Actor as Actor>::Msg
) -> Option<Self::History>