[−][src]Trait stateright::Checker
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.
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
M::Action: Debug,
M::State: Debug,
Self: Sized,
[src]
M::Action: Debug,
M::State: Debug,
Self: Sized,
Periodically emits a status message.
pub fn discovery_classification(&self, name: &str) -> &'static str
[src]
Indicates whether a discovery is an "example"
or "counterexample"
.
pub fn assert_properties(&self) where
M::Action: Debug,
M::State: Debug,
[src]
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.
pub fn assert_any_discovery(
&self,
name: &'static str
) -> Path<M::State, M::Action>
[src]
&self,
name: &'static str
) -> Path<M::State, M::Action>
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]
M::Action: Debug,
M::State: Debug,
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]
M::State: Debug + PartialEq,
M::Action: Debug + PartialEq,
Panics if the specified actions do not result in a discovery for the specified property name.