Support multiple ts in Lin and Lin_api signatures

lib/lin.mli

@@ -7,6 +7,20 @@
     at any time.
  *)
 module Internal : sig
+  module Var : sig
+    type t = int
+    val next : unit -> t
+    val reset : unit -> unit
+    val pp : Format.formatter -> t -> unit
+    val show : t -> string
+  end
+
+  module Env : sig
+    type t = Var.t list
+    val gen_t_var : t -> Var.t QCheck.Gen.t
+    val valid_t_vars : t -> Var.t -> Var.t QCheck.Iter.t
+  end
+
   module type CmdSpec = sig
     type t
     (** The type of the system under test *)
@@ -17,12 +31,18 @@ module Internal : sig
     val show_cmd : cmd -> string
     (** [show_cmd c] returns a string representing the command [c]. *)
 
-    val gen_cmd : cmd QCheck.Gen.t
-    (** A command generator. *)
+    val gen_cmd : Var.t QCheck.Gen.t -> (Var.t option * cmd) QCheck.Gen.t
+    (** A command generator.
+        It accepts a variable generator and generates a pair [(opt,cmd)] with the option indicating
+        an storage index to store the [cmd]'s result. *)
 
-    val shrink_cmd : cmd QCheck.Shrink.t
+    val shrink_cmd : Env.t -> cmd QCheck.Shrink.t
     (** A command shrinker.
-        To a first approximation you can use {!QCheck.Shrink.nil}. *)
+        It accepts the current environment as its argument.
+        To a first approximation you can use [fun _env -> Shrink.nil]. *)
+
+    val cmd_uses_var : Var.t -> cmd -> bool
+    (** [cmd_uses_var v cmd] should return [true] iff the command [cmd] refers to the variable [v]. *)
 
     type res
     (** The command result type *)
@@ -40,16 +60,27 @@ module Internal : sig
     (** Utility function to clean up [t] after each test instance,
         e.g., for closing sockets, files, or resetting global parameters *)
 
-    val run : cmd -> t -> res
-    (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *)
+    val run : (Var.t option * cmd) -> t array -> res
+    (** [run (opt,c) t] should interpret the command [c] over the various instances of the system under test [t array] (typically side-effecting).
+        [opt] indicates the index to store the result. *)
   end
 
+  type 'cmd cmd_triple =
+    { env_size   : int;
+      seq_prefix : (Var.t option * 'cmd) list;
+      tail_left  : (Var.t option * 'cmd) list;
+      tail_right : (Var.t option * 'cmd) list; }
+
   module Make(Spec : CmdSpec) : sig
-    val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-    val check_seq_cons : (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> Spec.t -> Spec.cmd list -> bool
-    val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list
-    val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
-    val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
+    val init_sut : int -> Spec.t array
+    val cleanup : Spec.t array -> (Var.t option * Spec.cmd) list -> (Var.t option * Spec.cmd) list -> (Var.t option * Spec.cmd) list -> unit
+    val show_cmd : Var.t option * Spec.cmd -> string
+    val init_cmd_ret : string
+    val arb_cmds_triple : int -> int -> Spec.cmd cmd_triple QCheck.arbitrary
+    val check_seq_cons : int -> ((Var.t option * Spec.cmd) * Spec.res) list -> ((Var.t option * Spec.cmd) * Spec.res) list -> ((Var.t option * Spec.cmd) * Spec.res) list -> Spec.t array -> (Var.t option * Spec.cmd) list -> bool
+    val interp_plain : Spec.t array -> (Var.t option * Spec.cmd) list -> ((Var.t option * Spec.cmd) * Spec.res) list
+    val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd cmd_triple -> bool) -> QCheck.Test.t
+    val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd cmd_triple -> bool) -> QCheck.Test.t
   end
 
   val pp_exn : Format.formatter -> exn -> unit
@@ -200,6 +231,12 @@ val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
     and have their elements generated by the [t] combinator.
     It is based on {!QCheck.array}. *)
 
+val bounded_array : int -> ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
+(** The [bounded_array] combinator represents the {{!Stdlib.Array.t}[array]} type.
+    The generated arrays from [bounded_array len t] have a length between [0] and [len]
+    (inclusive) and have their elements generated by the [t] combinator.
+    It is based on {!QCheck.array_of_size}. *)
+
 val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty
 (** The [seq] combinator represents the {!Stdlib.Seq.t} type.
     The generated sequences from [seq t] have a length resulting from {!QCheck.Gen.nat}

lib/lin_domain.ml

@@ -11,23 +11,23 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     List.combine cs (Array.to_list res_arr)
 
   (* Linearization property based on [Domain] and an Atomic flag *)
-  let lin_prop (seq_pref,cmds1,cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = init_sut array_size in
     let pref_obs = interp sut seq_pref in
     let wait = Atomic.make true in
     let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp sut cmds1) with exn -> Error exn) in
     let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in
     let obs1 = Domain.join dom1 in
     let obs2 = Domain.join dom2 in
-    Spec.cleanup sut ;
+    cleanup sut seq_pref cmds1 cmds2;
     let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
     let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
-    check_seq_cons pref_obs obs1 obs2 seq_sut []
+    let seq_sut = init_sut array_size in
+    check_seq_cons array_size pref_obs obs1 obs2 seq_sut []
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-              (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-              (pref_obs,obs1,obs2)
+         @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:init_cmd_ret
+              (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
+              (pref_obs,obs1,obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop

lib/lin_domain.mli

@@ -2,8 +2,9 @@ open Lin
 
 (** functor to build an internal module representing parallel tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
-  val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-  val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> Spec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : Spec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end

lib/lin_effect.ml

@@ -51,14 +51,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       | SchedYield -> "<SchedYield>"
       | UserCmd c  -> Spec.show_cmd c
 
-    let gen_cmd =
+    let gen_cmd env =
       (Gen.frequency
-         [(3,Gen.return SchedYield);
-          (5,Gen.map (fun c -> UserCmd c) Spec.gen_cmd)])
+         [(3,Gen.return (None,SchedYield));
+          (5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
 
-    let shrink_cmd c = match c with
+    let shrink_cmd env c = match c with
       | SchedYield -> Iter.empty
-      | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)
+      | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd env c)
+
+    let cmd_uses_var var c = match c with
+      | SchedYield -> false
+      | UserCmd cmd -> Spec.cmd_uses_var var cmd
 
     type res = SchedYieldRes | UserRes of Spec.res
 
@@ -72,18 +76,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       | _, _ -> false
 
     let run c sut = match c with
-      | SchedYield ->
+      | _, SchedYield ->
           (yield (); SchedYieldRes)
-      | UserCmd uc ->
-          let res = Spec.run uc sut in
+      | opt, UserCmd uc ->
+          let res = Spec.run (opt,uc) sut in
           UserRes res
   end
 
   module EffTest = Internal.Make(EffSpec) [@alert "-internal"]
 
   let arb_cmds_triple = EffTest.arb_cmds_triple
 
-  let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs
+  let filter_res rs = List.filter (fun ((_,c),_) -> c <> EffSpec.SchedYield) rs
 
   let rec interp sut cs = match cs with
     | [] -> []
@@ -92,25 +96,25 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
         (c,res)::interp sut cs
 
   (* Concurrent agreement property based on effect-handler scheduler *)
-  let lin_prop (seq_pref,cmds1,cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = EffTest.init_sut array_size in
+    let pref_obs = EffTest.interp_plain sut (List.filter (fun (_,c) -> c <> EffSpec.SchedYield) seq_pref) in
     (* exclude [Yield]s from sequential prefix *)
-    let pref_obs = EffTest.interp_plain sut (List.filter (fun c -> c <> EffSpec.SchedYield) seq_pref) in
     let obs1,obs2 = ref (Ok []), ref (Ok []) in
     let main () =
       fork (fun () -> let tmp1 = try Ok (interp sut cmds1) with exn -> Error exn in obs1 := tmp1);
       fork (fun () -> let tmp2 = try Ok (interp sut cmds2) with exn -> Error exn in obs2 := tmp2); in
     let () = start_sched main in
-    let () = Spec.cleanup sut in
+    let () = EffTest.cleanup sut seq_pref cmds1 cmds2 in
     let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
     let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
+    let seq_sut = EffTest.init_sut array_size in
     (* exclude [Yield]s from sequential executions when searching for an interleaving *)
-    EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
+    EffTest.check_seq_cons array_size (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
     || QCheck.Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
-    @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-      (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r))
-      (pref_obs,!obs1,!obs2)
+    @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:EffTest.init_cmd_ret
+      (fun (c,r) -> Printf.sprintf "%s : %s" (EffTest.show_cmd c) (EffSpec.show_res r))
+      (pref_obs,!obs1,!obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in

lib/lin_effect.mli

@@ -5,8 +5,9 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   module EffSpec : sig
     type cmd
   end
-  val arb_cmds_triple : int -> int -> (EffSpec.cmd list * EffSpec.cmd list * EffSpec.cmd list) QCheck.arbitrary
-  val lin_prop : (EffSpec.cmd list * EffSpec.cmd list * EffSpec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> EffSpec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : EffSpec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end

lib/lin_thread.ml

@@ -18,25 +18,25 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
   let arb_cmds_triple = arb_cmds_triple
 
   (* Linearization property based on [Thread] *)
-  let lin_prop (seq_pref, cmds1, cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = init_sut array_size in
     let obs1, obs2 = ref (Ok []), ref (Ok []) in
     let pref_obs = interp_plain sut seq_pref in
     let wait = ref true in
     let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_thread sut cmds1) with exn -> Error exn) () in
     let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_thread sut cmds2) with exn -> Error exn) () in
     Thread.join th1;
     Thread.join th2;
-    Spec.cleanup sut;
+    cleanup sut seq_pref cmds1 cmds2;
     let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
     let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
+    let seq_sut = init_sut array_size in
     (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
-    check_seq_cons pref_obs !obs1 !obs2 seq_sut []
+    check_seq_cons array_size pref_obs !obs1 !obs2 seq_sut []
     || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-            (pref_obs,!obs1,!obs2)
+       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:init_cmd_ret
+            (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
+            (pref_obs,!obs1,!obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop

lib/lin_thread.mli

@@ -2,8 +2,9 @@ open Lin
 
 (** functor to build an internal module representing concurrent tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
-  val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-  val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> Spec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : Spec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end

lib/util.ml

@@ -37,8 +37,9 @@ let print_vertical ?(fig_indent=3) show cmds =
   let () = List.iter (fun c -> indent (); print_seq_col c) cmds in
   Buffer.contents buf
 
-let print_triple_vertical ?(fig_indent=10) ?(res_width=20) ?(center_prefix=true) show (seq,cmds1,cmds2) =
+let print_triple_vertical ?(fig_indent=10) ?(res_width=20) ?(center_prefix=true) ?init_cmd show (seq,cmds1,cmds2) =
   let seq,cmds1,cmds2 = List.(map show seq, map show cmds1, map show cmds2) in
+  let seq = match init_cmd with None -> seq | Some init_cmd -> init_cmd::seq in
   let max_width ss = List.fold_left max 0 (List.map String.length ss) in
   let width = List.fold_left max 0 [max_width seq; max_width cmds1; max_width cmds2] in
   let res_width = max width res_width in

lib/util.mli

@@ -29,13 +29,15 @@ val print_triple_vertical :
   ?fig_indent:int ->
   ?res_width:int ->
   ?center_prefix:bool ->
+  ?init_cmd:string ->
   ('a -> string) -> 'a list * 'a list * 'a list -> string
 (** [print_triple_vertical pr (xs,ys,zs)] returns a string representing a
     parallel trace, with [xs] printed first, and then [ys] and [zs] printed
     in parallel.
     Optional [fig_indent] indicates how many spaces it should be indented (default: 10 spaces).
     Optional [res_width] specifies the reserved width for printing each list entry (default: 20 chars).
     Optional [center_prefix] centers the sequential prefix if [true] (the default) and otherwise left-adjust it.
+    Optional [init_cmd] indicates a string-rendered, initial command.
  *)
 
 val protect : ('a -> 'b) -> 'a -> ('b, exn) result