Trait stateright::Checker

pub trait Checker<M: Model> {
    // Required methods
    fn model(&self) -> &M;
    fn state_count(&self) -> usize;
    fn unique_state_count(&self) -> usize;
    fn max_depth(&self) -> usize;
    fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>>;
    fn handles(&mut self) -> Vec<JoinHandle<()>>;
    fn is_done(&self) -> bool;

    // Provided methods
    fn check_fingerprint(&self, _fingerprint: NonZeroU64) { ... }
    fn run_to_completion(&self) { ... }
    fn join(self) -> Self
       where Self: Sized { ... }
    fn discovery(&self, name: &'static str) -> Option<Path<M::State, M::Action>> { ... }
    fn join_and_report<R>(self, reporter: &mut R) -> Self
       where M::Action: Debug,
             M::State: Debug + Hash,
             Self: Sized + Send + Sync,
             R: Reporter<M> + Send { ... }
    fn report<R>(self, reporter: &mut R) -> Self
       where M::Action: Debug,
             M::State: Debug + Hash,
             Self: Sized,
             R: Reporter<M> { ... }
    fn discovery_classification(&self, name: &str) -> DiscoveryClassification { ... }
    fn assert_properties(&self)
       where M::Action: Debug,
             M::State: Debug { ... }
    fn assert_any_discovery(
        &self,
        name: &'static str
    ) -> Path<M::State, M::Action> { ... }
    fn assert_no_discovery(&self, name: &'static str)
       where M::Action: Debug,
             M::State: Debug { ... }
    fn assert_discovery(&self, name: &'static str, actions: Vec<M::Action>)
       where M::State: Debug + PartialEq,
             M::Action: Debug + PartialEq { ... }
}

Implementations perform Model checking.

Call Model::checker to instantiate a CheckerBuilder. Then call CheckerBuilder::spawn_dfs or CheckerBuilder::spawn_bfs.

Required Methods

fn model(&self) -> &M

Returns a reference to this checker’s Model.

fn state_count(&self) -> usize

Indicate how many states have been generated including repeats. Always greater than or equal to Checker::unique_state_count.

fn unique_state_count(&self) -> usize

Indicates how many unique states have been generated. Always less than or equal to Checker::state_count.

fn max_depth(&self) -> usize

Indicates the maximum depth that has been explored.

fn discoveries(&self) -> HashMap<&'static str, Path<M::State, M::Action>>

Returns a map from property name to corresponding “discovery” (indicated by a Path).

fn handles(&mut self) -> Vec<JoinHandle<()>>

Extract the thread handles from this checker.

fn is_done(&self) -> bool

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

Provided Methods

fn check_fingerprint(&self, _fingerprint: NonZeroU64)

Asks the checker to check the given fingerprint if not done already.

fn run_to_completion(&self)

Asks the checker to run to completion, no longer waiting for fingerprints.

fn join(self) -> Selfwhere Self: Sized,

Blocks the current thread until checking is_done or each thread evaluates a specified maximum number of states.

fn discovery(&self, name: &'static str) -> Option<Path<M::State, M::Action>>

Looks up a discovery by property name. Panics if the property does not exist.

fn join_and_report<R>(self, reporter: &mut R) -> Selfwhere M::Action: Debug, M::State: Debug + Hash, Self: Sized + Send + Sync, R: Reporter<M> + Send,

Wait for all threads to finish whilst reporting, reporting the finish more accurately than the interval used for the reporting.

fn report<R>(self, reporter: &mut R) -> Selfwhere M::Action: Debug, M::State: Debug + Hash, Self: Sized, R: Reporter<M>,

Periodically emits a status message.

fn discovery_classification(&self, name: &str) -> DiscoveryClassification

Indicates whether a discovery is an "example" or "counterexample".

fn assert_properties(&self)where M::Action: Debug, M::State: Debug,

A helper that verifies examples exist for all sometimes properties and no counterexamples exist for any always/eventually properties.

fn assert_any_discovery(&self, name: &'static str) -> Path<M::State, M::Action>

Panics if a particular discovery is not found.

fn assert_no_discovery(&self, name: &'static str)where M::Action: Debug, M::State: Debug,

Panics if a particular discovery is found.

fn assert_discovery(&self, name: &'static str, actions: Vec<M::Action>)where M::State: Debug + PartialEq, M::Action: Debug + PartialEq,

Panics if the specified actions do not result in a discovery for the specified property name.

Implementors