Struct stateright::StateRecorder
source · pub struct StateRecorder<M: Model>(_);
Expand description
A CheckerVisitor
that records states evaluated by the model checker. Does not record
generated states that are still pending property evaluation.
Example
let (recorder, accessor) = StateRecorder::new_with_accessor();
model.checker().visitor(recorder).spawn_dfs().join();
assert_eq!(accessor(), expected_states);
Implementations§
source§impl<M> StateRecorder<M>where
M: Model,
M::State: Clone,
impl<M> StateRecorder<M>where M: Model, M::State: Clone,
sourcepub fn new_with_accessor() -> (Self, impl Fn() -> Vec<M::State>)
pub fn new_with_accessor() -> (Self, impl Fn() -> Vec<M::State>)
Instantiates a (StateRecorder
, accessor) pair.
Trait Implementations§
Auto Trait Implementations§
impl<M> RefUnwindSafe for StateRecorder<M>
impl<M> Send for StateRecorder<M>where <M as Model>::State: Send,
impl<M> Sync for StateRecorder<M>where <M as Model>::State: Send,
impl<M> Unpin for StateRecorder<M>
impl<M> UnwindSafe for StateRecorder<M>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more