Trait stateright::Checker[−][src]

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

    fn generated_count(&self) -> usize;

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

    fn join(self) -> Self;

    fn is_done(&self) -> bool;

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

    fn report(self, w: &mut impl Write) -> Self
    where
        M::Action: Debug,
        M::State: Debug,
        Self: Sized,
    { ... }

    fn discovery_classification(&self, name: &str) -> &'static str { ... }

    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[src]

Returns a reference to this checker’s Model.

fn generated_count(&self) -> usize[src]

Indicates how many states have been generated.

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

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

fn join(self) -> Self[src]

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

fn is_done(&self) -> bool[src]

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

Loading content...

Provided methods

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

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

fn report(self, w: &mut impl Write) -> Self where
    M::Action: Debug,
    M::State: Debug,
    Self: Sized, [src]

Periodically emits a status message.

fn discovery_classification(&self, name: &str) -> &'static str[src]

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

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

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>[src]

Panics if a particular discovery is not found.

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

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, [src]

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

Loading content...

Implementors

Loading content...