Struct stateright::CheckerBuilder

pub struct CheckerBuilder<M: Model> { /* private fields */ }

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.

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.

pub fn spawn_on_demand(self) -> impl Checker<M>where M: Model + Send + Sync + 'static, M::State: Hash + Send + Sync + 'static,

Spawns an on-demand model checker. This traversal strategy doesn’t compute any states until it is asked to, useful for lightweight exploration. Internally the exploration strategy is very similar to that of CheckerBuilder::spawn_bfs.

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

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 spawn_simulation<C>(self, seed: u64, chooser: C) -> impl Checker<M>where M: Model + Send + Sync + 'static, M::State: Hash + Send + Sync + 'static, C: Chooser<M>,

Spawns a simulation model checker. This repeatedly traverses the model from initial states to a terminal state. This aims to provide faster coverage of deep states for models that cannot practically be checked exhaustively.

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

pub fn symmetry(self) -> Selfwhere M::State: Representative,

Enables symmetry reduction. Requires the model state to implement Representative.

pub fn symmetry_fn(self, representative: fn(_: &M::State) -> M::State) -> Self

Enables symmetry reduction based on a representative function.

pub fn target_state_count(self, 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 target_max_depth(self, depth: usize) -> Self

Sets the maximum depth that the checker should aim to explore.

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.