Module stateright::checker

A Model checker.

Models can have sometimes and always properties. The model checker will attempt to discover an example of every sometimes property and a counterexample of every always property. Usually the absence of a sometimes example or the presence of an always counterexample indicates a problem with the implementation.

An example that solves a sliding puzzle follows.

use stateright::*;
use stateright::checker::*;

#[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
        })]
    }
}
let example = Puzzle(vec![1, 4, 2,
                          3, 5, 8,
                          6, 7, 0])
    .checker().check(100).example("solved");
assert_eq!(
    example,
    Some(Path(vec![
        (vec![1, 4, 2,
              3, 5, 8,
              6, 7, 0], Some(Slide::Down)),
        (vec![1, 4, 2,
              3, 5, 0,
              6, 7, 8], Some(Slide::Right)),
        (vec![1, 4, 2,
              3, 0, 5,
              6, 7, 8], Some(Slide::Down)),
        (vec![1, 0, 2,
              3, 4, 5,
              6, 7, 8], Some(Slide::Right)),
        (vec![0, 1, 2,
              3, 4, 5,
              6, 7, 8], None)])));

Additional examples are available in the repository.

Structs

Checker	Generates every state reachable by a model, and verifies that all properties hold. Can be instantiated with Model::checker() or Model::checker_with_threads(...).
Path	A path of states including actions. i.e. state --action--> state ... --action--> state. You can convert to a Vec<_> with path.into_vec(). If you only need the actions, then use path.into_actions().