1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
use crate::{Model, Path};
use std::collections::HashSet;
use std::hash::Hash;
use std::sync::{Arc, Mutex};
/// 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
///
/// ```
/// # use stateright::*; let model = ();
/// model.checker()
/// .visitor(|p: Path<_, _>| println!("\t{:?}", p.last_state()))
/// .spawn_dfs().join();
/// ```
pub trait CheckerVisitor<M: Model> {
/// The method to apply to every [`Path`].
fn visit(&self, model: &M, path: Path<M::State, M::Action>);
}
impl<M, F> CheckerVisitor<M> for F
where
M: Model,
F: Fn(Path<M::State, M::Action>),
{
fn visit(&self, _: &M, path: Path<M::State, M::Action>) {
self(path)
}
}
/// A [`CheckerVisitor`] that records paths visited by the model checker.
///
/// # Example
///
/// ```
/// # use stateright::*; let model = ();
/// # let expected_paths = vec![
/// # Path::from_actions(&model, (), Vec::new()).unwrap(),
/// # ].into_iter().collect();
/// let (recorder, accessor) = PathRecorder::new_with_accessor();
/// model.checker().visitor(recorder).spawn_dfs().join();
/// assert_eq!(accessor(), expected_paths);
/// ```
#[allow(clippy::type_complexity)]
pub struct PathRecorder<M: Model>(Arc<Mutex<HashSet<Path<M::State, M::Action>>>>);
impl<M> CheckerVisitor<M> for PathRecorder<M>
where
M: Model,
M::Action: Eq + Hash,
M::State: Eq + Hash,
{
fn visit(&self, _: &M, path: Path<M::State, M::Action>) {
self.0.lock().unwrap().insert(path);
}
}
impl<M> PathRecorder<M>
where
M: Model,
M::Action: Clone,
M::State: Clone,
{
/// Instantiates a ([`PathRecorder`], accessor) pair.
pub fn new_with_accessor() -> (Self, impl Fn() -> HashSet<Path<M::State, M::Action>>) {
let recorder = Self(Arc::new(Mutex::new(Default::default())));
let accessor = {
let r = Arc::clone(&recorder.0);
move || r.lock().unwrap().clone()
};
(recorder, accessor)
}
}
/// A [`CheckerVisitor`] that records states evaluated by the model checker. Does not record
/// generated states that are still pending property evaluation.
///
/// # Example
///
/// ```
/// # use stateright::*; let model = ();
/// # let expected_states = vec![()];
/// let (recorder, accessor) = StateRecorder::new_with_accessor();
/// model.checker().visitor(recorder).spawn_dfs().join();
/// assert_eq!(accessor(), expected_states);
/// ```
pub struct StateRecorder<M: Model>(Arc<Mutex<Vec<M::State>>>);
impl<M> CheckerVisitor<M> for StateRecorder<M>
where
M: Model,
M::State: Clone,
{
fn visit(&self, _: &M, path: Path<M::State, M::Action>) {
self.0.lock().unwrap().push(path.last_state().clone())
}
}
impl<M> StateRecorder<M>
where
M: Model,
M::State: Clone,
{
/// Instantiates a ([`StateRecorder`], accessor) pair.
pub fn new_with_accessor() -> (Self, impl Fn() -> Vec<M::State>) {
let recorder = Self(Arc::new(Mutex::new(Default::default())));
let accessor = {
let r = Arc::clone(&recorder.0);
move || r.lock().unwrap().clone()
};
(recorder, accessor)
}
}