Crate stateright

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 model submodule for a state machine implementation that can check a system of actors.

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 KeepPaths::No for faster model checking.

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.