Struct stateright::CheckerBuilder [−][src]
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>
[src]
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,
[src]
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,
[src]
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,
[src]
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
[src]
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
[src]
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
[src]
self,
visitor: impl CheckerVisitor<M> + Send + Sync + 'static
) -> Self
Indicates a function to be run on each evaluated state.
Auto Trait Implementations
impl<M> !RefUnwindSafe for CheckerBuilder<M>
impl<M> Send for CheckerBuilder<M> where
M: Send,
M: Send,
impl<M> Sync for CheckerBuilder<M> where
M: Sync,
M: Sync,
impl<M> Unpin for CheckerBuilder<M> where
M: Unpin,
M: Unpin,
impl<M> !UnwindSafe for CheckerBuilder<M>
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
pub fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<V, T> VZip<V> for T where
V: MultiLane<T>,
V: MultiLane<T>,