Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reduce STM.cmds_gen list size #472

Merged
merged 5 commits into from
Sep 17, 2024
Merged

Reduce STM.cmds_gen list size #472

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
314b95d
Move gen_cmds_size up
jmid Aug 30, 2024
27cbb37
Switch STM.arb_cmds to use an exponential distribution, avoiding list…
jmid Aug 30, 2024
984c8ce
Update expect test output
jmid Aug 30, 2024
bdd363a
Add a CHANGES entry
jmid Sep 2, 2024
a661f27
Factor exp_dist_gen into two combinators
jmid Sep 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
15 changes: 12 additions & 3 deletions lib/STM.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions test/mutable_set_v4.expected.32
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand All @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion test/mutable_set_v4.expected.64
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
8 changes: 4 additions & 4 deletions test/mutable_set_v5.expected.32
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@

Test STM sequential tests failed (2 shrink steps):

Add (-942638288)
Remove (-942638288)
Add (-286715106)
Remove (-286715106)
Cardinal


Expand All @@ -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)
Expand Down
10 changes: 5 additions & 5 deletions test/mutable_set_v5.expected.64
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand All @@ -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)
Expand Down