diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml index 6d8d3dffa..df45549d4 100644 --- a/lib/STM_domain.ml +++ b/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); diff --git a/lib/STM_thread.ml b/lib/STM_thread.ml index 89447ff42..79f0c54c5 100644 --- a/lib/STM_thread.ml +++ b/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); diff --git a/lib/lin.ml b/lib/lin.ml index 6a1fb7609..84534417d 100644 --- a/lib/lin.ml +++ b/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 diff --git a/lib/util.ml b/lib/util.ml index be23eedf8..2019c9865 100644 --- a/lib/util.ml +++ b/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 = diff --git a/lib/util.mli b/lib/util.mli index 915458017..d51900287 100644 --- a/lib/util.mli +++ b/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]. *) diff --git a/test/cleanup_lin.ml b/test/cleanup_lin.ml index 23e25728c..96a0700da 100644 --- a/test/cleanup_lin.ml +++ b/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