Trait stateright::Checker

pub trait Checker<M: Model> {
    pub fn model(&self) -> &M;
    pub fn generated_count(&self) -> usize;
    pub fn discoveries(
        &self
    ) -> HashMap<&'static str, Path<M::State, M::Action>>;
    pub fn join(self) -> Self;
    pub fn is_done(&self) -> bool;

    pub fn serve(self, addresses: impl ToSocketAddrs) -> Arc<Self>
    where
        M: 'static + Model,
        M::Action: Debug,
        M::State: Debug + Hash,
        Self: 'static + Send + Sized + Sync,
    { ... }
    pub fn discovery(
        &self, 
        name: &'static str
    ) -> Option<Path<M::State, M::Action>> { ... }
    pub fn report(self, w: &mut impl Write) -> Self
    where
        Self: Sized,
    { ... }
    pub fn assert_properties(&self)
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }
    pub fn assert_any_discovery(
        &self, 
        name: &'static str
    ) -> Path<M::State, M::Action> { ... }
    pub fn assert_no_discovery(&self, name: &'static str)
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }
    pub fn assert_discovery(&self, name: &'static str, actions: Vec<M::Action>)
    where
        M::State: Debug + PartialEq,
        M::Action: Debug + PartialEq,
    { ... }
}

Implementations perform Model checking.

Call Model::checker to instantiate a CheckerBuilder. Then call CheckerBuilder::spawn_dfs or CheckerBuilder::spawn_bfs.

Required methods

pub fn model(&self) -> &M

Returns a reference to this checker's Model.

pub fn generated_count(&self) -> usize

Indicates how many states have been generated.

pub fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>>

Returns a map from property name to corresponding "discovery" (indicated by a Path).

pub fn join(self) -> Self

Blocks the current thread until checking is_done or each thread evaluates a specified maximum number of states.

pub fn is_done(&self) -> bool

Indicates that either all properties have associated discoveries or all reachable states have been visited.

Loading content...

Provided methods

pub fn serve(self, addresses: impl ToSocketAddrs) -> Arc<Self> where
    M: 'static + Model,
    M::Action: Debug,
    M::State: Debug + Hash,
    Self: 'static + Send + Sized + Sync, 

Starts a web service for interactively exploring a model.

Demo

You can explore an abstract model for two phase commit at demo.stateright.rs.

Example

use stateright::{Checker, Model};

#[derive(Clone, Debug, Hash)]
enum FizzBuzzAction { Fizz, Buzz, FizzBuzz }
#[derive(Clone)]
struct FizzBuzzModel { max: usize }

impl Model for FizzBuzzModel {
    type State = Vec<(usize, Option<FizzBuzzAction>)>;
    type Action = Option<FizzBuzzAction>;
    fn init_states(&self) -> Vec<Self::State> {
        vec![Vec::new()]
    }
    fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
        actions.push(
            if state.len() % 15 == 0 {
                Some(FizzBuzzAction::FizzBuzz)
            } else if state.len() % 5 == 0 {
                Some(FizzBuzzAction::Buzz)
            } else if state.len() % 3 == 0 {
                Some(FizzBuzzAction::Fizz)
            } else {
                None
            });
    }
    fn next_state(&self, state: &Self::State, action: Self::Action) -> Option<Self::State> {
        let mut state = state.clone();
        state.push((state.len(), action));
        Some(state)
    }
    fn within_boundary(&self, state: &Self::State) -> bool {
        state.len() <= self.max
    }
}

let _ = FizzBuzzModel { max: 30 }.checker().spawn_dfs().serve("localhost:3000");

API

• GET / returns a web browser UI as HTML.
• GET /.status returns information about the model checker status.
• GET /.states returns available initial states and fingerprints.
• GET /.states/{fingerprint1}/{fingerprint2}/... follows the specified path of fingerprints and returns available actions with resulting states and fingerprints.
• GET /.states/.../{invalid-fingerprint} returns 404.

pub fn discovery(&self, name: &'static str) -> Option<Path<M::State, M::Action>>

Looks up a discovery by property name. Panics if the property does not exist.

pub fn report(self, w: &mut impl Write) -> Self where
    Self: Sized, 

Periodically emits a status message.

pub fn assert_properties(&self) where
    M::Action: Debug,
    M::State: Debug, 

A helper that verifies examples exist for all sometimes properties and no counterexamples exist for any always/eventually properties.

pub fn assert_any_discovery(
    &self,
    name: &'static str
) -> Path<M::State, M::Action>

Panics if a particular discovery is not found.

pub fn assert_no_discovery(&self, name: &'static str) where
    M::Action: Debug,
    M::State: Debug, 

Panics if a particular discovery is found.

pub fn assert_discovery(&self, name: &'static str, actions: Vec<M::Action>) where
    M::State: Debug + PartialEq,
    M::Action: Debug + PartialEq, 

Panics if the specified actions do not result in a discovery for the specified property name.

Loading content...

Implementors

Loading content...