Chore: Collect magic constants

lib/STM_domain.ml

@@ -79,51 +79,47 @@ module MakeExt (Spec: SpecExt) = struct
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,parent_obs,child_obs)
 
+  (* Common magic constants *)
+  let rep_count = 25 (* No. of repetitions of the non-deterministic property *)
+  let retries = 10   (* Additional factor of repetition during shrinking *)
+  let seq_len = 20   (* max length of the sequential prefix *)
+  let par_len = 12   (* max length of the parallel cmd lists *)
+
   let agree_test_par ~count ~name =
-    let rep_count = 25 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make ~retries:10 ~max_gen ~count ~name
+    Test.make ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
   let stress_test_par ~count ~name =
-    let rep_count = 25 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make ~retries:10 ~max_gen ~count ~name
+    Test.make ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
          repeat rep_count stress_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
   let neg_agree_test_par ~count ~name =
-    let rep_count = 25 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make_neg ~retries:10 ~max_gen ~count ~name
+    Test.make_neg ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
   let agree_test_par_asym ~count ~name =
-    let rep_count = 25 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make ~retries:10 ~max_gen ~count ~name
+    Test.make ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
   let neg_agree_test_par_asym ~count ~name =
-    let rep_count = 25 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make_neg ~retries:10 ~max_gen ~count ~name
+    Test.make_neg ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);

lib/STM_thread.ml

@@ -49,22 +49,24 @@ module MakeExt (Spec: SpecExt) = struct
            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,obs1,obs2)
 
+  (* Common magic constants *)
+  let rep_count = 3 (* No. of repetitions of the non-deterministic property *)
+  let retries = 25  (* Additional factor of repetition during shrinking *)
+  let seq_len = 20  (* max length of the sequential prefix *)
+  let par_len = 12  (* max length of the parallel cmd lists *)
+
   let agree_test_conc ~count ~name =
     (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *)
-    let rep_count = 3 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make ~retries:25 ~max_gen ~count ~name
+    Test.make ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun ((seq_pref,cmds1,cmds2) as triple) ->
          assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
          repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)
 
   let neg_agree_test_conc ~count ~name =
-    let rep_count = 3 in
-    let seq_len,par_len = 20,12 in
     let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
-    Test.make_neg ~retries:25 ~max_gen ~count ~name
+    Test.make_neg ~retries ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun ((seq_pref,cmds1,cmds2) as triple) ->
          assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);

lib/lin.ml

@@ -121,15 +121,19 @@ struct
            then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace)
            else (Spec.cleanup seq_sut'; false))
 
+    (* Common magic constants *)
+    let seq_len = 20   (* max length of the sequential prefix *)
+    let par_len = 12   (* max length of the parallel cmd lists *)
+
     (* Linearization test *)
     let lin_test ~rep_count ~retries ~count ~name ~lin_prop =
-      let arb_cmd_triple = arb_cmds_triple 20 12 in
+      let arb_cmd_triple = arb_cmds_triple seq_len par_len in
       Test.make ~count ~retries ~name
         arb_cmd_triple (repeat rep_count lin_prop)
 
     (* Negative linearization test *)
     let neg_lin_test ~rep_count ~retries ~count ~name ~lin_prop =
-      let arb_cmd_triple = arb_cmds_triple 20 12 in
+      let arb_cmd_triple = arb_cmds_triple seq_len par_len in
       Test.make_neg ~count ~retries ~name
         arb_cmd_triple (repeat rep_count lin_prop)
   end

lib/lin_domain.ml

@@ -43,13 +43,17 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     let _ = run_parallel (seq_pref,cmds1,cmds2) in
     true
 
+  (* Common magic constants *)
+  let rep_count = 50 (* No. of repetitions of the non-deterministic property *)
+  let retries = 3    (* Additional factor of repetition during shrinking *)
+
   let lin_test ~count ~name =
-    M.lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
+    M.lin_test ~rep_count ~count ~retries ~name ~lin_prop
 
   let neg_lin_test ~count ~name =
-    neg_lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
+    neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop
 
-  let stress_test ~count ~name =
+  let stress_test ~count ~name = (* Note: magic constants differ for this one *)
     M.lin_test ~rep_count:25 ~count ~retries:5 ~name ~lin_prop:stress_prop
 end
 

lib/lin_effect.ml

@@ -112,17 +112,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r))
       (pref_obs,!obs1,!obs2)
 
+  (* Common magic constants *)
+  let retries = 10  (* Additional factor of repetition during shrinking *)
+  let seq_len = 20  (* max length of the sequential prefix *)
+  let par_len = 12  (* max length of the parallel cmd lists *)
+
   let lin_test ~count ~name =
-    let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in
-    let rep_count = 1 in
-    QCheck.Test.make ~count ~retries:10 ~name
-      arb_cmd_triple (Util.repeat rep_count lin_prop)
+    let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in
+    QCheck.Test.make ~count ~retries ~name arb_cmd_triple lin_prop
 
   let neg_lin_test ~count ~name =
-    let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in
-    let rep_count = 1 in
-    QCheck.Test.make_neg ~count ~retries:10 ~name
-      arb_cmd_triple (Util.repeat rep_count lin_prop)
+    let arb_cmd_triple = EffTest.arb_cmds_triple seq_len par_len in
+    QCheck.Test.make_neg ~count ~retries ~name arb_cmd_triple lin_prop
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))

lib/lin_thread.ml

@@ -49,11 +49,15 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
             (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
             (pref_obs,!obs1,!obs2)
 
+  (* Common magic constants *)
+  let rep_count = 3 (* No. of repetitions of the non-deterministic property *)
+  let retries = 25  (* Additional factor of repetition during shrinking *)
+
   let lin_test ~count ~name =
-    lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop
+    lin_test ~rep_count ~count ~retries ~name ~lin_prop
 
   let neg_lin_test ~count ~name =
-    neg_lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop
+    neg_lin_test ~rep_count ~count ~retries ~name ~lin_prop
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))