diff --git a/CHANGES.md b/CHANGES.md index d984b4cc..56e57049 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -8,6 +8,9 @@ requiring an interleaving search. - #462: Add `STM_domain.stress_test_par`, similar to `Lin_domain.stress_test` for STM models. +- #472: Switch `arb_cmds` to use an exponential distribution with a + mean of 10, avoiding lists of up to 10000 cmds in `STM_sequential` + (reported by @nikolaushuber). ## 0.3 diff --git a/lib/STM.ml b/lib/STM.ml index ce25ba7c..03441c8e 100644 --- a/lib/STM.ml +++ b/lib/STM.ml @@ -157,8 +157,19 @@ struct | None -> () (* no elem. shrinker provided *) | Some shrink -> Shrink.list_elems shrink l yield + let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s) + + let exp_dist_gen mean = + let unit_gen = Gen.float_bound_inclusive 1.0 in + Gen.map (fun p -> -. mean *. (log p)) unit_gen + + let cmd_list_size_dist mean = + let skew = 0.75 in (* to avoid too many empty cmd lists *) + Gen.map (fun p -> int_of_float (p +. skew)) (exp_dist_gen mean) + let arb_cmds s = - let cmds_gen = Gen.sized (gen_cmds Spec.arb_cmd s) in + let mean = 10. in (* generate on average ~10 cmds, ignoring skew *) + let cmds_gen = gen_cmds_size Spec.arb_cmd s (cmd_list_size_dist mean) in let shrinker = shrink_list ?shrink:(Spec.arb_cmd s).shrink in (* pass opt. elem. shrinker *) let ac = QCheck.make ~shrink:(Shrink.filter (cmds_ok Spec.init_state) shrinker) cmds_gen in (match (Spec.arb_cmd s).print with @@ -237,8 +248,6 @@ struct (let b2 = Spec.postcond c2 s res2 in b2 && check_obs pref cs1 cs2' (Spec.next_state c2 s)) - let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s) - (* Shrinks a single cmd, starting in the given state *) let shrink_cmd arb cmd state = Option.value (arb state).shrink ~default:Shrink.nil @@ cmd diff --git a/test/mutable_set_v4.expected.32 b/test/mutable_set_v4.expected.32 index 2cca3550..40b13a82 100644 --- a/test/mutable_set_v4.expected.32 +++ b/test/mutable_set_v4.expected.32 @@ -2,10 +2,10 @@ --- Failure -------------------------------------------------------------------- -Test STM sequential tests failed (13 shrink steps): +Test STM sequential tests failed (9 shrink steps): - Add (-605797133) - Remove (-605797133) + Add (-923247292) + Remove (-923247292) Cardinal @@ -15,8 +15,8 @@ Messages for test STM sequential tests: Results incompatible with model - Add (-605797133) : () - Remove (-605797133) : Some (-605797133) + Add (-923247292) : () + Remove (-923247292) : Some (-923247292) Cardinal : 1 ================================================================================ failure (1 tests failed, 0 tests errored, ran 1 tests) diff --git a/test/mutable_set_v4.expected.64 b/test/mutable_set_v4.expected.64 index 21e57d85..7a9ef9b5 100644 --- a/test/mutable_set_v4.expected.64 +++ b/test/mutable_set_v4.expected.64 @@ -2,7 +2,7 @@ --- Failure -------------------------------------------------------------------- -Test STM sequential tests failed (13 shrink steps): +Test STM sequential tests failed (11 shrink steps): Add (-3576245632788335623) Remove (-3576245632788335623) diff --git a/test/mutable_set_v5.expected.32 b/test/mutable_set_v5.expected.32 index 6a3b51c8..502ec6ec 100644 --- a/test/mutable_set_v5.expected.32 +++ b/test/mutable_set_v5.expected.32 @@ -4,8 +4,8 @@ Test STM sequential tests failed (2 shrink steps): - Add (-942638288) - Remove (-942638288) + Add (-286715106) + Remove (-286715106) Cardinal @@ -15,8 +15,8 @@ Messages for test STM sequential tests: Results incompatible with model - Add (-942638288) : () - Remove (-942638288) : Some (-942638288) + Add (-286715106) : () + Remove (-286715106) : Some (-286715106) Cardinal : 1 ================================================================================ failure (1 tests failed, 0 tests errored, ran 1 tests) diff --git a/test/mutable_set_v5.expected.64 b/test/mutable_set_v5.expected.64 index 6529f572..b2ddcf1b 100644 --- a/test/mutable_set_v5.expected.64 +++ b/test/mutable_set_v5.expected.64 @@ -2,10 +2,10 @@ --- Failure -------------------------------------------------------------------- -Test STM sequential tests failed (15 shrink steps): +Test STM sequential tests failed (6 shrink steps): - Add (-3922091896265746428) - Remove (-3922091896265746428) + Add 3036269937054427589 + Remove 3036269937054427589 Cardinal @@ -15,8 +15,8 @@ Messages for test STM sequential tests: Results incompatible with model - Add (-3922091896265746428) : () - Remove (-3922091896265746428) : Some (-3922091896265746428) + Add 3036269937054427589 : () + Remove 3036269937054427589 : Some (3036269937054427589) Cardinal : 1 ================================================================================ failure (1 tests failed, 0 tests errored, ran 1 tests)