Struct stateright::Checker [−][src]
pub struct Checker<'a, SM, I> where
SM: 'a + StateMachine,
I: Fn(&SM, &SM::State) -> bool, { pub visited: FxHashSet<u64>, // some fields omitted }
Visits every state reachable by a state machine, and verifies that an invariant holds.
Fields
visited: FxHashSet<u64>
Methods
impl<'a, SM, I> Checker<'a, SM, I> where
SM: 'a + StateMachine,
SM::State: Hash,
I: Fn(&SM, &SM::State) -> bool, [src]
impl<'a, SM, I> Checker<'a, SM, I> where
SM: 'a + StateMachine,
SM::State: Hash,
I: Fn(&SM, &SM::State) -> bool, pub fn check(&mut self, max_count: usize) -> CheckResult<SM::State>[src]
pub fn check(&mut self, max_count: usize) -> CheckResult<SM::State>Visits up to a specified number of states checking the model's invariant. May return earlier when all states have been visited or a state is found in which the invariant fails to hold.
pub fn path_to(&self, state: &SM::State) -> Option<Vec<Step<SM::State>>>[src]
pub fn path_to(&self, state: &SM::State) -> Option<Vec<Step<SM::State>>>Identifies the action-state "behavior" path by which a visited state was reached.
pub fn check_and_report(&mut self) where
SM::State: Debug, [src]
pub fn check_and_report(&mut self) where
SM::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.