Struct stateright::CheckerBuilder

#[must_use =
  "This code constructs a builder, not a checker. \
              Consider calling spawn_bfs() or spawn_dfs()."]pub struct CheckerBuilder<M: Model> { /* fields omitted */ }

A Model Checker builder. Instantiable via the Model::checker method.

Example

model.checker().threads(4).spawn_dfs().join().assert_properties();

Implementations

impl<M: Model> CheckerBuilder<M>

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

Starts a web service for interactively exploring a model (demo).

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().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.

#[must_use = "Checkers run on background threads. \ Consider calling join() or report(...), for example."]pub fn spawn_bfs(self) -> impl Checker<M> where
    M: Model + Send + Sync + 'static,
    M::State: Hash + Send + Sync + 'static, 

Spawns a breadth-first search model checker. This traversal strategy uses more memory than CheckerBuilder::spawn_dfs but will find the shortest Path to each discovery if checking is single threadeded (the default behavior, which CheckerBuilder::threads overrides).

This call does not block the current thread. Call Checker::join to block until checking completes.

#[must_use = "Checkers run on background threads. \ Consider calling join() or report(...), for example."]pub fn spawn_dfs(self) -> impl Checker<M> where
    M: Model + Send + Sync + 'static,
    M::State: Hash + Send + Sync + 'static, 

Spawns a depth-first search model checker. This traversal strategy uses dramatically less memory than CheckerBuilder::spawn_bfs at the cost of not finding the shortest Path to each discovery.

This call does not block the current thread. Call Checker::join to block until checking completes.

pub fn target_generated_count(self, target_generated_count: usize) -> Self

Sets the number of states that the checker should aim to generate. For performance reasons the checker may exceed this number, but it will never generate fewer states if more exist.

pub fn threads(self, thread_count: usize) -> Self

Sets the number of threads available for model checking. For maximum performance this should match the number of cores.

pub fn visitor(
    self,
    visitor: impl CheckerVisitor<M> + Send + Sync + 'static
) -> Self

Indicates a function to be run on each evaluated state.