Struct stateright::CheckerBuilder
source · pub struct CheckerBuilder<M: Model> { /* private fields */ }
Expand description
A Model
Checker
builder. Instantiable via the Model::checker
method.
Example
model.checker().threads(4).spawn_dfs().join().assert_properties();
Implementations§
source§impl<M: Model> CheckerBuilder<M>
impl<M: Model> CheckerBuilder<M>
sourcepub 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,
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.
sourcepub fn spawn_bfs(self) -> impl Checker<M>where
M: Model + Send + Sync + 'static,
M::State: Hash + Send + Sync + 'static,
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.
sourcepub fn spawn_on_demand(self) -> impl Checker<M>where
M: Model + Send + Sync + 'static,
M::State: Hash + Send + Sync + 'static,
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.
sourcepub fn spawn_dfs(self) -> impl Checker<M>where
M: Model + Send + Sync + 'static,
M::State: Hash + Send + Sync + 'static,
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.
sourcepub 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>,
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.
sourcepub fn symmetry(self) -> Selfwhere
M::State: Representative,
pub fn symmetry(self) -> Selfwhere M::State: Representative,
Enables symmetry reduction. Requires the model state to implement Representative
.
sourcepub fn symmetry_fn(self, representative: fn(_: &M::State) -> M::State) -> Self
pub fn symmetry_fn(self, representative: fn(_: &M::State) -> M::State) -> Self
Enables symmetry reduction based on a representative function.
sourcepub fn target_state_count(self, count: usize) -> Self
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.
sourcepub fn target_max_depth(self, depth: usize) -> Self
pub fn target_max_depth(self, depth: usize) -> Self
Sets the maximum depth that the checker should aim to explore.
sourcepub fn threads(self, thread_count: usize) -> Self
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.
sourcepub fn visitor(
self,
visitor: impl CheckerVisitor<M> + Send + Sync + 'static
) -> Self
pub fn visitor( self, visitor: impl CheckerVisitor<M> + Send + Sync + 'static ) -> Self
Indicates a function to be run on each evaluated state.