diff --git a/proptest-state-machine/src/iterative_runner.rs b/proptest-state-machine/src/iterative_runner.rs new file mode 100644 index 00000000..72d8d3b8 --- /dev/null +++ b/proptest-state-machine/src/iterative_runner.rs @@ -0,0 +1,861 @@ +use std::{cell::RefCell, marker::PhantomData}; + +use proptest::{ + bits::{BitSetLike, VarBitSet}, + collection::SizeRange, + num::sample_uniform_incl, + prelude::Just, + std_facade::fmt::Debug, + strategy::{BoxedStrategy, Strategy, ValueTree}, + test_runner::{Config, Reason, TestError, TestRunner}, +}; + +pub fn test_sequential< + T, + MS, + SS, + M: IterativeModelStateMachine, + S: IterativeSutStateMachine, +>( + config: Config, + mut mod_state: MS, + mut sut_state: SS, + transitions: Vec, +) where + T: Clone + Debug, +{ + let trans_len = transitions.len(); + #[cfg(feature = "std")] + if config.verbose >= super::INFO_LOG { + eprintln!(); + eprintln!("Running a test case with {} transitions.", trans_len); + } + #[cfg(not(feature = "std"))] + let _ = (config, trans_len); + + // Check the invariants on the initial state + S::check_invariants(&sut_state, &mod_state); + + for (ix, transition) in transitions.into_iter().enumerate() { + #[cfg(feature = "std")] + if config.verbose >= super::INFO_LOG { + eprintln!(); + eprintln!( + "Applying transition {}/{}: {:?}", + ix + 1, + trans_len, + transition + ); + } + #[cfg(not(feature = "std"))] + let _ = ix; + assert_eq!( + true, + M::preconditions(&mod_state, &sut_state, &transition), + "precondition failed on transition: {:?}", + transition + ); + // Apply the transition on the states + mod_state = M::apply(mod_state, &transition); + sut_state = S::apply(sut_state, &mod_state, transition); + + // Check the invariants after the transition is applied + S::check_invariants(&sut_state, &mod_state); + } + + S::teardown(sut_state, mod_state) +} + +pub trait IterativeModelStateMachine { + /// Model state used to drive the generation of the transitions + type ModelState: Clone + Debug; + /// Transition generated by this model + type Transition: Clone + Debug; + /// Concrete SUT state, which could be consulted to further sharpern + /// the state transition generation + type SutState; + + /// Initial state of the model + fn init_state() -> BoxedStrategy; + + /// Generate transition based on the state of the model. System under + /// test can be consulted here as well to reduce number of generated + /// transitions + fn transition( + mod_state: &Self::ModelState, + sut_state: &Self::SutState, + ) -> BoxedStrategy; + + /// Apply a transition to the model + fn apply(mod_state: Self::ModelState, transition: &Self::Transition) -> Self::ModelState; + + /// Pre-conditions may be specified to control which transitions are valid + /// from the current state. If not overridden, this allows any transition. + /// The pre-conditions are checked in the generated transitions and during + /// shrinking. System under test can be consulted in both phases to discard + /// transitions. + fn preconditions( + mod_state: &Self::ModelState, + sut_state: &Self::SutState, + transition: &Self::Transition, + ) -> bool { + // This is to avoid `unused_variables` warning + let _ = (mod_state, sut_state, transition); + true + } +} + +/// SUT state machine that relies on a machine model +pub trait IterativeSutStateMachine { + /// The concrete state, that is the system under test (SUT). + type SutState; + /// Transition generated by the model + type Transition: Clone + Debug; + /// Abstract machine model + type ModelState: Clone + Debug; + + /// Initialize the state of SUT. + /// + /// If the reference state machine is generated from a non-constant + /// strategy, ensure to use it to initialize the SUT to a corresponding + /// state. + fn init_test(ref_state: &Self::ModelState) -> Self::SutState; + + /// Apply a transition in the SUT state and check post-conditions. + /// The post-conditions are properties of your state machine that you want + /// to assert. + /// + /// Note that the `mod_state` is the state *after* this `transition` is + /// applied. You can use it to compare it with your SUT after you apply + /// the transition. + fn apply( + sut_state: Self::SutState, + mod_state: &Self::ModelState, + transition: Self::Transition, + ) -> Self::SutState; + + /// Check some invariant on the SUT state after every transition. + fn check_invariants(sut_state: &Self::SutState, mod_state: &Self::ModelState) { + // This is to avoid `unused_variables` warning + let _ = (sut_state, mod_state); + } + + /// Override this function to add some teardown logic on the SUT state + /// at the end of each test case. The default implementation simply drops + /// the state. + fn teardown(sut_state: Self::SutState, mod_state: Self::ModelState) { + // This is to avoid `unused_variables` warning + let (_, _) = (sut_state, mod_state); + } +} + +pub struct Iterative { + size: SizeRange, + init_state: fn() -> BoxedStrategy, + transition: fn(model_state: &ModelState, sut_state: &SutState) -> BoxedStrategy, + preconditions: + fn(model_state: &ModelState, sut_state: &SutState, transition: &Transition) -> bool, + next: fn(model_state: ModelState, transition: &Transition) -> ModelState, + + impl_state: fn(model_state: &ModelState) -> SutState, + next_impl: + fn(sut_state: SutState, model_state: &ModelState, transition: Transition) -> SutState, + check_invariants: fn(sut_state: &SutState, model_state: &ModelState), + teardown: fn(sut_state: SutState, model_state: ModelState), +} + +impl Iterative { + pub fn new( + size: impl Into, + ) -> Iterative + where + M: IterativeModelStateMachine, + S: IterativeSutStateMachine, + { + Iterative { + size: size.into(), + init_state: M::init_state, + preconditions: M::preconditions, + transition: M::transition, + next: M::apply, + impl_state: S::init_test, + next_impl: S::apply, + check_invariants: S::check_invariants, + teardown: S::teardown, + } + } +} + +pub struct IterativeValueTree { + initial_state: Box>, + last_valid_initial_state: ModelState, + transitions: Vec>>, + acceptable_transitions: Vec<(TransitionState, Transition)>, + included_transitions: VarBitSet, + shrinkable_transitions: VarBitSet, + min_size: usize, + max_size: usize, + model_state: RefCell>, + sut_state: RefCell>, + shrink: Shrink, + is_initial_state_shrinkable: bool, + is_delete_after_shrink_possible: bool, + why: Option, +} + +impl + IterativeValueTree +{ + fn new(s: &Iterative, runner: &mut TestRunner) -> Self { + let (min_size, end) = s.size.start_end_incl(); + // Sample the maximum number of the transitions from the size range + + let max_size = sample_uniform_incl(runner, min_size, end); + let shrink = Shrink::DeleteTransition(max_size - 1); + + let included_transitions = VarBitSet::saturated(max_size); + let shrinkable_transitions = VarBitSet::saturated(max_size); + + let transitions = Vec::with_capacity(max_size); + let acceptable_transitions = Vec::with_capacity(max_size); + + let initial_state = (s.init_state)().new_tree(runner).unwrap(); + + let model_state = initial_state.current(); + + IterativeValueTree { + initial_state, + last_valid_initial_state: model_state.clone(), + is_initial_state_shrinkable: false, + is_delete_after_shrink_possible: true, + transitions, + acceptable_transitions, + shrinkable_transitions, + included_transitions, + model_state: RefCell::new(None), + sut_state: RefCell::new(None), + min_size: 1, + max_size, + shrink, + why: None, + } + } + + pub fn try_simplify( + &mut self, + s: &Iterative, + runner: &mut TestRunner, + ) -> bool { + while let Shrink::DeleteTransition(ix) = self.shrink { + let current_shrink = self.shrink; + let included_count = self.included_transitions.count(); + + if included_count <= self.min_size { + // Can't delete any more transitions, move on to shrinking them + self.is_delete_after_shrink_possible = false; + debug!("can't delete any more transitions: {:?}", included_count); + self.shrink = Shrink::Transition(0); + break; + } + + self.included_transitions.clear(ix); + if !self.check_acceptable(s, runner, None, current_shrink) { + self.included_transitions.set(ix) + } else { + self.shrinkable_transitions.clear(ix); + } + + self.shrink = match self.next_delete_transition(ix) { + None => { + if self.shrinkable_transitions.count() == 0 { + // This is delete after shrink, we can't do anything + // more + self.is_delete_after_shrink_possible = false; + return false; + } else { + // Reached the beginning of the list, move on to shrinking + // individual transitions + Shrink::Transition(0) + } + } + // Try to delete the previous transition next + Some(shrink) => shrink, + }; + } + + while let Shrink::Transition(ix) = self.shrink { + let current_shrink = self.shrink; + if self.shrinkable_transitions.count() == 0 { + debug!("nothing to shrink"); + + // Even though it's nothing to shrink, it could be, that we + // can still remove some transitions. So try to do the last pass + if !self.is_delete_after_shrink_possible { + return false; + } + let still_included = self.get_included_acceptable_transitions(None); + if still_included.len() > 0 { + let (last_ix, _) = still_included.last().unwrap(); + self.shrink = Shrink::DeleteTransition(*last_ix); + return true; + } else { + return false; + } + } + + if !self.included_transitions.test(ix) { + self.shrink = self.next_shrink_transition(ix); + continue; + } + + match self.acceptable_transitions.get(ix).unwrap() { + (TransitionState::SimplifyRejected, _) => { + // This transition is already simplified and rejected + self.shrink = self.next_shrink_transition(ix); + continue; + } + (TransitionState::Simplified, _) => { + // Shouldn't happen, as we don't do multiple shrink passes + self.shrink = self.next_shrink_transition(ix); + continue; + } + (TransitionState::Accepted, _) => { + if self.transitions[ix].simplify() { + if self.check_acceptable(s, runner, Some(ix), current_shrink) { + self.acceptable_transitions[ix] = + (TransitionState::Accepted, self.transitions[ix].current()); + } else { + let (state, _trans) = self.acceptable_transitions.get_mut(ix).unwrap(); + *state = TransitionState::SimplifyRejected; + self.shrinkable_transitions.clear(ix); + self.shrink = self.next_shrink_transition(ix); + } + } else { + let (state, _trans) = self.acceptable_transitions.get_mut(ix).unwrap(); + *state = TransitionState::Simplified; + self.shrinkable_transitions.clear(ix); + self.shrink = self.next_shrink_transition(ix); + } + } + } + } + panic!("Unexpected shrink state"); + } + + // Return true if the shrinked result is causing a failure in the test (meaning we found a + // shorter) example. Function may discard some of other transitions on the way, if they do + // not pass the precondition + fn check_acceptable( + &mut self, + s: &Iterative, + runner: &mut TestRunner, + ix: Option, + shrink: Shrink, + ) -> bool { + debug!("check shrinking: {:?}", shrink); + trace!( + "self.acceptable_transitions: {:?}", + self.acceptable_transitions + ); + trace!("self.included_transitions: {:?}", self.included_transitions); + trace!("ix: {:?}", ix); + let transitions = self.get_included_acceptable_transitions(ix); + + self.model_state = RefCell::new(Some(self.last_valid_initial_state.clone())); + self.sut_state = RefCell::new(Some((s.impl_state)( + &self.model_state.borrow().as_ref().unwrap(), + ))); + + let mut skipped_transitions = Vec::new(); + let mut remove_the_rest = false; + let mut shrink_result = false; + + trace!( + "check transitions [{:?}]: {:?}", + transitions.len(), + transitions + ); + for (idx, (ix, transition)) in transitions.iter().enumerate() { + // We found a failure earlier then expected, the rest of the + // transitions could be shrinked + if remove_the_rest == true { + self.included_transitions.clear(*ix); + self.shrinkable_transitions.clear(*ix); + continue; + } + if (s.preconditions)( + &self.model_state.borrow().as_ref().unwrap(), + &self.sut_state.borrow().as_ref().unwrap(), + &transition, + ) { + let is_last = idx == transitions.len() - 1; + let result = IterativeRunner::run_test(self, s, &transition, runner, is_last); + match result { + Ok(true) => {} + Ok(false) => panic!("Test has been rejected"), + Err(TestError::Fail(why, _)) => { + // Prepare to return, first we would like to discard all skipped + // transitions, as they can safely be discarded + for idx in &skipped_transitions { + self.included_transitions.clear(*idx); + self.shrinkable_transitions.clear(*idx); + } + shrink_result = true; + remove_the_rest = true; + self.why = Some(why); + } + Err(TestError::Abort(_)) => + // FIXME: When the test can be aborted? + { + panic!( + "Test aborted: {:?} {:?}", + transition, self.acceptable_transitions + ) + } + } + } else { + // If precondition is violated it might be the case, that we are dealing with + // the dependent transitions here. If that's the case - try to skip transition + // and see if we can make progress. If the test fails, we know that we have dropped + // more transitions then previously thought. If test passes, then we should not drop + // this precondition + skipped_transitions.push(*ix); + } + } + debug!("skrink success: {:?}", shrink_result); + return shrink_result; + } + + // When ix is provided, such a transition would be picked from the Strategy, rather + // then from the already stored transitions + fn get_included_acceptable_transitions(&self, ix: Option) -> Vec<(usize, Transition)> { + self.acceptable_transitions + .iter() + .enumerate() + // Filter out deleted transitions + .filter(|&(this_ix, _)| this_ix < self.max_size) + .filter(|&(this_ix, _)| self.included_transitions.test(this_ix)) + // Map the indices to the values + .map(|(this_ix, (_, transition))| match ix { + Some(ix) if this_ix == ix => (this_ix, self.transitions[ix].current()), + _ => (this_ix, transition.clone()), + }) + .collect() + } + + fn next_shrink_transition(&self, current_ix: usize) -> Shrink { + if current_ix == self.max_size { + // Loop back to the start of the line + Shrink::Transition(0) + } else { + Shrink::Transition(current_ix + 1) + } + } + + fn next_delete_transition(&self, current_ix: usize) -> Option { + if current_ix == 0 { + return None; + } else { + let next_ix = current_ix - 1; + if !self.included_transitions.test(next_ix) { + return self.next_delete_transition(next_ix); + } else { + return Some(Shrink::DeleteTransition(next_ix)); + } + } + } + + pub fn can_simplify(&self) -> bool { + debug!( + "can simplify: {:?} acceptable transitions count: {:?}", + self.shrink, + self.get_included_acceptable_transitions(None).len() + ); + + self.is_initial_state_shrinkable || + self.is_delete_after_shrink_possible || + // If there are some transitions whose shrinking has not yet been + // rejected, we can try to shrink them further + !self + .acceptable_transitions + .iter() + .enumerate() + // Filter out deleted transitions + .filter(|&(ix, _)| ix < self.max_size) + .filter(|&(ix, _)| self.included_transitions.test(ix)) + .all(|(_, (state, _transition))| { + matches!(state, TransitionState::SimplifyRejected + | TransitionState::Simplified + ) + }) + } +} + +pub struct IterativeRunner { + phantom_t: PhantomData, + phantom_ms: PhantomData, + phantom_ss: PhantomData, +} + +impl IterativeRunner +where + T: Clone + Debug, + MS: Clone + Debug, +{ + pub fn incremental_runner( + s: &Iterative, + runner: &mut TestRunner, + ) -> Result<(), TestError<(MS, Vec)>> { + let mut test_setup = IterativeValueTree::new(&s, runner); + let result = Self::explore_transition_space(&mut test_setup, s, runner); + + match result { + Ok(true) => Ok(()), // Test passed + Ok(false) => Self::shrink(&mut test_setup, s, runner), + Err(e) => Err(e), + } + } + + fn run_test( + test_setup: &mut IterativeValueTree, + s: &Iterative, + transition: &T, + runner: &mut TestRunner, + is_last_transition: bool, + ) -> Result> { + let strategy = Just(transition.clone()).no_shrink(); + runner.run_one(strategy, |tr| { + let mut model_state = test_setup.model_state.replace(None).unwrap(); + model_state = (s.next)(model_state.clone(), &transition); + + let mut sut_state = test_setup.sut_state.replace(None).unwrap(); + sut_state = (s.next_impl)(sut_state, &model_state, tr); + (s.check_invariants)(&sut_state, &model_state); + + if is_last_transition { + (s.teardown)(sut_state, model_state) + } else { + test_setup.model_state.replace(Some(model_state)); + test_setup.sut_state.replace(Some(sut_state)); + } + Ok(()) + }) + } + + fn explore_transition_space( + test_setup: &mut IterativeValueTree, + s: &Iterative, + runner: &mut TestRunner, + ) -> Result)>> { + debug!("explore transition space"); + + let model_state = test_setup.initial_state.current(); + test_setup + .sut_state + .replace(Some((s.impl_state)(&model_state))); + test_setup.model_state.replace(Some(model_state)); + + while test_setup.transitions.len() < test_setup.max_size { + let transition_tree = (s.transition)( + &test_setup.model_state.borrow().as_ref().unwrap(), + &test_setup.sut_state.borrow().as_ref().unwrap(), + ) + .new_tree(runner) + .unwrap(); + let transition = transition_tree.current(); + + trace!("suggested transition: {:?}", &transition); + + // If the pre-conditions are satisfied, use the transition + if (s.preconditions)( + &test_setup.model_state.borrow().as_ref().unwrap(), + &test_setup.sut_state.borrow().as_ref().unwrap(), + &transition, + ) { + trace!("precond transition: {:?}", &transition); + + test_setup.transitions.push(transition_tree); + test_setup + .acceptable_transitions + .push((TransitionState::Accepted, transition.clone())); + + let is_last_transition = !(test_setup.transitions.len() < test_setup.max_size); + let result = Self::run_test(test_setup, s, &transition, runner, is_last_transition); + match result { + Ok(true) => (), // Continue + Ok(false) => panic!("Test has been rejected"), // When can we have this? + Err(TestError::Fail(why, _)) => { + let max_size = test_setup.transitions.len(); + debug!("TEST HAS FAILED: {}", max_size); + test_setup.max_size = max_size; + test_setup.shrink = Shrink::DeleteTransition(max_size - 1); + test_setup.included_transitions = VarBitSet::saturated(max_size); + test_setup.shrinkable_transitions = VarBitSet::saturated(max_size); + test_setup.why = Some(why); + + return Ok(false); // shrinking + } + Err(TestError::Abort(_)) => + // FIXME: When the test can be aborted? + { + panic!( + "Test aborted: {:?} {:?}", + transition, test_setup.acceptable_transitions + ) + } + } + } else { + runner + .reject_local("Pre-conditions were not satisfied") + .map_err(|reason| TestError::Abort(reason))?; + } + } + debug!( + "test passed, transitions:: {:?}", + &test_setup.acceptable_transitions.len() + ); + + Ok(true) + } + + fn shrink( + test: &mut IterativeValueTree, + s: &Iterative, + runner: &mut TestRunner, + ) -> Result<(), TestError<(MS, Vec)>> { + loop { + debug!("enter shrinking phase"); + if test.can_simplify() { + if test.try_simplify(s, runner) { + continue; + } + } else { + debug!("can't simplify"); + break; + } + } + + let reason = test.why.clone().unwrap(); + let initial_state = test.last_valid_initial_state.clone(); + let shrinked_transitions = test + .get_included_acceptable_transitions(None) + .into_iter() + .map(|(_, transition)| transition.clone()) + .collect::>(); + + debug!("initial state: {:?}", initial_state); + debug!( + "shrinked transitions count: {:?}", + shrinked_transitions.len() + ); + debug!("shrinked transition: {:?}", shrinked_transitions); + + Err(TestError::Fail( + reason, + (initial_state, shrinked_transitions), + )) + } +} +/// A shrinking operation +#[derive(Clone, Copy, Debug)] +enum Shrink { + /// Delete a transition at given index + DeleteTransition(usize), + /// Shrink a transition at given index + Transition(usize), +} + +/// The state of a transition in the model +#[derive(Clone, Copy, Debug)] +enum TransitionState { + /// The transition that is equal to the result of `ValueTree::current()` + /// and satisfies the pre-conditions + Accepted, + /// Transition is accepted, but we can't simplify it further + Simplified, + /// The transition has been simplified, but rejected by pre-conditions + SimplifyRejected, +} + +#[cfg(test)] +mod test { + use traffic_light::*; + use super::*; + + #[test] + fn test_iterative_runner() -> Result< + (), + TestError<( + TrafficLightModelState, + Vec, + )>, + > { + let config = Config { + max_shrink_iters: 5, + ..Config::default() + }; + let mut runner = TestRunner::new(config); + let iterative = Iterative::new::(1..200); + + IterativeRunner::incremental_runner(&iterative, &mut runner) + } + + mod traffic_light { + use proptest::{prelude::*, strategy::Union}; + + use crate::proptest::custom_runner::{ + IterativeModelStateMachine, IterativeSutStateMachine, + }; + + pub struct TrafficLightTest; + + #[derive(Clone, Debug)] + pub struct TrafficLightModel; + pub struct TrafficLightSutState { + cur_state: TrafficLightState, + prev_state: TrafficLightState, + failure_count: u32, + } + + // Lets assume that our implementation has a bug where after SystemRestart the + // implementation Will start with the last light that has been set before the + // restart + + #[derive(Clone, Debug)] + pub struct TrafficLightModelState(TrafficLightState); + + #[derive(Clone, Debug, PartialEq)] + pub enum TrafficLightState { + None, + Red, + Green, + Amber, + FlashingRed, + } + + #[derive(Clone, Debug, PartialEq)] + pub enum TrafficLightTransition { + SystemPowerOn, + TimerExpires, + SystemError, + SystemRestart, + } + + impl IterativeModelStateMachine for TrafficLightModel { + type ModelState = TrafficLightModelState; + type Transition = TrafficLightTransition; + type SutState = TrafficLightSutState; + + fn init_state() -> BoxedStrategy { + Just(TrafficLightModelState(TrafficLightState::None)).boxed() + } + + fn transition( + model_state: &Self::ModelState, + _sut_state: &Self::SutState, + ) -> BoxedStrategy { + // FIXME: Introduce some case where we need sut_state to generate a transition + let TrafficLightModelState(inner_state) = model_state; + match inner_state { + TrafficLightState::None => Just(TrafficLightTransition::SystemPowerOn).boxed(), + TrafficLightState::FlashingRed => { + Just(TrafficLightTransition::SystemRestart).boxed() + } + _ => Union::new_weighted(vec![ + (10, Just(TrafficLightTransition::TimerExpires)), + (1, Just(TrafficLightTransition::SystemError)), + ]) + .boxed(), + } + } + + fn apply( + model_state: Self::ModelState, + transition: &Self::Transition, + ) -> Self::ModelState { + let new_state = match transition { + TrafficLightTransition::SystemPowerOn => TrafficLightState::Red, + TrafficLightTransition::TimerExpires => { + let TrafficLightModelState(m_state) = model_state; + match m_state { + TrafficLightState::Red => TrafficLightState::Green, + TrafficLightState::Green => TrafficLightState::Amber, + TrafficLightState::Amber => TrafficLightState::Red, + _ => unreachable!(), + } + } + TrafficLightTransition::SystemError => TrafficLightState::FlashingRed, + TrafficLightTransition::SystemRestart => TrafficLightState::Red, + }; + TrafficLightModelState(new_state) + } + + fn preconditions( + model_state: &Self::ModelState, + _sut_state: &Self::SutState, + transition: &Self::Transition, + ) -> bool { + let TrafficLightModelState(m_state) = model_state; + debug!("checking precondition: {:?} {:?}", &m_state, &transition); + match transition { + TrafficLightTransition::TimerExpires => match *m_state { + TrafficLightState::FlashingRed => false, + TrafficLightState::None => false, + _ => true, + }, + _ => true, + } + } + } + + impl IterativeSutStateMachine for TrafficLightTest { + type SutState = TrafficLightSutState; + type ModelState = TrafficLightModelState; + type Transition = TrafficLightTransition; + + fn init_test(_model_state: &Self::ModelState) -> Self::SutState { + TrafficLightSutState { + cur_state: TrafficLightState::None, + prev_state: TrafficLightState::None, + failure_count: 0, + } + } + + fn apply( + mut sut_state: Self::SutState, + _model_state: &Self::ModelState, + transition: Self::Transition, + ) -> Self::SutState { + let new_state = match transition { + TrafficLightTransition::SystemPowerOn => TrafficLightState::Red, + TrafficLightTransition::TimerExpires => match sut_state.cur_state { + TrafficLightState::Red => TrafficLightState::Green, + TrafficLightState::Green => TrafficLightState::Amber, + TrafficLightState::Amber => TrafficLightState::Red, + _ => unreachable!(), + }, + TrafficLightTransition::SystemError => { + sut_state.failure_count += 1; + sut_state.prev_state = sut_state.cur_state.clone(); + TrafficLightState::FlashingRed + } + TrafficLightTransition::SystemRestart => { + // NOTE: Deliberate error. On system error we do not reset + // sut_state.prev_state.clone() + TrafficLightState::Red + } + }; + sut_state.cur_state = new_state; + sut_state + } + + fn check_invariants(sut_state: &Self::SutState, model_state: &Self::ModelState) { + // This is to avoid `unused_variables` warning + let TrafficLightModelState(inner_state) = model_state; + debug!("sut({:?}) == mod({:?})", inner_state, sut_state.cur_state); + + assert!(sut_state.cur_state == *inner_state); + } + } + } +}