@@ -527,8 +527,9 @@ explored. But be sure that it will be in real life!
527527In order to overcome this problem, it is possible to skew the distribution of
528528generated [cmd]s by looking at the [state] parameter. If the model of the set
529529is empty, then we just generate a random element. But if there are already some
530- elements in the set, then we can choose between picking one of them or generating a
531- random new one:
530+ elements in the set, then we can choose between picking one of them or
531+ generating a random new one. Now that we are aware of the problem, we also
532+ update the generators for [Mem] and [Add] which suffer from the same weakness.
532533
533534{[
534535 let arb_cmd state =
@@ -540,8 +541,8 @@ random new one:
540541 QCheck.make ~print:show_cmd
541542 (QCheck.Gen.oneof
542543 [Gen.return Cardinal;
543- Gen.map (fun i -> Mem i) Gen.int ;
544- Gen.map (fun i -> Add i) Gen.int ;
544+ Gen.map (fun i -> Mem i) gen ;
545+ Gen.map (fun i -> Add i) gen ;
545546 Gen.map (fun i -> Remove i) gen;
546547 ])
547548]}
@@ -550,33 +551,31 @@ This will be enough to trigger a failure in the test which can help us correct
550551our implementation.
551552
552553{[
553- random seed: 284906494
554- random seed: 514138659
554+ random seed: 77853703
555555generated error fail pass / total time test name
556- [✗] 2 0 1 1 / 100 0.0s STM sequential tests
556+ [✗] 1 0 1 0 / 100 0.0s STM sequential tests
557557
558558--- Failure --------------------------------------------------------------------
559559
560- Test STM sequential tests failed (10 shrink steps):
560+ Test STM sequential tests failed (15 shrink steps):
561561
562- [(Add -2964307208881402510 ); (Remove -2964307208881402510 ); Cardinal; (Mem -371385102013799484 )]
562+ [(Add -4159291639600813199 ); (Remove -4159291639600813199 ); Cardinal; (Remove 1369714189526732393 )]
563563
564564+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
565565
566566Messages for test STM sequential tests:
567567
568568 Results incompatible with model
569569
570- (Add -2964307208881402510 ) : ()
571- (Remove -2964307208881402510 ) : Some (-2964307208881402510 )
570+ (Add -4159291639600813199 ) : ()
571+ (Remove -4159291639600813199 ) : Some (-4159291639600813199 )
572572 Cardinal : 1
573573================================================================================
574574failure (1 tests failed, 0 tests errored, ran 1 tests)
575575]}
576576
577577We see in the output that there is indeed a [Remove] of a previously added
578- element. So this execution path is
579- now explored. As there is only one [Add], one [Remove] of the added element and
580- then [Cardinal] returns [1], we can easily conclude there is something wrong in
581- the implementation of the removal of an element when the element is indeed in
582- the set.
578+ element. So this execution path is now explored. As there is only one [Add],
579+ one [Remove] of the added element and then [Cardinal] returns [1], we can
580+ easily conclude there is something wrong in the implementation of the removal
581+ of an element when the element is indeed in the set.
0 commit comments