Crate stateright
source ·Expand description
A library for specifying state machines and model checking invariants.
A small example follows. Please see the README for a more thorough introduction.
use stateright::*;
struct BinaryClock { start: u8 }
impl StateMachine for BinaryClock {
type State = u8;
fn init(&self, results: &mut StepVec<Self::State>) {
results.push(("start", self.start));
}
fn next(&self, state: &Self::State, results: &mut StepVec<Self::State>) {
results.push(("flip bit", (1 - *state)));
}
}
let mut checker = BinaryClock { start: 1 }.checker(
|clock, time| 0 <= *time && *time <= 1);
assert_eq!(
checker.check(100),
CheckResult::Pass);
assert_eq!(
checker.path_to(&0),
vec![("start", 1), ("flip bit", 0)]);
Modules
This module provides an actor abstraction. See the
model
submodule for a state machine
implementation that can check a system of actors.Macros
Provides a DSL to eliminate some boilerplate for defining an actor.
Structs
Generates every state reachable by a state machine, and verifies that an invariant holds.
Enums
Model checking can be time consuming, so the library checks up to a fixed number of states then
returns. This approach allows the library to avoid tying up a thread indefinitely while still
maintaining adequate performance. This type represents the result of one of those checking
passes.
Traits
Defines how a state begins and evolves, possibly nondeterministically.