[−][src]Trait stateright::Checker

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

    pub fn generated_count(&self) -> usize;

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

    pub fn join(self) -> Self;

    pub fn is_done(&self) -> bool;

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

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

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

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

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

    pub 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

pub fn model(&self) -> &M[src]

Returns a reference to this checker's Model.

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

Indicates how many states have been generated.

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

pub fn join(self) -> Self[src]

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

pub 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

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

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

Periodically emits a status message.

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

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

Panics if a particular discovery is not found.

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

Panics if a particular discovery is found.

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