Struct stateright::checker::Checker

pub struct Checker<'a, SM: StateMachine> { /* fields omitted */ }

Generates every state reachable by a state machine, and verifies that all properties hold. Can be instantiated with model.checker().

Methods

impl<'a, SM: StateMachine> Checker<'a, SM> where
    SM: Sync,
    SM::State: Debug + Hash + Send + Sync,
    SM::Action: Debug, 

pub fn check(&mut self, max_count: usize) -> &mut Self

Visits up to a specified number of states checking the model's properties. May return earlier when all states have been checked or all the properties are resolved.

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

An example of a "sometimes" property. None indicates that the property exists but no example has been found. Will panic if a corresponding "sometimes" property does not exist.

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

A counterexaple of an "always" property. None indicates that the property exists but no counterexample has been found. Will panic if a corresponding "always" property does not exist.

pub fn check_and_report(&mut self, w: &mut impl Write)

Blocks the thread until model checking is complete. Periodically emits a status while checking, tailoring the block size to the checking speed. Emits a report when complete.

pub fn is_done(&'a self) -> bool

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

pub fn generated_count(&self) -> usize

Indicates how many states were generated during model checking.

pub fn generated_fingerprints(&self) -> HashSet<Fingerprint>

Extracts the fingerprints generated during model checking.