Module stateright::actor

This module provides an Actor trait, which can be model checked using ActorModel. 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::borrow::Cow;
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;
    type Timer = ();

    fn on_start(&self, _id: Id, o: &mut Out<Self>) -> Self::State {
        // The actor either bootstraps or starts at time zero.
        if let Some(peer_id) = self.bootstrap_to_id {
            o.send(peer_id, MsgWithTimestamp(1));
            Timestamp(1)
        } else {
            Timestamp(0)
        }
    }

    fn on_msg(&self, id: Id, state: &mut Cow<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.send(src, MsgWithTimestamp(timestamp + 1));
            *state.to_mut() = Timestamp(timestamp + 1);
        }
    }
}

// The model checker should quickly find a counterexample sequence of actions that causes an
// actor timestamp to reach a specified maximum.
let checker = ActorModel::new((), ())
    .actor(LogicalClockActor { bootstrap_to_id: None})
    .actor(LogicalClockActor { bootstrap_to_id: Some(Id::from(0)) })
    .property(Expectation::Always, "less than max", |_, state| {
        state.actor_states.iter().all(|s| s.0 < 3)
    })
    .checker().spawn_bfs().join();
checker.assert_discovery("less than max", vec![
    ActorModelAction::Deliver {
        src: Id::from(1),
        dst: Id::from(0),
        msg: MsgWithTimestamp(1),
    },
    ActorModelAction::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 RegisterMsg) and also provides RegisterActor for model checking.
• write_once_register
  Defines an interface for write-once-register-like actors (via WORegisterMsg) and also provides WORegisterActor for model checking.

Structs

• ActorModel
  Represents a system of Actors that communicate over a network. H indicates 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.
• ActorModelState
  Represents a snapshot in time for the entire actor system.
• Envelope
  Indicates the source and destination for a message.
• Id
  Uniquely identifies an Actor. Encodes the socket address for spawned actors. Encodes an index for model checked actors.
• Out
  Holds Commands output by an actor.
• Timers
  A collection of timers that have been set for a given actor.

Enums

• ActorModelAction
  Indicates possible steps that an actor system can take as it evolves.
• Command
  Commands with which an actor can respond.
• 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.
• Network
  Represents a network of messages.
• NetworkDeliverableIter
• NetworkIter

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.

Functions

• is_no_op
  If true, then the actor did not update its state or output commands.
• is_no_op_with_timer
  If true, then the actor did not update its state or output commands, besides renewing the same timer.
• 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 Ids 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.
• peer_ids
  A helper to generate peer Ids.
• spawn
  Runs an actor, sending messages over UDP. Blocks the current thread.