Crate stateright[−][src]
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::ActorModel
,
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 Path
s (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. This simple example leverages only a sometimes
property,
but in most cases for a real system you would have an always
property at
a minimum. The imagined use case is one in which we must ensure that a particular
configuration of the puzzle has a solution.
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([u8; 9]); impl Model for Puzzle { type State = [u8; 9]; type Action = Slide; fn init_states(&self) -> Vec<Self::State> { vec![self.0] } 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; next_state[empty] = last_state[from]; next_state[from] = 0; next_state }) } fn properties(&self) -> Vec<Property<Self>> { vec![Property::<Self>::sometimes("solved", |_, state| { let solved = [0, 1, 2, 3, 4, 5, 6, 7, 8]; state == &solved })] } } let checker = Puzzle([1, 4, 2, 3, 5, 8, 6, 7, 0]) .checker().spawn_bfs().join(); checker.assert_properties(); checker.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 using |
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 |
Structs
CheckerBuilder | A |
Path | A path of states including actions. i.e. |
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 |
Enums
Expectation | Indicates whether a property is always, eventually, or sometimes true. |
Traits
Checker | Implementations perform |
CheckerVisitor | |
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 leverage
|