9
9
10
10
//! Strategies used for abstract state machine testing.
11
11
12
+ use std:: sync:: atomic:: { self , AtomicUsize } ;
13
+ use std:: sync:: Arc ;
14
+
12
15
use proptest:: bits:: { BitSetLike , VarBitSet } ;
13
16
use proptest:: collection:: SizeRange ;
14
17
use proptest:: num:: sample_uniform_incl;
@@ -118,14 +121,19 @@ pub trait ReferenceStateMachine {
118
121
/// The shrinking strategy is to iteratively apply `Shrink::InitialState`,
119
122
/// `Shrink::DeleteTransition` and `Shrink::Transition`.
120
123
///
121
- /// 1. We start by trying to delete transitions from the back of the list, until
122
- /// we can do so no further (reached the beginning of the list).
123
- /// We start from the back, because it's less likely to affect the state
124
- /// machine's pre-conditions, if any.
125
- /// 2. Then, we again iteratively attempt to shrink the individual transitions,
124
+ /// 1. We start by trying to delete transitions from the back of the list that
125
+ /// were never seen by the test, if any. Note that because proptest expects
126
+ /// deterministic results in for reproducible issues, unlike the following
127
+ /// steps this step will not be undone on `complicate`. If there were any
128
+ /// unseen transitions, then the next step will start at trying to delete
129
+ /// the transition before the last one seen as we know that the last
130
+ /// transition cannot be deleted as it's the one that has failed.
131
+ /// 2. Then, we keep trying to delete transitions from the back of the list, until
132
+ /// we can do so no further (reached the beginning of the list)..
133
+ /// 3. Then, we again iteratively attempt to shrink the individual transitions,
126
134
/// but this time starting from the front of the list - i.e. from the first
127
135
/// transition to be applied.
128
- /// 3 . Finally, we try to shrink the initial state until it's not possible to
136
+ /// 4 . Finally, we try to shrink the initial state until it's not possible to
129
137
/// shrink it any further.
130
138
///
131
139
/// For `complicate`, we attempt to undo the last shrink operation, if there was
@@ -162,7 +170,7 @@ impl<
162
170
StateStrategy :: Tree ,
163
171
TransitionStrategy :: Tree ,
164
172
> ;
165
- type Value = ( State , Vec < Transition > ) ;
173
+ type Value = ( State , Vec < Transition > , Option < Arc < AtomicUsize > > ) ;
166
174
167
175
fn new_tree ( & self , runner : & mut TestRunner ) -> NewTree < Self > {
168
176
// Generate the initial state value tree
@@ -214,6 +222,7 @@ impl<
214
222
// which is less likely to invalidate pre-conditions
215
223
shrink : Shrink :: DeleteTransition ( max_ix) ,
216
224
last_shrink : None ,
225
+ seen_transitions_counter : Some ( Default :: default ( ) ) ,
217
226
} )
218
227
}
219
228
}
@@ -276,6 +285,13 @@ pub struct SequentialValueTree<
276
285
shrink : Shrink ,
277
286
/// The last applied shrink operation, if any
278
287
last_shrink : Option < Shrink > ,
288
+ /// The number of transitions that were seen by the test runner.
289
+ /// On a test run this is shared with `StateMachineTest::test_sequential`
290
+ /// which increments the inner counter value on every transition. If the
291
+ /// test fails, the counter is used to remove any unseen transitions before
292
+ /// shrinking and this field is set to `None` as it's no longer needed for
293
+ /// shrinking.
294
+ seen_transitions_counter : Option < Arc < AtomicUsize > > ,
279
295
}
280
296
281
297
impl <
@@ -289,6 +305,46 @@ impl<
289
305
/// Try to apply the next `self.shrink`. Returns `true` if a shrink has been
290
306
/// applied.
291
307
fn try_simplify ( & mut self ) -> bool {
308
+ if let Some ( seen_transitions_counter) =
309
+ self . seen_transitions_counter . as_ref ( )
310
+ {
311
+ let seen_count =
312
+ seen_transitions_counter. load ( atomic:: Ordering :: SeqCst ) ;
313
+
314
+ let included_count = self . included_transitions . count ( ) ;
315
+
316
+ if seen_count < included_count {
317
+ // the test runner did not see all the transitions so we can
318
+ // delete the transitions that were not seen because they were
319
+ // not executed
320
+
321
+ let mut kept_count = 0 ;
322
+ for ix in 0 ..self . transitions . len ( ) {
323
+ if self . included_transitions . test ( ix) {
324
+ // transition at ix was part of test
325
+
326
+ if kept_count < seen_count {
327
+ // transition at xi was seen by the test or we are
328
+ // still below minimum size for the test
329
+ kept_count += 1 ;
330
+ } else {
331
+ // transition at ix was never seen
332
+ self . included_transitions . clear ( ix) ;
333
+ self . shrinkable_transitions . clear ( ix) ;
334
+ }
335
+ }
336
+ }
337
+ // Set the next shrink to the transition before the last seen
338
+ // transition (subtract 2 from `kept_count`)
339
+ self . shrink = DeleteTransition (
340
+ kept_count. checked_sub ( 2 ) . unwrap_or_default ( ) ,
341
+ ) ;
342
+ }
343
+
344
+ // Remove the seen transitions counter for shrinking runs
345
+ self . seen_transitions_counter = None ;
346
+ }
347
+
292
348
if let DeleteTransition ( ix) = self . shrink {
293
349
// Delete the index from the included transitions
294
350
self . included_transitions . clear ( ix) ;
@@ -442,7 +498,7 @@ impl<
442
498
/// yet been rejected.
443
499
fn can_simplify ( & self ) -> bool {
444
500
self . is_initial_state_shrinkable ||
445
- // If there are some transitions whose shrinking has not yet been
501
+ // If there are some transitions whose shrinking has not yet been
446
502
// rejected, we can try to shrink them further
447
503
!self
448
504
. acceptable_transitions
@@ -483,39 +539,54 @@ impl<
483
539
TransitionValueTree ,
484
540
>
485
541
{
486
- type Value = ( State , Vec < Transition > ) ;
542
+ type Value = ( State , Vec < Transition > , Option < Arc < AtomicUsize > > ) ;
487
543
488
544
fn current ( & self ) -> Self :: Value {
545
+ if let Some ( seen_transitions_counter) = & self . seen_transitions_counter {
546
+ if seen_transitions_counter. load ( atomic:: Ordering :: SeqCst ) > 0 {
547
+ panic ! ( "Unexpected non-zero `seen_transitions_counter`" ) ;
548
+ }
549
+ }
550
+
489
551
(
490
552
self . last_valid_initial_state . clone ( ) ,
491
553
// The current included acceptable transitions
492
554
self . get_included_acceptable_transitions ( None ) ,
555
+ self . seen_transitions_counter . clone ( ) ,
493
556
)
494
557
}
495
558
496
559
fn simplify ( & mut self ) -> bool {
497
- if self . can_simplify ( ) {
560
+ let was_simplified = if self . can_simplify ( ) {
498
561
self . try_simplify ( )
562
+ } else if let Some ( Transition ( ix) ) = self . last_shrink {
563
+ self . try_to_find_acceptable_transition ( ix)
499
564
} else {
500
- if let Some ( Transition ( ix) ) = self . last_shrink {
501
- return self . try_to_find_acceptable_transition ( ix) ;
502
- }
503
565
false
504
- }
566
+ } ;
567
+
568
+ // reset seen transactions counter for next run
569
+ self . seen_transitions_counter = Default :: default ( ) ;
570
+
571
+ was_simplified
505
572
}
506
573
507
574
fn complicate ( & mut self ) -> bool {
508
- match self . last_shrink {
575
+ // reset seen transactions counter for next run
576
+ self . seen_transitions_counter = Default :: default ( ) ;
577
+
578
+ match & self . last_shrink {
509
579
None => false ,
510
580
Some ( DeleteTransition ( ix) ) => {
511
581
// Undo the last item we deleted. Can't complicate any further,
512
582
// so unset prev_shrink.
513
- self . included_transitions . set ( ix) ;
514
- self . shrinkable_transitions . set ( ix) ;
583
+ self . included_transitions . set ( * ix) ;
584
+ self . shrinkable_transitions . set ( * ix) ;
515
585
self . last_shrink = None ;
516
586
true
517
587
}
518
588
Some ( Transition ( ix) ) => {
589
+ let ix = * ix;
519
590
if self . transitions [ ix] . complicate ( ) {
520
591
if self . check_acceptable ( Some ( ix) ) {
521
592
self . acceptable_transitions [ ix] =
@@ -574,6 +645,11 @@ mod test {
574
645
#[ test]
575
646
fn number_of_sequential_value_tree_simplifications ( ) {
576
647
let mut value_tree = deterministic_sequential_value_tree ( ) ;
648
+ value_tree
649
+ . seen_transitions_counter
650
+ . as_mut ( )
651
+ . unwrap ( )
652
+ . store ( TRANSITIONS , atomic:: Ordering :: SeqCst ) ;
577
653
578
654
let mut i = 0 ;
579
655
loop {
@@ -614,7 +690,7 @@ mod test {
614
690
let mut value_tree = deterministic_sequential_value_tree ( ) ;
615
691
616
692
let check_preconditions = |value_tree : & TestValueTree | {
617
- let ( mut state, transitions) = value_tree. current ( ) ;
693
+ let ( mut state, transitions, _seen_counter ) = value_tree. current ( ) ;
618
694
let len = transitions. len ( ) ;
619
695
println ! ( "Transitions {}" , len) ;
620
696
for ( ix, transition) in transitions. into_iter ( ) . enumerate ( ) {
@@ -660,6 +736,77 @@ mod test {
660
736
}
661
737
}
662
738
739
+ proptest ! {
740
+ /// Test the initial simplifications of the `SequentialValueTree` produced
741
+ /// by `deterministic_sequential_value_tree`.
742
+ ///
743
+ /// We want to make sure that we initially remove the transitions that
744
+ /// where not seen.
745
+ #[ test]
746
+ fn test_value_tree_initial_simplification(
747
+ len in 10usize ..100 ,
748
+ ) {
749
+ test_value_tree_initial_simplification_aux( len)
750
+ }
751
+ }
752
+
753
+ fn test_value_tree_initial_simplification_aux ( len : usize ) {
754
+ let sequential =
755
+ <HeapStateMachine as ReferenceStateMachine >:: sequential_strategy (
756
+ ..len,
757
+ ) ;
758
+
759
+ let mut runner = TestRunner :: deterministic ( ) ;
760
+ let mut value_tree = sequential. new_tree ( & mut runner) . unwrap ( ) ;
761
+
762
+ let ( _, transitions, mut seen_counter) = value_tree. current ( ) ;
763
+
764
+ let num_seen = transitions. len ( ) / 2 ;
765
+ let seen_counter = seen_counter. as_mut ( ) . unwrap ( ) ;
766
+ seen_counter. store ( num_seen, atomic:: Ordering :: SeqCst ) ;
767
+
768
+ let mut seen_before_complication =
769
+ transitions. into_iter ( ) . take ( num_seen) . collect :: < Vec < _ > > ( ) ;
770
+
771
+ assert ! ( value_tree. simplify( ) ) ;
772
+
773
+ let ( _, transitions, _seen_counter) = value_tree. current ( ) ;
774
+
775
+ let seen_after_first_complication =
776
+ transitions. into_iter ( ) . collect :: < Vec < _ > > ( ) ;
777
+
778
+ // After the unseen transitions are removed, the shrink to delete the
779
+ // transition before the last seen one is applied
780
+ let last = seen_before_complication. pop ( ) . unwrap ( ) ;
781
+ seen_before_complication. pop ( ) ;
782
+ seen_before_complication. push ( last) ;
783
+
784
+ assert_eq ! (
785
+ seen_before_complication, seen_after_first_complication,
786
+ "only seen transitions should be present after first simplification"
787
+ ) ;
788
+ }
789
+
790
+ #[ test]
791
+ fn test_call_to_current_with_non_zero_seen_counter ( ) {
792
+ let result = std:: panic:: catch_unwind ( || {
793
+ let value_tree = deterministic_sequential_value_tree ( ) ;
794
+
795
+ let ( _, _transitions1, mut seen_counter) = value_tree. current ( ) ;
796
+ {
797
+ let seen_counter = seen_counter. as_mut ( ) . unwrap ( ) ;
798
+ seen_counter. store ( 1 , atomic:: Ordering :: SeqCst ) ;
799
+ }
800
+ drop ( seen_counter) ;
801
+
802
+ let _transitions2 = value_tree. current ( ) ;
803
+ } )
804
+ . expect_err ( "should panic" ) ;
805
+
806
+ let s = "Unexpected non-zero `seen_transitions_counter`" ;
807
+ assert_eq ! ( result. downcast_ref:: <& str >( ) , Some ( & s) ) ;
808
+ }
809
+
663
810
/// The following is a definition of an reference state machine used for the
664
811
/// tests.
665
812
mod heap_state_machine {
@@ -682,7 +829,7 @@ mod test {
682
829
683
830
pub type TestState = Vec < i32 > ;
684
831
685
- #[ derive( Clone , Debug ) ]
832
+ #[ derive( Clone , Debug , PartialEq ) ]
686
833
pub enum TestTransition {
687
834
PopNonEmpty ,
688
835
PopEmpty ,
@@ -839,22 +986,23 @@ mod test {
839
986
Config :: default ( ) , TestRng :: from_seed( Default :: default ( ) , & seed) ) ;
840
987
let result = runner. run(
841
988
& FailIfLessThan :: sequential_strategy( 10 ..50_usize ) ,
842
- |( ref_state, transitions) | {
989
+ |( ref_state, transitions, seen_counter ) | {
843
990
Ok ( FailIfLessThanTest :: test_sequential(
844
991
Default :: default ( ) ,
845
992
ref_state,
846
993
transitions,
994
+ seen_counter,
847
995
) )
848
996
} ,
849
997
) ;
850
998
if let Err ( TestError :: Fail (
851
999
_,
852
- ( FailIfLessThan ( limit) , transitions) ,
1000
+ ( FailIfLessThan ( limit) , transitions, _seen_counter ) ,
853
1001
) ) = result
854
1002
{
855
1003
assert_eq!( transitions. len( ) , 1 , "The minimal failing case should be " ) ;
856
1004
assert_eq!( limit, MIN_TRANSITION + 1 ) ;
857
- assert!( transitions[ 0 ] < limit) ;
1005
+ assert!( transitions. into_iter ( ) . next ( ) . unwrap ( ) < limit) ;
858
1006
} else {
859
1007
prop_assume!( false ,
860
1008
"If the state machine doesn't fail as intended, we need a case that fails." ) ;
0 commit comments