Crate stateright[−][src]
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( KeepPaths::Yes, |clock, time| 0 <= *time && *time <= 1); assert_eq!( checker.check(100), CheckResult::Pass); assert_eq!( checker.path_to(&0), Some(vec![("start", 1), ("flip bit", 0)]));
Modules
actor |
This module provides an actor abstraction. See the |
Macros
actor |
Provides a DSL to eliminate some boilerplate for defining an actor. |
Structs
Checker |
Visits every state reachable by a state machine, and verifies that an invariant holds. |
Enums
CheckResult |
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. |
KeepPaths |
Use |
Traits
StateMachine |
Defines how a state begins and evolves, possibly nondeterministically. |
Type Definitions
Step |
Represents an action-state pair. |
StepVec |
Represents the range of action-state pairs that a state machine can follow during a step. |