[−][src]Module stateright::actor
This module provides an Actor trait, which can be model checked by implementing
System and calling System::into_model(). You can also spawn()
the actor
in which case it will communicate over a UDP socket.
Example
In the following example two actors track events with logical clocks. A false claim is made that a clock will never reach 3, which the checker disproves by demonstrating that the actors continue sending messages back and forth (therefore increasing their clocks) after an initial message is sent.
use stateright::*; use stateright::actor::*; use std::iter::FromIterator; use std::sync::Arc; /// The actor needs to know whether it should "bootstrap" by sending the first /// message. If so, it needs to know to which peer the message should be sent. struct LogicalClockActor { bootstrap_to_id: Option<Id> } /// Actor state is simply a "timestamp" sequencer. #[derive(Clone, Debug, Eq, Hash, PartialEq)] struct Timestamp(u32); /// And we define a generic message containing a timestamp. #[derive(Clone, Debug, Eq, Hash, PartialEq)] struct MsgWithTimestamp(u32); impl Actor for LogicalClockActor { type Msg = MsgWithTimestamp; type State = Timestamp; fn on_start(&self, _id: Id, o: &mut Out<Self>) { // The actor either bootstraps or starts at time zero. if let Some(peer_id) = self.bootstrap_to_id { o.set_state(Timestamp(1)); o.send(peer_id, MsgWithTimestamp(1)); } else { o.set_state(Timestamp(0)); } } fn on_msg(&self, id: Id, state: &Self::State, src: Id, msg: Self::Msg, o: &mut Out<Self>) { // Upon receiving a message, the actor updates its timestamp and replies. let MsgWithTimestamp(timestamp) = msg; if timestamp > state.0 { o.set_state(Timestamp(timestamp + 1)); o.send(src, MsgWithTimestamp(timestamp + 1)); } } } /// We now define the actor system, which we parameterize by the maximum /// expected timestamp. struct LogicalClockSystem { max_expected: u32 }; impl System for LogicalClockSystem { type Actor = LogicalClockActor; type History = (); /// The system contains two actors, one of which bootstraps. fn actors(&self) -> Vec<Self::Actor> { vec![ LogicalClockActor { bootstrap_to_id: None}, LogicalClockActor { bootstrap_to_id: Some(Id::from(0)) } ] } /// The only property is one indicating that every actor's timestamp is less than the /// maximum expected timestamp defined for the system. fn properties(&self) -> Vec<Property<SystemModel<Self>>> { vec![Property::<SystemModel<Self>>::always("less than max", |model, state| { state.actor_states.iter().all(|s| s.0 < model.system.max_expected) })] } } // The model checker should quickly find a counterexample sequence of actions that causes an // actor timestamp to reach a specified maximum. let checker = LogicalClockSystem { max_expected: 3 } .into_model().checker().spawn_bfs().join(); checker.assert_discovery("less than max", vec![ SystemAction::Deliver { src: Id::from(1), dst: Id::from(0), msg: MsgWithTimestamp(1) }, SystemAction::Deliver { src: Id::from(0), dst: Id::from(1), msg: MsgWithTimestamp(2) }, ]); assert_eq!( checker.discovery("less than max").unwrap().last_state().actor_states, vec![Arc::new(Timestamp(2)), Arc::new(Timestamp(3))]);
Additional examples are available in the repository.
Modules
ordered_reliable_link | An ordered reliable link (ORL) based loosely on the "perfect link" described in "Introduction to Reliable and Secure Distributed Programming" by Cachin, Guerraoui, and Rodrigues (with enhancements to provide ordering). |
register | Defines an interface for register-like actors (via |
Structs
Envelope | Indicates the source and destination for a message. |
Id | Uniquely identifies an |
Out | Groups outputs to make function types more concise when implementing an actor. |
SystemModel | A model of an actor system. |
SystemState | Represents a snapshot in time for the entire actor system. |
Enums
Command | Commands with which an actor can respond. |
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. |
Traits
Actor | An actor initializes internal state optionally emitting outputs; then it waits for incoming events, responding by updating its internal state and optionally emitting outputs. |
System | Represents a system of actors that communicate over a network.
Usage: |
Functions
majority | Indicates the number of nodes that constitute a majority for a particular cluster size. |
model_peers | A helper to generate a list of peer |
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. |
spawn | Runs an actor, sending messages over UDP. |
Type Definitions
Network | Represents a network of messages. |