[−][src]Crate stateright

A library for model checking systems, with an emphasis on distributed systems.

Most of the docs are here, but a short book is being written to provide a gentler introduction: "Building Distributed Systems With Stateright."

Introduction to Model Checking

Model implementations indicate how a system evolves, such as a set of actors executing a distributed protocol on an IP network. Incidentally, that scenario is so common for model checking that Stateright includes an actor System model, and unlike many model checkers, Stateright is also able to spawn these actors on a real network.

Models of a system are supplemented with always and sometimes properties. An always Property (also known as a safety property or invariant) indicates that a specific problematic outcome is not possible, such as data inconsistency. A sometimes property on the other hand is used to ensure a particular outcome is reachable, such as the ability for a distributed system to process a write request.

A Checker will attempt to discover a counterexample for every always property and an example for every sometimes property, and these examples/counterexamples are indicated by sequences of system steps known as Paths (also known as traces or behaviors). The presence of an always discovery or the absence of a sometimes discovery indicate that the model checker identified a problem with the code under test.

Example

A toy example that solves a sliding puzzle follows. Caveat: this simple example leverages only a sometimes property, but in most cases for a real scenario you would have an always property at a minimum.

TIP: see the actor module documentation for an actor system example. More sophisticated examples are available in the examples/ directory of the repository

use stateright::*;

#[derive(Clone, Debug, Eq, PartialEq)]
enum Slide { Down, Up, Right, Left }

struct Puzzle(Vec<u8>);
impl Model for Puzzle {
    type State = Vec<u8>;
    type Action = Slide;

    fn init_states(&self) -> Vec<Self::State> {
        vec![self.0.clone()]
    }

    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
        actions.append(&mut vec![
            Slide::Down, Slide::Up, Slide::Right, Slide::Left
        ]);
    }

    fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
        let empty = last_state.iter().position(|x| *x == 0).unwrap();
        let empty_y = empty / 3;
        let empty_x = empty % 3;
        let maybe_from = match action {
            Slide::Down  if empty_y > 0 => Some(empty - 3), // above
            Slide::Up    if empty_y < 2 => Some(empty + 3), // below
            Slide::Right if empty_x > 0 => Some(empty - 1), // left
            Slide::Left  if empty_x < 2 => Some(empty + 1), // right
            _ => None
        };
        maybe_from.map(|from| {
            let mut next_state = last_state.clone();
            next_state[empty] = last_state[from];
            next_state[from] = 0;
            next_state
        })
    }

    fn properties(&self) -> Vec<Property<Self>> {
        vec![Property::sometimes("solved", |_, state: &Vec<u8>| {
            let solved = vec![0, 1, 2,
                              3, 4, 5,
                              6, 7, 8];
            state == &solved
        })]
    }
}
Puzzle(vec![1, 4, 2,
            3, 5, 8,
            6, 7, 0])
    .checker().spawn_bfs().join().assert_discovery("solved", vec![
        Slide::Down,
        // ... results in:
        //       [1, 4, 2,
        //        3, 5, 0,
        //        6, 7, 8]
        Slide::Right,
        // ... results in:
        //       [1, 4, 2,
        //        3, 0, 5,
        //        6, 7, 8]
        Slide::Down,
        // ... results in:
        //       [1, 0, 2,
        //        3, 4, 5,
        //        6, 7, 8]
        Slide::Right,
        // ... results in:
        //       [0, 1, 2,
        //        3, 4, 5,
        //        6, 7, 8]
    ]);

What to Read Next

The actor and semantics submodules will be of particular interest to most individuals.

Also, as mentioned earlier, you can find more examples in the Stateright repository.

Modules

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.
semantics	This module provides code to define and verify the correctness of an object or system based on how it responds to a collection of potentially concurrent (i.e. partially ordered) operations.
util	Utilities such as `HashableHashSet` and `HashableHashMap`. Those two in particular are useful because the corresponding `HashSet` and `HashMap` do not implement `Hash`, meaning they cannot be used directly in models.

Structs

CheckerBuilder	A `Model` `Checker` builder. Instantiable via the `Model::checker` method.
Path	A path of states including actions. i.e. `state --action--> state ... --action--> state`.
Property	A named predicate, such as "an epoch sometimes has no leader" (for which the the model checker would find an example) or "an epoch always has at most one leader" (for which the model checker would find a counterexample) or "a proposal is eventually accepted" (for which the model checker would find a counterexample path leading from the initial state through to a terminal state).
StateRecorder	A `CheckerVisitor` that records states evaluated by the model checker. Does not record generated states that are still pending property evaluation.

Enums

Expectation

Indicates whether a property is always, eventually, or sometimes true.

Traits

Checker	Implementations perform `Model` checking.
CheckerVisitor	A visitor to apply to every `Path` of the checked `Model`.
Model	This is the primary abstraction for Stateright. Implementations model a nondeterministic system's evolution. If you are using Stateright's actor framework, then you do not need to implement this interface and can instead implement `actor::Actor` and `actor::System`.