Add Util functions to make tests with logging of generated test values

lib/STM_domain.ml

@@ -66,7 +66,7 @@ module Make (Spec: Spec) = struct
     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
+    Util.make_test ~show_cmd:Spec.show_cmd ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
@@ -76,7 +76,7 @@ module Make (Spec: Spec) = struct
     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
+    Util.make_neg_test ~show_cmd:Spec.show_cmd ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
@@ -86,7 +86,7 @@ module Make (Spec: Spec) = struct
     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
+    Util.make_test ~show_cmd:Spec.show_cmd ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);
@@ -96,7 +96,7 @@ module Make (Spec: Spec) = struct
     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
+    Util.make_neg_test ~show_cmd:Spec.show_cmd ~retries:10 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun triple ->
          assume (all_interleavings_ok triple);

lib/STM_thread.ml

@@ -43,7 +43,7 @@ module Make (Spec: Spec) = struct
     let rep_count = 100 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:15 ~max_gen ~count ~name
+    Util.make_test ~show_cmd:Spec.show_cmd ~retries:15 ~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);
@@ -53,7 +53,7 @@ module Make (Spec: Spec) = struct
     let rep_count = 100 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:15 ~max_gen ~count ~name
+    Util.make_neg_test ~show_cmd:Spec.show_cmd ~retries:15 ~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,13 +121,13 @@ struct
     (* Linearization test *)
     let lin_test ~rep_count ~retries ~count ~name ~lin_prop =
       let arb_cmd_triple = arb_cmds_triple 20 12 in
-      Test.make ~count ~retries ~name
+      Util.make_test ~count ~retries ~name ~show_cmd:Spec.show_cmd
         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
-      Test.make_neg ~count ~retries ~name
+      Util.make_neg_test ~count ~retries ~name ~show_cmd:Spec.show_cmd
         arb_cmd_triple (repeat rep_count lin_prop)
   end
 end

lib/util.ml

@@ -4,6 +4,40 @@ let rec repeat n prop = fun input ->
   then true
   else prop input && repeat (n-1) prop input
 
+let log_triple_channels = ref None
+
+let set_log_triple_channels oc =
+  (match (oc, !log_triple_channels) with None, Some oc -> close_out oc | _, _ -> ());
+  log_triple_channels := oc
+
+let make_test ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name ?show_cmd arb law =
+  let law =
+    match (show_cmd, !log_triple_channels) with
+    | Some show_cmd, Some oc ->
+        fun trp ->
+          Printf.fprintf oc "Triple: %s\n%!" QCheck.Print.(triple (list show_cmd) (list show_cmd) (list show_cmd) trp);
+          let res = law trp in
+          Printf.fprintf oc " -> %b\n%!" res;
+          res
+    | _, None -> law
+    | None, Some _ -> invalid_arg "show_cmd optional argument must be set when logging is enabled"
+  in
+  QCheck.Test.make ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name arb law
+
+let make_neg_test ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name ?show_cmd arb law =
+  let law =
+    match (show_cmd, !log_triple_channels) with
+    | Some show_cmd, Some oc ->
+        fun trp ->
+          Printf.fprintf oc "Triple: %s\n%!" QCheck.Print.(triple (list show_cmd) (list show_cmd) (list show_cmd) trp);
+          let res = law trp in
+          Printf.fprintf oc " -> %b\n%!" res;
+          res
+    | _, None -> law
+    | None, Some _ -> invalid_arg "show_cmd optional argument must be set when logging is enabled"
+  in
+  QCheck.Test.make_neg ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name arb law
+
 exception Timeout
 
 let prop_timeout sec p x =

lib/util.mli

@@ -8,6 +8,39 @@ val repeat : int -> ('a -> bool) -> 'a -> bool
     This is handy if the property outcome is non-determistic, for example,
     if it depends on scheduling. *)
 
+val set_log_triple_channels : out_channel option -> unit
+(** TODO *)
+
+val make_test :
+  ?if_assumptions_fail:[ `Fatal | `Warning ] * float ->
+  ?count:int ->
+  ?long_factor:int ->
+  ?max_gen:int ->
+  ?max_fail:int ->
+  ?small:('a list * 'a list * 'a list -> int) ->
+  ?retries:int ->
+  ?name:string ->
+  ?show_cmd:'a QCheck.Print.t ->
+  ('a list * 'a list * 'a list) QCheck.arbitrary ->
+  ('a list * 'a list * 'a list -> bool) ->
+  QCheck.Test.t
+(** TODO *)
+
+val make_neg_test :
+  ?if_assumptions_fail:[ `Fatal | `Warning ] * float ->
+  ?count:int ->
+  ?long_factor:int ->
+  ?max_gen:int ->
+  ?max_fail:int ->
+  ?small:('a list * 'a list * 'a list -> int) ->
+  ?retries:int ->
+  ?name:string ->
+  ?show_cmd:'a QCheck.Print.t ->
+  ('a list * 'a list * 'a list) QCheck.arbitrary ->
+  ('a list * 'a list * 'a list -> bool) ->
+  QCheck.Test.t
+(** TODO *)
+
 exception Timeout
 (** exception raised by [prop_timeout] and [fork_prop_with_timeout]. *)
 

test/cleanup_lin.ml

@@ -49,7 +49,7 @@ module RT = Lin_domain.Make_internal(RConf) [@alert "-internal"]
 ;;
 Test.check_exn
   (let seq_len,par_len = 20,15 in
-   Test.make ~count:1000 ~name:("exactly one-cleanup test")
+   Util.make_test ~show_cmd:RConf.show_cmd ~count:1000 ~name:("exactly one-cleanup test")
      (RT.arb_cmds_triple seq_len par_len)
      (fun input ->
         try