Trait stateright::CheckerVisitor

pub trait CheckerVisitor<M: Model> {
    // Required method
    fn visit(&self, model: &M, path: Path<M::State, M::Action>);
}

A visitor to apply to every Path of the checked Model.

Implementations include PathRecorder, StateRecorder, and impl<M: Model> Fn(Path<M::State, M::Action>).

Example

model.checker()
    .visitor(|p: Path<_, _>| println!("\t{:?}", p.last_state()))
    .spawn_dfs().join();

Required Methods

fn visit(&self, model: &M, path: Path<M::State, M::Action>)

The method to apply to every Path.

Implementations on Foreign Types

impl<M: Model> CheckerVisitor<M> for Arc<RwLock<Snapshot<M::Action>>>

fn visit(&self, _: &M, path: Path<M::State, M::Action>)

Implementors

impl<M> CheckerVisitor<M> for PathRecorder<M>where M: Model, M::Action: Eq + Hash, M::State: Eq + Hash,

impl<M> CheckerVisitor<M> for StateRecorder<M>where M: Model, M::State: Clone,

impl<M, F> CheckerVisitor<M> for Fwhere M: Model, F: Fn(Path<M::State, M::Action>),