Module stateright::actor

This module provides an actor abstraction. See the system submodule for model checking. See the spawn submodule for a runtime that can run your actor over a real network. See the register submodule for an example wrapper.

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 stateright::actor::system::*;
use stateright::checker::*;
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 counterexample = LogicalClockSystem { max_expected: 3 }
    .into_model().checker().check(1_000)
    .assert_counterexample("less than max");
assert_eq!(
    counterexample.last_state().actor_states,
    vec![Arc::new(Timestamp(2)), Arc::new(Timestamp(3))]);
assert_eq!(
    counterexample.into_actions(),
    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) }]);

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 RegisterMsg) and also provides RegisterTestSystem for model checking.
spawn	A simple runtime for executing an actor mapping messages to JSON over UDP.
system	Models semantics for an actor system on a lossy network that can redeliver messages.

Structs

Id	Uniquely identifies an Actor. Encodes the socket address for spawned actors. Encodes an index for model checked actors.
Out	Groups outputs to make function types more concise when implementing an actor.

Enums

Command

Commands with which an actor can respond.

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. At the moment, the only inputs and outputs relate to messages, but other events like timers will likely be added.