[−][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. Consider using `SystemState<Actor>` instead for simpler type signatures.

DuplicatingNetwork	Indicates whether the network duplicates messages. If duplication is disabled, messages are forgotten once delivered, which can improve model checking perfomance.
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().

Network	Represents a network of messages.
SystemState	A type alias that accepts an actor type and resolves the associated `Msg` and `State` types. Introduced because parameterizing `_SystemState` by `Actor` necessitates implementing extra traits.