Skip to content

Commit

Permalink
Merge branch 'hs/simplify-unseen' (proptest-rs#388)
Browse files Browse the repository at this point in the history
* hs/simplify-unseen:
  changelog: add proptest-rs#388
  panic on misuse
  add fallback to avoid panic
  delete unseen transitions in state machine test
  • Loading branch information
tzemanovic committed Mar 21, 2024
2 parents 2efefa8 + c7d383f commit 418c912
Show file tree
Hide file tree
Showing 3 changed files with 192 additions and 27 deletions.
5 changes: 5 additions & 0 deletions proptest-state-machine/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
## Unreleased

### New Features

- Remove unseen transitions on a first step of shrinking.
([\#388](https://github.com/proptest-rs/proptest/pull/388))

## 0.2.0

### Other Notes
Expand Down
192 changes: 170 additions & 22 deletions proptest-state-machine/src/strategy.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,9 @@

//! Strategies used for abstract state machine testing.
use std::sync::atomic::{self, AtomicUsize};
use std::sync::Arc;

use proptest::bits::{BitSetLike, VarBitSet};
use proptest::collection::SizeRange;
use proptest::num::sample_uniform_incl;
Expand Down Expand Up @@ -118,14 +121,19 @@ pub trait ReferenceStateMachine {
/// The shrinking strategy is to iteratively apply `Shrink::InitialState`,
/// `Shrink::DeleteTransition` and `Shrink::Transition`.
///
/// 1. We start by trying to delete transitions from the back of the list, until
/// we can do so no further (reached the beginning of the list).
/// We start from the back, because it's less likely to affect the state
/// machine's pre-conditions, if any.
/// 2. Then, we again iteratively attempt to shrink the individual transitions,
/// 1. We start by trying to delete transitions from the back of the list that
/// were never seen by the test, if any. Note that because proptest expects
/// deterministic results in for reproducible issues, unlike the following
/// steps this step will not be undone on `complicate`. If there were any
/// unseen transitions, then the next step will start at trying to delete
/// the transition before the last one seen as we know that the last
/// transition cannot be deleted as it's the one that has failed.
/// 2. Then, we keep trying to delete transitions from the back of the list, until
/// we can do so no further (reached the beginning of the list)..
/// 3. Then, we again iteratively attempt to shrink the individual transitions,
/// but this time starting from the front of the list - i.e. from the first
/// transition to be applied.
/// 3. Finally, we try to shrink the initial state until it's not possible to
/// 4. Finally, we try to shrink the initial state until it's not possible to
/// shrink it any further.
///
/// For `complicate`, we attempt to undo the last shrink operation, if there was
Expand Down Expand Up @@ -162,7 +170,7 @@ impl<
StateStrategy::Tree,
TransitionStrategy::Tree,
>;
type Value = (State, Vec<Transition>);
type Value = (State, Vec<Transition>, Option<Arc<AtomicUsize>>);

fn new_tree(&self, runner: &mut TestRunner) -> NewTree<Self> {
// Generate the initial state value tree
Expand Down Expand Up @@ -214,6 +222,7 @@ impl<
// which is less likely to invalidate pre-conditions
shrink: Shrink::DeleteTransition(max_ix),
last_shrink: None,
seen_transitions_counter: Some(Default::default()),
})
}
}
Expand Down Expand Up @@ -276,6 +285,13 @@ pub struct SequentialValueTree<
shrink: Shrink,
/// The last applied shrink operation, if any
last_shrink: Option<Shrink>,
/// The number of transitions that were seen by the test runner.
/// On a test run this is shared with `StateMachineTest::test_sequential`
/// which increments the inner counter value on every transition. If the
/// test fails, the counter is used to remove any unseen transitions before
/// shrinking and this field is set to `None` as it's no longer needed for
/// shrinking.
seen_transitions_counter: Option<Arc<AtomicUsize>>,
}

impl<
Expand All @@ -289,6 +305,46 @@ impl<
/// Try to apply the next `self.shrink`. Returns `true` if a shrink has been
/// applied.
fn try_simplify(&mut self) -> bool {
if let Some(seen_transitions_counter) =
self.seen_transitions_counter.as_ref()
{
let seen_count =
seen_transitions_counter.load(atomic::Ordering::SeqCst);

let included_count = self.included_transitions.count();

if seen_count < included_count {
// the test runner did not see all the transitions so we can
// delete the transitions that were not seen because they were
// not executed

let mut kept_count = 0;
for ix in 0..self.transitions.len() {
if self.included_transitions.test(ix) {
// transition at ix was part of test

if kept_count < seen_count {
// transition at xi was seen by the test or we are
// still below minimum size for the test
kept_count += 1;
} else {
// transition at ix was never seen
self.included_transitions.clear(ix);
self.shrinkable_transitions.clear(ix);
}
}
}
// Set the next shrink to the transition before the last seen
// transition (subtract 2 from `kept_count`)
self.shrink = DeleteTransition(
kept_count.checked_sub(2).unwrap_or_default(),
);
}

// Remove the seen transitions counter for shrinking runs
self.seen_transitions_counter = None;
}

if let DeleteTransition(ix) = self.shrink {
// Delete the index from the included transitions
self.included_transitions.clear(ix);
Expand Down Expand Up @@ -442,7 +498,7 @@ impl<
/// yet been rejected.
fn can_simplify(&self) -> bool {
self.is_initial_state_shrinkable ||
// If there are some transitions whose shrinking has not yet been
// If there are some transitions whose shrinking has not yet been
// rejected, we can try to shrink them further
!self
.acceptable_transitions
Expand Down Expand Up @@ -483,39 +539,54 @@ impl<
TransitionValueTree,
>
{
type Value = (State, Vec<Transition>);
type Value = (State, Vec<Transition>, Option<Arc<AtomicUsize>>);

fn current(&self) -> Self::Value {
if let Some(seen_transitions_counter) = &self.seen_transitions_counter {
if seen_transitions_counter.load(atomic::Ordering::SeqCst) > 0 {
panic!("Unexpected non-zero `seen_transitions_counter`");
}
}

(
self.last_valid_initial_state.clone(),
// The current included acceptable transitions
self.get_included_acceptable_transitions(None),
self.seen_transitions_counter.clone(),
)
}

fn simplify(&mut self) -> bool {
if self.can_simplify() {
let was_simplified = if self.can_simplify() {
self.try_simplify()
} else if let Some(Transition(ix)) = self.last_shrink {
self.try_to_find_acceptable_transition(ix)
} else {
if let Some(Transition(ix)) = self.last_shrink {
return self.try_to_find_acceptable_transition(ix);
}
false
}
};

// reset seen transactions counter for next run
self.seen_transitions_counter = Default::default();

was_simplified
}

fn complicate(&mut self) -> bool {
match self.last_shrink {
// reset seen transactions counter for next run
self.seen_transitions_counter = Default::default();

match &self.last_shrink {
None => false,
Some(DeleteTransition(ix)) => {
// Undo the last item we deleted. Can't complicate any further,
// so unset prev_shrink.
self.included_transitions.set(ix);
self.shrinkable_transitions.set(ix);
self.included_transitions.set(*ix);
self.shrinkable_transitions.set(*ix);
self.last_shrink = None;
true
}
Some(Transition(ix)) => {
let ix = *ix;
if self.transitions[ix].complicate() {
if self.check_acceptable(Some(ix)) {
self.acceptable_transitions[ix] =
Expand Down Expand Up @@ -574,6 +645,11 @@ mod test {
#[test]
fn number_of_sequential_value_tree_simplifications() {
let mut value_tree = deterministic_sequential_value_tree();
value_tree
.seen_transitions_counter
.as_mut()
.unwrap()
.store(TRANSITIONS, atomic::Ordering::SeqCst);

let mut i = 0;
loop {
Expand Down Expand Up @@ -614,7 +690,7 @@ mod test {
let mut value_tree = deterministic_sequential_value_tree();

let check_preconditions = |value_tree: &TestValueTree| {
let (mut state, transitions) = value_tree.current();
let (mut state, transitions, _seen_counter) = value_tree.current();
let len = transitions.len();
println!("Transitions {}", len);
for (ix, transition) in transitions.into_iter().enumerate() {
Expand Down Expand Up @@ -660,6 +736,77 @@ mod test {
}
}

proptest! {
/// Test the initial simplifications of the `SequentialValueTree` produced
/// by `deterministic_sequential_value_tree`.
///
/// We want to make sure that we initially remove the transitions that
/// where not seen.
#[test]
fn test_value_tree_initial_simplification(
len in 10usize..100,
) {
test_value_tree_initial_simplification_aux(len)
}
}

fn test_value_tree_initial_simplification_aux(len: usize) {
let sequential =
<HeapStateMachine as ReferenceStateMachine>::sequential_strategy(
..len,
);

let mut runner = TestRunner::deterministic();
let mut value_tree = sequential.new_tree(&mut runner).unwrap();

let (_, transitions, mut seen_counter) = value_tree.current();

let num_seen = transitions.len() / 2;
let seen_counter = seen_counter.as_mut().unwrap();
seen_counter.store(num_seen, atomic::Ordering::SeqCst);

let mut seen_before_complication =
transitions.into_iter().take(num_seen).collect::<Vec<_>>();

assert!(value_tree.simplify());

let (_, transitions, _seen_counter) = value_tree.current();

let seen_after_first_complication =
transitions.into_iter().collect::<Vec<_>>();

// After the unseen transitions are removed, the shrink to delete the
// transition before the last seen one is applied
let last = seen_before_complication.pop().unwrap();
seen_before_complication.pop();
seen_before_complication.push(last);

assert_eq!(
seen_before_complication, seen_after_first_complication,
"only seen transitions should be present after first simplification"
);
}

#[test]
fn test_call_to_current_with_non_zero_seen_counter() {
let result = std::panic::catch_unwind(|| {
let value_tree = deterministic_sequential_value_tree();

let (_, _transitions1, mut seen_counter) = value_tree.current();
{
let seen_counter = seen_counter.as_mut().unwrap();
seen_counter.store(1, atomic::Ordering::SeqCst);
}
drop(seen_counter);

let _transitions2 = value_tree.current();
})
.expect_err("should panic");

let s = "Unexpected non-zero `seen_transitions_counter`";
assert_eq!(result.downcast_ref::<&str>(), Some(&s));
}

/// The following is a definition of an reference state machine used for the
/// tests.
mod heap_state_machine {
Expand All @@ -682,7 +829,7 @@ mod test {

pub type TestState = Vec<i32>;

#[derive(Clone, Debug)]
#[derive(Clone, Debug, PartialEq)]
pub enum TestTransition {
PopNonEmpty,
PopEmpty,
Expand Down Expand Up @@ -839,22 +986,23 @@ mod test {
Config::default(), TestRng::from_seed(Default::default(), &seed));
let result = runner.run(
&FailIfLessThan::sequential_strategy(10..50_usize),
|(ref_state, transitions)| {
|(ref_state, transitions, seen_counter)| {
Ok(FailIfLessThanTest::test_sequential(
Default::default(),
ref_state,
transitions,
seen_counter,
))
},
);
if let Err(TestError::Fail(
_,
(FailIfLessThan(limit), transitions),
(FailIfLessThan(limit), transitions, _seen_counter),
)) = result
{
assert_eq!(transitions.len(), 1, "The minimal failing case should be ");
assert_eq!(limit, MIN_TRANSITION + 1);
assert!(transitions[0] < limit);
assert!(transitions.into_iter().next().unwrap() < limit);
} else {
prop_assume!(false,
"If the state machine doesn't fail as intended, we need a case that fails.");
Expand Down
22 changes: 17 additions & 5 deletions proptest-state-machine/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@

//! Test declaration helpers and runners for abstract state machine testing.
use std::sync::atomic::{self, AtomicUsize};
use std::sync::Arc;

use crate::strategy::ReferenceStateMachine;
use proptest::std_facade::Vec;
use proptest::test_runner::Config;

/// State machine test that relies on a reference state machine model
Expand Down Expand Up @@ -72,6 +74,7 @@ pub trait StateMachineTest {
transitions: Vec<
<Self::Reference as ReferenceStateMachine>::Transition,
>,
mut seen_counter: Option<Arc<AtomicUsize>>,
) {
#[cfg(feature = "std")]
use proptest::test_runner::INFO_LOG;
Expand All @@ -91,6 +94,15 @@ pub trait StateMachineTest {
Self::check_invariants(&concrete_state, &ref_state);

for (ix, transition) in transitions.into_iter().enumerate() {
// The counter is `Some` only before shrinking. When it's `Some` it
// must be incremented before every transition that's being applied
// to inform the strategy that the transition has been applied for
// the first step of its shrinking process which removes any unseen
// transitions.
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!();
Expand Down Expand Up @@ -170,11 +182,11 @@ macro_rules! prop_state_machine {
#![proptest_config($config)]
$(#[$meta])*
fn $test_name(
(initial_state, transitions) in <<$test $(< $( $ty_param ),+ >)? as $crate::StateMachineTest>::Reference as $crate::ReferenceStateMachine>::sequential_strategy($size)
(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)
<$test $(::< $( $ty_param ),+ >)? as $crate::StateMachineTest>::test_sequential(config, initial_state, transitions, seen_counter)
}
}
)*
Expand All @@ -189,10 +201,10 @@ macro_rules! prop_state_machine {
::proptest::proptest! {
$(#[$meta])*
fn $test_name(
(initial_state, transitions) in <<$test $(< $( $ty_param ),+ >)? as $crate::StateMachineTest>::Reference as $crate::ReferenceStateMachine>::sequential_strategy($size)
(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)
::proptest::test_runner::Config::default(), initial_state, transitions, seen_counter)
}
}
)*
Expand Down

0 comments on commit 418c912

Please sign in to comment.