[−][src]Module stateright::actor::system

Models semantics for an actor system on a lossy network that can redeliver messages.

Structs

Envelope	Indicates the source and destination for a message.
SystemModel	A model of an actor system.
SystemState	Represents a snapshot in time for the entire actor system.

DuplicatingNetwork	Indicates whether the network duplicates messages. If duplication is disabled, messages are forgotten once delivered, which can improve model checking performance.
LossyNetwork	Indicates whether the network loses messages. Note that as long as invariants do not check the network state, losing a message is indistinguishable from an unlimited delay, so in many cases you can improve model checking performance by not modeling message loss.
SystemAction	Indicates possible steps that an actor system can take as it evolves.

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

model_peers	A helper to generate a list of peer `Id`s given an actor count and the index of a particular actor.
model_timeout	The specific timeout value is not relevant for model checking, so this helper can be used to generate an arbitrary timeout range. The specific value is subject to change, so this helper must only be used for model checking.

Represents a network of messages.