use std::sync::atomic::{self, AtomicUsize};
use std::sync::Arc;
use crate::strategy::ReferenceStateMachine;
use proptest::test_runner::Config;
pub trait StateMachineTest {
type SystemUnderTest;
type Reference: ReferenceStateMachine;
fn init_test(
ref_state: &<Self::Reference as ReferenceStateMachine>::State,
) -> Self::SystemUnderTest;
fn apply(
state: Self::SystemUnderTest,
ref_state: &<Self::Reference as ReferenceStateMachine>::State,
transition: <Self::Reference as ReferenceStateMachine>::Transition,
) -> Self::SystemUnderTest;
fn check_invariants(
state: &Self::SystemUnderTest,
ref_state: &<Self::Reference as ReferenceStateMachine>::State,
) {
let _ = (state, ref_state);
}
fn teardown(
state: Self::SystemUnderTest,
ref_state: <Self::Reference as ReferenceStateMachine>::State,
) {
let _ = state;
let _ = ref_state;
}
fn test_sequential(
config: Config,
mut ref_state: <Self::Reference as ReferenceStateMachine>::State,
transitions: Vec<
<Self::Reference as ReferenceStateMachine>::Transition,
>,
mut seen_counter: Option<Arc<AtomicUsize>>,
) {
#[cfg(feature = "std")]
use proptest::test_runner::INFO_LOG;
let trans_len = transitions.len();
#[cfg(feature = "std")]
if config.verbose >= INFO_LOG {
eprintln!();
eprintln!("Running a test case with {} transitions.", trans_len);
}
#[cfg(not(feature = "std"))]
let _ = (config, trans_len);
let mut concrete_state = Self::init_test(&ref_state);
Self::check_invariants(&concrete_state, &ref_state);
for (ix, transition) in transitions.into_iter().enumerate() {
if let Some(seen_counter) = seen_counter.as_mut() {
seen_counter.fetch_add(1, atomic::Ordering::SeqCst);
}
#[cfg(feature = "std")]
if config.verbose >= INFO_LOG {
eprintln!();
eprintln!(
"Applying transition {}/{}: {:?}",
ix + 1,
trans_len,
transition
);
}
#[cfg(not(feature = "std"))]
let _ = ix;
ref_state = <Self::Reference as ReferenceStateMachine>::apply(
ref_state,
&transition,
);
concrete_state =
Self::apply(concrete_state, &ref_state, transition);
Self::check_invariants(&concrete_state, &ref_state);
}
Self::teardown(concrete_state, ref_state)
}
}
#[macro_export]
macro_rules! prop_state_machine {
(#![proptest_config($config:expr)]
$(
$(#[$meta:meta])*
fn $test_name:ident(sequential $size:expr => $test:ident $(< $( $ty_param:tt ),+ >)?);
)*) => {
$(
::proptest::proptest! {
#![proptest_config($config)]
$(#[$meta])*
fn $test_name(
(initial_state, transitions, seen_counter) in <<$test $(< $( $ty_param ),+ >)? as $crate::StateMachineTest>::Reference as $crate::ReferenceStateMachine>::sequential_strategy($size)
) {
let config = $config.__sugar_to_owned();
<$test $(::< $( $ty_param ),+ >)? as $crate::StateMachineTest>::test_sequential(config, initial_state, transitions, seen_counter)
}
}
)*
};
($(
$(#[$meta:meta])*
fn $test_name:ident(sequential $size:expr => $test:ident $(< $( $ty_param:tt ),+ >)?);
)*) => {
$(
::proptest::proptest! {
$(#[$meta])*
fn $test_name(
(initial_state, transitions, seen_counter) in <<$test $(< $( $ty_param ),+ >)? as $crate::StateMachineTest>::Reference as $crate::ReferenceStateMachine>::sequential_strategy($size)
) {
<$test $(::< $( $ty_param ),+ >)? as $crate::StateMachineTest>::test_sequential(
::proptest::test_runner::Config::default(), initial_state, transitions, seen_counter)
}
}
)*
};
}
#[cfg(test)]
mod tests {
mod macro_test {
struct Test;
impl crate::ReferenceStateMachine for Test {
type State = ();
type Transition = ();
fn init_state() -> proptest::strategy::BoxedStrategy<Self::State> {
use proptest::prelude::*;
Just(()).boxed()
}
fn transitions(
_: &Self::State,
) -> proptest::strategy::BoxedStrategy<Self::Transition>
{
use proptest::prelude::*;
Just(()).boxed()
}
fn apply(_: Self::State, _: &Self::Transition) -> Self::State {
()
}
}
impl crate::StateMachineTest for Test {
type SystemUnderTest = ();
type Reference = Self;
fn init_test(
_: &<Self::Reference as crate::ReferenceStateMachine>::State,
) -> Self::SystemUnderTest {
}
fn apply(
_: Self::SystemUnderTest,
_: &<Self::Reference as crate::ReferenceStateMachine>::State,
_: <Self::Reference as crate::ReferenceStateMachine>::Transition,
) -> Self::SystemUnderTest {
}
}
prop_state_machine! {
#[test]
fn no_config_annotation(sequential 1..2 => Test);
}
prop_state_machine! {
#![proptest_config(::proptest::test_runner::Config::default())]
#[test]
fn with_config_annotation(sequential 1..2 => Test);
}
}
}