[−][src]Trait stateright::ModelChecker

pub trait ModelChecker<M: Model> {
    fn model(&self) -> &M;

    fn generated_count(&self) -> usize;

    fn pending_count(&self) -> usize;

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

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

    fn is_done(&self) -> bool { ... }

    fn example(&self, name: &'static str) -> Option<Path<M::State, M::Action>> { ... }

    fn counterexample(
        &self, 
        name: &'static str
    ) -> Option<Path<M::State, M::Action>> { ... }

    fn check_and_report(&mut self, w: &mut impl Write)
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }

    fn assert_properties(&self) -> &Self
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }

    fn assert_example(&self, name: &'static str) -> Path<M::State, M::Action> { ... }

    fn assert_counterexample(
        &self, 
        name: &'static str
    ) -> Path<M::State, M::Action> { ... }

    fn assert_no_example(&self, name: &'static str)
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }

    fn assert_no_counterexample(&self, name: &'static str)
    where
        M::Action: Debug,
        M::State: Debug,
    { ... }
}

A trait providing convenience methods for Model checkers. Implemented by BfsChecker and DfsChecker.

Required methods

fn model(&self) -> &M

Returns a reference to this checker's Model.

fn generated_count(&self) -> usize

Indicates how many states have been generated.

fn pending_count(&self) -> usize

Indicates how many generated states are pending verification.

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 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.

Loading content...

Provided methods

fn is_done(&self) -> bool

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

fn example(&self, name: &'static str) -> Option<Path<M::State, M::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.

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

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

fn check_and_report(&mut self, w: &mut impl Write) where
    M::Action: Debug,
    M::State: Debug, 

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.

fn assert_properties(&self) -> &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_example(&self, name: &'static str) -> Path<M::State, M::Action>

Panics if an example is not found. Otherwise returns a path to the example.

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

Panics if a counterexample is not found. Otherwise returns a path to the counterexample.

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

Panics if an example is found.

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

Panics if a counterexample is found.

Loading content...

Implementors

impl<M> ModelChecker<M> for BfsChecker<M> where
    M: Model + Sync,
    M::State: Hash + Send + Sync, [src]

impl<M> ModelChecker<M> for DfsChecker<M> where
    M: Model,
    M::State: Hash, [src]

Loading content...