From e902ec175d434a1086bffd66d01638e0c2970840 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 12 Aug 2022 16:38:33 +0200
Subject: [PATCH 01/57] initial Lin attempt to support multiple ts

---
 lib/lin.ml | 183 +++++++++++++++++++++++++++++++++++------------------
 1 file changed, 122 insertions(+), 61 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 68bdb0ff9..419dfedff 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -1,6 +1,33 @@
 open QCheck
 include Util
 
+module Var : sig
+  type t = int
+  val next : unit -> t
+  val reset : unit -> unit
+  val pp : Format.formatter -> t -> unit
+  val shrink : t Shrink.t
+end =
+struct
+  type t = int
+  let next, reset =
+    let counter = ref 0 in
+    (fun () -> let old = !counter in
+      incr counter; old),
+    (fun () -> counter := 0)
+  let pp fmt v = Format.fprintf fmt "v%i" v
+  let shrink = Shrink.int
+end
+
+module Env : sig
+  type t = Var.t list
+  val gen_t_var : t -> Var.t Gen.t
+end =
+struct
+  type t = Var.t list
+  let gen_t_var env = Gen.oneofl env
+end
+
 module type CmdSpec = sig
   type t
   (** The type of the system under test *)
@@ -11,8 +38,10 @@ module type CmdSpec = sig
   val show_cmd : cmd -> string
   (** [show_cmd c] returns a string representing the command [c]. *)
 
-  val gen_cmd : cmd Gen.t
-  (** A command generator. *)
+  val gen_cmd : Var.t Gen.t -> (Var.t option * cmd) 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 Shrink.t
   (** A command shrinker.
@@ -33,8 +62,9 @@ module type CmdSpec = 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 system under test [t] (typically side-effecting).
+      [opt] indicates the index to store the result. *)
 end
 
 (** A functor to create Domain and Thread test setups.
@@ -62,18 +92,23 @@ module MakeDomThr(Spec : CmdSpec)
         let res = Spec.run c sut in
         (c,res)::interp_thread sut cs
 
-  let rec gen_cmds fuel =
+  (* val gen_cmds : Env.t -> int -> (Env.t * (Var.t option * Spec.cmd) list) Gen.t *)
+  let rec gen_cmds env fuel =
     Gen.(if fuel = 0
-         then return []
+         then return (env,[])
          else
-  	  Spec.gen_cmd >>= fun c ->
-	   gen_cmds (fuel-1) >>= fun cs ->
-             return (c::cs))
-  (** A fueled command list generator. *)
+           Spec.gen_cmd (Env.gen_t_var env) >>= fun (opt,c) ->
+             let env = match opt with None -> env | Some v -> v::env in
+             gen_cmds env (fuel-1) >>= fun (env,cs) -> return (env,(opt,c)::cs))
+  (** A fueled command list generator.
+      Accepts an environment parameter [env] to enable [cmd] generation of multiple [t]s
+      and returns the extended environment. *)
+
+  let gen_cmds_size env size_gen = Gen.sized_size size_gen (gen_cmds env)
 
-  let gen_cmds_size size_gen = Gen.sized_size size_gen gen_cmds
+  let shrink_cmd (opt,c) = Iter.map (fun c -> opt,c) (Spec.shrink_cmd c)
 
-  let shrink_triple (seq,p1,p2) =
+  let shrink_triple' (seq,p1,p2) =
     let open Iter in
     (* Shrinking heuristic:
        First reduce the cmd list sizes as much as possible, since the interleaving
@@ -89,53 +124,78 @@ module MakeDomThr(Spec : CmdSpec)
     (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
     <+>
     (* Secondly reduce the cmd data of individual list elements *)
-    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems Spec.shrink_cmd seq))
+    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
     <+>
-    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems Spec.shrink_cmd p1))
+    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems shrink_cmd p1))
     <+>
-    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems Spec.shrink_cmd p2))
+    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems shrink_cmd p2))
+
+  let shrink_triple (size,t) =
+    Iter.map (fun t -> (size,t)) (shrink_triple' t)
+
+  let show_cmd (opt,c) = match opt with
+    | None   -> Spec.show_cmd c
+    | Some v -> Printf.sprintf "let v%i = %s" v (Spec.show_cmd c)
 
   let arb_cmds_par seq_len par_len =
-    let gen_triple =
+    let gen_triple st =
+      Var.reset ();
+      let init_var = Var.next () in
+      assert (init_var = 0);
       Gen.(int_range 2 (2*par_len) >>= fun dbl_plen ->
-           let seq_pref_gen = gen_cmds_size (int_bound seq_len) in
            let par_len1 = dbl_plen/2 in
-           let par_gen1 = gen_cmds_size (return par_len1) in
-           let par_gen2 = gen_cmds_size (return (dbl_plen - par_len1)) in
-           triple seq_pref_gen par_gen1 par_gen2) in
-    make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
-
-  let rec check_seq_cons pref cs1 cs2 seq_sut seq_trace = match pref with
+           gen_cmds_size [init_var] (int_bound seq_len) >>= fun (env,seq_pref) ->
+           gen_cmds_size env (return par_len1) >>= fun (_env1,par1) ->
+           gen_cmds_size env (return (dbl_plen - par_len1)) >>= fun (_env2,par2) ->
+           let array_size = Var.next () in
+           return (array_size,(seq_pref,par1,par2))) st
+    in
+    make ~print:(fun (_,t) -> print_triple_vertical show_cmd t) ~shrink:shrink_triple gen_triple
+
+  let init_sut array_size =
+    let sut = Spec.init () in
+    Array.make array_size sut
+
+  let cleanup sut seq_pref cmds1 cmds2 =
+    let cleanup_opt ((opt,_c),_res) = match opt with
+      | None -> ()
+      | Some v -> Spec.cleanup sut.(v) in
+    Spec.cleanup sut.(0); (* always present *)
+    List.iter cleanup_opt seq_pref;
+    List.iter cleanup_opt cmds1;
+    List.iter cleanup_opt cmds2
+
+  let rec check_seq_cons array_size pref cs1 cs2 seq_sut seq_trace = match pref with
     | (c,res)::pref' ->
         if Spec.equal_res res (Spec.run c seq_sut)
-        then check_seq_cons pref' cs1 cs2 seq_sut (c::seq_trace)
-        else (Spec.cleanup seq_sut; false)
+        then check_seq_cons array_size pref' cs1 cs2 seq_sut (c::seq_trace)
+        else (cleanup seq_sut pref cs1 cs2; false)
     (* Invariant: call Spec.cleanup immediately after mismatch  *)
     | [] -> match cs1,cs2 with
-            | [],[] -> Spec.cleanup seq_sut; true
+            | [],[] -> cleanup seq_sut pref cs1 cs2; true
             | [],(c2,res2)::cs2' ->
                 if Spec.equal_res res2 (Spec.run c2 seq_sut)
-                then check_seq_cons pref cs1 cs2' seq_sut (c2::seq_trace)
-                else (Spec.cleanup seq_sut; false)
+                then check_seq_cons array_size pref cs1 cs2' seq_sut (c2::seq_trace)
+                else (cleanup seq_sut pref cs1 cs2; false)
             | (c1,res1)::cs1',[] ->
                 if Spec.equal_res res1 (Spec.run c1 seq_sut)
-                then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-                else (Spec.cleanup seq_sut; false)
+                then check_seq_cons array_size pref cs1' cs2 seq_sut (c1::seq_trace)
+                else (cleanup seq_sut pref cs1 cs2; false)
             | (c1,res1)::cs1',(c2,res2)::cs2' ->
                 (if Spec.equal_res res1 (Spec.run c1 seq_sut)
-                 then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-                 else (Spec.cleanup seq_sut; false))
+                 then check_seq_cons array_size pref cs1' cs2 seq_sut (c1::seq_trace)
+                 else (cleanup seq_sut pref cs1 cs2; false))
                 ||
                 (* rerun to get seq_sut to same cmd branching point *)
-                (let seq_sut' = Spec.init () in
+                (let seq_sut' = init_sut array_size in
                  let _ = interp_plain seq_sut' (List.rev seq_trace) in
                  if Spec.equal_res res2 (Spec.run c2 seq_sut')
-                 then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace)
-                 else (Spec.cleanup seq_sut'; false))
+                 then check_seq_cons array_size pref cs1 cs2' seq_sut' (c2::seq_trace)
+                 else (cleanup seq_sut' pref cs1 cs2; false))
 
   (* Linearizability property based on [Domain] and an Atomic flag *)
-  let lin_prop_domain (seq_pref,cmds1,cmds2) =
-    let sut = Spec.init () in
+  let lin_prop_domain (array_size, (seq_pref,cmds1,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
@@ -144,17 +204,18 @@ module MakeDomThr(Spec : CmdSpec)
     let obs2 = Domain.join dom2 in
     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 []
+    cleanup sut pref_obs obs1 obs2;
+    let seq_sut = init_sut array_size in
+    check_seq_cons array_size pref_obs obs1 obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
-              (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
+              (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
               (pref_obs,obs1,obs2)
 
   (* Linearizability property based on [Thread] *)
   let lin_prop_thread =
-    (fun (seq_pref, cmds1, cmds2) ->
-      let sut = Spec.init () in
+    (fun (array_size, (seq_pref, cmds1, cmds2)) ->
+      let sut = init_sut array_size in
       let obs1, obs2 = ref [], ref [] in
       let pref_obs = interp_plain sut seq_pref in
       let wait = ref true in
@@ -162,13 +223,13 @@ module MakeDomThr(Spec : CmdSpec)
       let th2 = Thread.create (fun () -> wait := false; obs2 := interp_thread sut cmds2) () in
       Thread.join th1;
       Thread.join th2;
-      Spec.cleanup sut;
-      let seq_sut = Spec.init () in
+      cleanup sut pref_obs !obs1 !obs2;
+      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 []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
-              (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
+              (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
               (pref_obs,!obs1,!obs2))
 end
 
@@ -219,16 +280,16 @@ module Make(Spec : CmdSpec)
     let init = Spec.init
     let cleanup = Spec.cleanup
 
-    type cmd = SchedYield | UserCmd of Spec.cmd [@@deriving qcheck]
+    type cmd = SchedYield | UserCmd of Spec.cmd
 
     let show_cmd c = match c with
       | 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
       | SchedYield -> Iter.empty
@@ -246,36 +307,36 @@ module Make(Spec : CmdSpec)
       | _, _ -> 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 = MakeDomThr(EffSpec)
 
-  let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs
+  let filter_res rs = List.filter (fun ((_,c),_) -> c <> EffSpec.SchedYield) rs
 
   (* Parallel agreement property based on effect-handler scheduler *)
   let lin_prop_effect =
-    (fun (seq_pref,cmds1,cmds2) ->
-       let sut = Spec.init () in
+    (fun (array_size,(seq_pref,cmds1,cmds2)) ->
+       let sut = EffTest.init_sut array_size 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 pref_obs = EffTest.interp_plain sut (List.filter (fun (_,c) -> c <> EffSpec.SchedYield) seq_pref) in
        let obs1,obs2 = ref [], ref [] in
        let main () =
          (* For now, we reuse [interp_thread] which performs useless [Thread.yield] on single-domain/fibered program *)
          fork (fun () -> let tmp1 = EffTest.interp_thread sut cmds1 in obs1 := tmp1);
          fork (fun () -> let tmp2 = EffTest.interp_thread sut cmds2 in obs2 := tmp2); in
        let () = start_sched main in
-       let () = Spec.cleanup sut in
-       let seq_sut = Spec.init () in
+       let () = EffTest.cleanup sut pref_obs !obs1 !obs2 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 []
        || 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))
+         (fun (c,r) -> Printf.sprintf "%s : %s" (EffTest.show_cmd c) (EffSpec.show_res r))
          (pref_obs,!obs1,!obs2))
 
   module FirstTwo = MakeDomThr(Spec)

From 742118bc659b5fab14a28d7dc7f095accd9aaccd Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 12 Aug 2022 16:39:09 +0200
Subject: [PATCH 02/57] array test example updated

---
 src/array/lin_tests.ml | 96 ++++++++++++++++++++++++++++++------------
 1 file changed, 70 insertions(+), 26 deletions(-)

diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml
index 2c4f15549..ea95150c2 100644
--- a/src/array/lin_tests.ml
+++ b/src/array/lin_tests.ml
@@ -7,30 +7,68 @@ module AConf =
 struct
   type t = char array
 
+ (* note to self:
+    - generate one t_var per input [t] parameter and
+    - record [Env.next] for each resulting [t] in an option *)
+  open Lin
   type cmd =
-    | Length
-    | Get of int'
-    | Set of int' * char'
-    | Sub of int' * int'
-    | Copy
-    | Fill of int' * int' * char'
-    | To_list
-    | Mem of char'
-    | Sort
-    | To_seq [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.small_nat]
-  and char' = char [@gen Gen.printable]
+    | Length of Var.t
+    | Get of Var.t * int
+    | Set of Var.t * int * char
+    | Append of Var.t * Var.t
+    | Sub of Var.t * int * int
+    | Copy of Var.t
+    | Fill of Var.t * int * int * char
+    | To_list of Var.t
+    | Mem of Var.t * char
+    | Sort of Var.t
+    | To_seq of Var.t [@@deriving show { with_path = false }]
 
-  let shrink_cmd c = Iter.empty
+  let gen_int = Gen.small_nat
+  let gen_char = Gen.printable
+  let map4 f w x y z st = f (w st) (x st) (y st) (z st)
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> (None, Length t)) gen_var;
+        map2 (fun t i -> (None, Get (t,i))) gen_var gen_int;
+        map3 (fun t i c -> (None, Set (t,i,c))) gen_var gen_int gen_char;
+        map2 (fun t1 t2 -> (Some (Var.next ()), Append (t1,t2))) gen_var gen_var;
+        map3 (fun v i l -> (Some (Var.next ()), Sub (v,i,l))) gen_var gen_int gen_int;
+        map  (fun t -> (Some (Var.next ()), Copy t)) gen_var;
+        map4 (fun v i l c -> (None, Fill (v,i,l,c))) gen_var gen_int gen_int gen_char;
+        map  (fun v -> (None, To_list v)) gen_var;
+        map2 (fun v c -> (None, Mem (v,c))) gen_var gen_char;
+        map  (fun v -> (None, Sort v)) gen_var;
+        map  (fun v -> (None, To_seq v)) gen_var;
+      ])
+
+  let shrink_cmd c = match c with
+    | Length v     -> Iter.map (fun v -> Length v)    (Var.shrink v)
+    | Get (v,i)    -> Iter.map (fun v -> Get (v,i))   (Var.shrink v)
+    | Set (v,i,c)  -> Iter.map (fun v -> Set (v,i,c)) (Var.shrink v)
+    | Append (v,w) ->
+      Iter.(map (fun v -> Append (v,w)) (Var.shrink v)
+            <+>
+            map (fun w -> Append (v,w)) (Var.shrink w))
+    | Sub (v,i,l) -> Iter.map (fun v -> Sub (v,i,l)) (Var.shrink v)
+    | Copy v      -> Iter.map (fun v -> Copy v)      (Var.shrink v)
+    | Fill (v,i,l,c) -> Iter.map (fun v -> Fill (v,i,l,c)) (Var.shrink v)
+    | To_list v   -> Iter.map (fun v -> To_list v)   (Var.shrink v)
+    | Mem (v,c)   -> Iter.map (fun v -> Mem (v,c))   (Var.shrink v)
+    | Sort v      -> Iter.map (fun v -> Sort v)      (Var.shrink v)
+    | To_seq v    -> Iter.map (fun v -> To_seq v)    (Var.shrink v)
 
   open Util
   (*let pp_exn = Util.pp_exn*)
+  let pp fmt t = Format.fprintf fmt "%s" (QCheck.Print.(array char) t)
+  let equal a1 a2 = Array.for_all2 (=) a1 a2
   type res =
     | RLength of int
     | RGet of ((char, exn) result)
     | RSet of ((unit, exn) result)
-    | RSub of ((char array, exn) result)
-    | RCopy of char array
+    | RAppend of unit
+    | RSub of ((unit, exn) result)
+    | RCopy of unit
     | RFill of ((unit, exn) result)
     | RTo_list of char list
     | RMem of bool
@@ -38,21 +76,27 @@ struct
     | RTo_seq of (char Seq.t [@printer fun fmt seq -> fprintf fmt "%s" (QCheck.Print.(list char) (List.of_seq seq))])
   [@@deriving show { with_path = false }, eq]
 
-  let array_size = 16
+  let array_size = 2
 
   let init () = Array.make array_size 'a'
 
+  (* FIXME:
+     - shrink target variables generically:
+       match on optional target i, unless someone is refering to it (how to tell for arb. cmds?)
+  *)
   let run c a = match c with
-    | Length        -> RLength (Array.length a)
-    | Get i         -> RGet (Util.protect (Array.get a) i)
-    | Set (i,c)     -> RSet (Util.protect (Array.set a i) c)
-    | Sub (i,l)     -> RSub (Util.protect (Array.sub a i) l)
-    | Copy          -> RCopy (Array.copy a)
-    | Fill (i,l,c)  -> RFill (Util.protect (Array.fill a i l) c)
-    | To_list       -> RTo_list (Array.to_list a)
-    | Mem c         -> RMem (Array.mem c a)
-    | Sort          -> RSort (Array.sort Char.compare a)
-    | To_seq        -> RTo_seq (List.to_seq (List.of_seq (Array.to_seq a))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *)
+    | None,   Length v       -> RLength (Array.length a.(v))
+    | None,   Get (v,i)      -> RGet (Util.protect (Array.get a.(v)) i)
+    | None,   Set (v,i,c)    -> RSet (Util.protect (Array.set a.(v) i) c)
+    | Some r, Append (v,w)   -> RAppend (let tmp = Array.append a.(v) a.(w) in a.(r) <- tmp)
+    | Some r, Sub (v,i,l)    -> RSub (Util.protect (fun () -> let tmp = Array.sub a.(v) i l in a.(r) <- tmp) ())
+    | Some r, Copy v         -> RCopy (let tmp = Array.copy a.(v) in a.(r) <- tmp)
+    | None,   Fill (v,i,l,c) -> RFill (Util.protect (Array.fill a.(v) i l) c)
+    | None,   To_list v      -> RTo_list (Array.to_list a.(v))
+    | None,   Mem (v,c)      -> RMem (Array.mem c a.(v))
+    | None,   Sort v         -> RSort (Array.sort Char.compare a.(v))
+    | None,   To_seq v       -> RTo_seq (List.to_seq (List.of_seq (Array.to_seq a.(v)))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   let cleanup _ = ()
 end
 

From 6864a6d7f54b563dedbaf8c725f9952dc3fff27e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 12 Aug 2022 17:11:02 +0200
Subject: [PATCH 03/57] port Hashtbl test example

---
 src/hashtbl/lin_tests.ml | 84 ++++++++++++++++++++++++----------------
 1 file changed, 51 insertions(+), 33 deletions(-)

diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml
index 625ba78be..527adafcc 100644
--- a/src/hashtbl/lin_tests.ml
+++ b/src/hashtbl/lin_tests.ml
@@ -9,37 +9,53 @@ struct
   type t = (char, int) Hashtbl.t
 
   type cmd =
-    | Clear
-    | Add of char' * int'
-    | Remove of char'
-    | Find of char'
-    | Find_opt of char'
-    | Find_all of char'
-    | Replace of char' * int'
-    | Mem of char'
-    | Length [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
-  and char' = char [@gen Gen.printable]
+    | Clear of Var.t
+    | Copy of Var.t
+    | Add of Var.t * char * int
+    | Remove of Var.t * char
+    | Find of Var.t * char
+    | Find_opt of Var.t * char
+    | Find_all of Var.t * char
+    | Replace of Var.t * char * int
+    | Mem of Var.t * char
+    | Length of Var.t [@@deriving show { with_path = false }]
+  let gen_int = Gen.nat
+  let gen_char = Gen.printable
 
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun v -> None,Clear v) gen_var;
+        map  (fun v -> Some (Var.next ()),Copy v) gen_var;
+        map3 (fun v c i -> None,Add (v,c,i)) gen_var gen_char gen_int;
+        map2 (fun v c -> None,Remove (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find_opt (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find_all (v,c)) gen_var gen_char;
+        map3 (fun v c i -> None,Replace (v,c,i)) gen_var gen_char gen_int;
+        map2 (fun v c -> None,Mem (v,c)) gen_var gen_char;
+        map  (fun v -> None,Length v) gen_var;
+      ])
   let shrink_cmd c = match c with
-    | Clear -> Iter.empty
-    | Add (c,i) ->
-        Iter.((map (fun c -> Add (c,i)) (Shrink.char c))
+    | Clear _ -> Iter.empty
+    | Copy _ -> Iter.empty
+    | Add (v,c,i) ->
+        Iter.((map (fun c -> Add (v,c,i)) (Shrink.char c))
               <+>
-              (map (fun i -> Add (c,i)) (Shrink.int i)))
-    | Remove c -> Iter.map (fun c -> Remove c) (Shrink.char c)
-    | Find c -> Iter.map (fun c -> Find c) (Shrink.char c)
-    | Find_opt c -> Iter.map (fun c -> Find_opt c) (Shrink.char c)
-    | Find_all c -> Iter.map (fun c -> Find_all c) (Shrink.char c)
-    | Replace (c,i) ->
-        Iter.((map (fun c -> Replace (c,i)) (Shrink.char c))
+              (map (fun i -> Add (v,c,i)) (Shrink.int i)))
+    | Remove (v,c) -> Iter.map (fun c -> Remove (v,c)) (Shrink.char c)
+    | Find (v,c) -> Iter.map (fun c -> Find (v,c)) (Shrink.char c)
+    | Find_opt (v,c) -> Iter.map (fun c -> Find_opt (v,c)) (Shrink.char c)
+    | Find_all (v,c) -> Iter.map (fun c -> Find_all (v,c)) (Shrink.char c)
+    | Replace (v,c,i) ->
+        Iter.((map (fun c -> Replace (v,c,i)) (Shrink.char c))
               <+>
-              (map (fun i -> Replace (c,i)) (Shrink.int i)))
-    | Mem c -> Iter.map (fun c -> Mem c) (Shrink.char c)
-    | Length -> Iter.empty
+              (map (fun i -> Replace (v,c,i)) (Shrink.int i)))
+    | Mem (v,c) -> Iter.map (fun c -> Mem (v,c)) (Shrink.char c)
+    | Length _ -> Iter.empty
 
   type res =
     | RClear
+    | RCopy
     | RAdd
     | RRemove
     | RFind of ((int, exn) result [@equal (=)])
@@ -52,15 +68,17 @@ struct
   let init () = Hashtbl.create ~random:false 42
 
   let run c h = match c with
-    | Clear         -> Hashtbl.clear h; RClear
-    | Add (k,v)     -> Hashtbl.add h k v; RAdd
-    | Remove k      -> Hashtbl.remove h k; RRemove
-    | Find k        -> RFind (Util.protect (Hashtbl.find h) k)
-    | Find_opt k    -> RFind_opt (Hashtbl.find_opt h k)
-    | Find_all k    -> RFind_all (Hashtbl.find_all h k)
-    | Replace (k,v) -> Hashtbl.replace h k v; RReplace
-    | Mem k         -> RMem (Hashtbl.mem h k)
-    | Length        -> RLength (Hashtbl.length h)
+    | None, Clear w         -> Hashtbl.clear h.(w); RClear
+    | Some r, Copy w        -> let tmp = Hashtbl.copy h.(w) in h.(r) <- tmp; RCopy
+    | None, Add (w,k,v)     -> Hashtbl.add h.(w) k v; RAdd
+    | None, Remove (w,k)    -> Hashtbl.remove h.(w) k; RRemove
+    | None, Find (w,k)      -> RFind (Util.protect (fun () -> Hashtbl.find h.(w) k) ())
+    | None, Find_opt (w,k)  -> RFind_opt (Hashtbl.find_opt h.(w) k)
+    | None, Find_all (w,k)  -> RFind_all (Hashtbl.find_all h.(w) k)
+    | None, Replace (w,k,v) -> Hashtbl.replace h.(w) k v; RReplace
+    | None, Mem (w,k)       -> RMem (Hashtbl.mem h.(w) k)
+    | None, Length w        -> RLength (Hashtbl.length h.(w))
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end

From 86979cb0d54837bc5f28fdb932c84c6cbfd9d7c5 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 15 Aug 2022 19:33:42 +0200
Subject: [PATCH 04/57] add optional init_cmd printer

---
 lib/util.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/util.ml b/lib/util.ml
index 9b4b07fb9..4f9757bac 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -34,8 +34,9 @@ let fork_prop_with_timeout sec p x =
      | WSIGNALED _
      | WSTOPPED _  -> false)
 
-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

From a9dfab454f4e779b86caf677dbfa96e8a38d0e76 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 15 Aug 2022 19:34:33 +0200
Subject: [PATCH 05/57] add show function and use init_cmd printer

---
 lib/lin.ml | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 419dfedff..00faa15c4 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -6,6 +6,7 @@ module Var : sig
   val next : unit -> t
   val reset : unit -> unit
   val pp : Format.formatter -> t -> unit
+  val show : t -> string
   val shrink : t Shrink.t
 end =
 struct
@@ -15,7 +16,14 @@ struct
     (fun () -> let old = !counter in
       incr counter; old),
     (fun () -> counter := 0)
-  let pp fmt v = Format.fprintf fmt "v%i" v
+  let pp fmt v = Format.fprintf fmt "t%i%!" v
+  let show t =
+    let buf = Buffer.create 24 in
+    let fmt = Format.formatter_of_buffer buf in
+    pp fmt t;
+    let str = Buffer.contents buf in
+    Buffer.clear buf;
+    str
   let shrink = Shrink.int
 end
 
@@ -135,7 +143,9 @@ module MakeDomThr(Spec : CmdSpec)
 
   let show_cmd (opt,c) = match opt with
     | None   -> Spec.show_cmd c
-    | Some v -> Printf.sprintf "let v%i = %s" v (Spec.show_cmd c)
+    | Some v -> Printf.sprintf "let %s = %s" (Var.show v) (Spec.show_cmd c)
+
+  let init_cmd = "let t0 = init ()"
 
   let arb_cmds_par seq_len par_len =
     let gen_triple st =
@@ -150,7 +160,7 @@ module MakeDomThr(Spec : CmdSpec)
            let array_size = Var.next () in
            return (array_size,(seq_pref,par1,par2))) st
     in
-    make ~print:(fun (_,t) -> print_triple_vertical show_cmd t) ~shrink:shrink_triple gen_triple
+    make ~print:(fun (_,t) -> print_triple_vertical ~init_cmd show_cmd t) ~shrink:shrink_triple gen_triple
 
   let init_sut array_size =
     let sut = Spec.init () in
@@ -208,7 +218,7 @@ module MakeDomThr(Spec : CmdSpec)
     let seq_sut = init_sut array_size in
     check_seq_cons array_size pref_obs obs1 obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ print_triple_vertical ~fig_indent:5 ~res_width:35
+         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd
               (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
               (pref_obs,obs1,obs2)
 
@@ -228,7 +238,7 @@ module MakeDomThr(Spec : CmdSpec)
       (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
       check_seq_cons array_size pref_obs !obs1 !obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ print_triple_vertical ~fig_indent:5 ~res_width:35
+         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd
               (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
               (pref_obs,!obs1,!obs2))
 end
@@ -335,7 +345,7 @@ module Make(Spec : CmdSpec)
        (* exclude [Yield]s from sequential executions when searching for an interleaving *)
        EffTest.check_seq_cons array_size (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
        || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
-       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
+       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:EffTest.init_cmd
          (fun (c,r) -> Printf.sprintf "%s : %s" (EffTest.show_cmd c) (EffSpec.show_res r))
          (pref_obs,!obs1,!obs2))
 

From 0457c8487723ee42948311fa4018f69a6d99c80a Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 15 Aug 2022 19:35:38 +0200
Subject: [PATCH 06/57] initial support for multiple ts in Lin_api + some
 documentation

---
 lib/lin_api.ml  | 115 ++++++++++++++++++++++++++++--------------------
 lib/lin_api.mli |  27 ++++++++----
 2 files changed, 86 insertions(+), 56 deletions(-)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 0d301e728..84aedc7c2 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -94,12 +94,11 @@ let or_exn ty = match ty with
   | Deconstr (print, eq) ->
       Deconstr (print_result print Printexc.to_string, Result.equal ~ok:eq ~error:(=))
 
-let print : type a c s comb. (a, c, s, comb) ty -> a -> string = fun ty value ->
+let print : type a c s. (a, c, s, combinable) ty -> a -> string = fun ty value ->
   match ty with
   | Gen (_,print) -> print value
   | Deconstr (print,_) -> print value
   | GenDeconstr (_,print,_) -> print value
-  | State -> "t"
 
 let equal : type a s c. (a, deconstructible, s, c) ty -> a -> a -> bool = fun ty ->
   match ty with
@@ -111,8 +110,8 @@ module Fun = struct
   type (_,_,_) fn =
     | Ret :        ('a, deconstructible, 's, combinable) ty -> ('a, 'a, 's) fn
     | Ret_or_exc : ('a, deconstructible, 's, combinable) ty -> ('a, ('a,exn) result, 's) fn
-    | Ret_ignore : ('a, _, 's, combinable) ty -> ('a, unit, 's) fn
-    | Ret_ignore_or_exc : ('a, _, 's, combinable) ty -> ('a, (unit,exn) result, 's) fn
+    | Ret_ignore : ('a, _, 's, _) ty -> ('a, unit, 's) fn
+    | Ret_ignore_or_exc : ('a, _, 's, _) ty -> ('a, (unit,exn) result, 's) fn
     | Fn : ('a, constructible, 's, _) ty * ('b, 'r, 's) fn -> ('a -> 'b, 'r, 's) fn
 end
 
@@ -155,7 +154,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
     | Ret_ignore : ('a, _, t, _) ty -> ('a, unit) args
     | Ret_ignore_or_exc : ('a, _, t, _) ty -> ('a, (unit,exn) result) args
     | Fn : 'a * ('b,'r) args -> ('a -> 'b, 'r) args
-    | FnState : ('b,'r) args -> (t -> 'b, 'r) args
+    | FnState : Lin.Var.t * ('b,'r) args -> (t -> 'b, 'r) args
   end
 
   (* Operation name, typed argument list, return type descriptor, printer, shrinker, function *)
@@ -175,8 +174,8 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
   (* Function to generate typed list of arguments from a function description.
      The printer can be generated independently. *)
   let rec gen_args_of_desc
-    : type a r. (a, r, t) Fun.fn -> ((a, r) Args.args) QCheck.Gen.t =
-    fun fdesc ->
+    : type a r. (a, r, t) Fun.fn -> (Lin.Var.t QCheck.Gen.t) -> ((a, r) Args.args) QCheck.Gen.t =
+    fun fdesc gen_var ->
       let open QCheck.Gen in
       match fdesc with
       | Fun.Ret ty -> return @@ Args.Ret ty
@@ -184,28 +183,37 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
       | Fun.Ret_ignore_or_exc ty -> return @@ Args.Ret_ignore_or_exc ty
       | Fun.Ret_ignore ty -> return @@ Args.Ret_ignore ty
       | Fun.(Fn (State, fdesc_rem)) ->
-          let* args_rem = gen_args_of_desc fdesc_rem in
-          return @@ Args.FnState args_rem
+          map2 (fun state_arg args_rem -> Args.FnState (state_arg, args_rem))
+            gen_var (gen_args_of_desc fdesc_rem gen_var)
+       (* let* state_arg = gen_var in
+          let* args_rem = gen_args_of_desc fdesc_rem gen_var in
+          return @@ Args.FnState (state_arg, args_rem) *)
       | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
-          let* arg = arg_arb.gen in
-          let* args_rem = gen_args_of_desc fdesc_rem in
-          return @@ Args.Fn (arg, args_rem)
+          map2 (fun arg args_rem -> Args.Fn (arg, args_rem))
+            arg_arb.gen (gen_args_of_desc fdesc_rem gen_var)
+       (* let* arg = arg_arb.gen in
+          let* args_rem = gen_args_of_desc fdesc_rem gen_var in
+          return @@ Args.Fn (arg, args_rem) *)
 
   let rec ret_type
-    : type a r. (a,r,t) Fun.fn -> (r, deconstructible, t, _) ty
+    : type a r. (a,r,t) Fun.fn -> Lin.Var.t option * (r, deconstructible, t, _) ty
     = fun fdesc ->
       match fdesc with
-      | Fun.Ret ty -> ty
-      | Fun.Ret_or_exc ty -> or_exn ty
-      | Fun.Ret_ignore _ -> unit
-      | Fun.Ret_ignore_or_exc _ -> or_exn unit
+      | Fun.Ret ty -> None, ty
+      | Fun.Ret_or_exc ty -> None, or_exn ty
+      | Fun.Ret_ignore ty -> (match ty with
+          | State -> Some (Lin.Var.next ()), unit
+          | _     -> None, unit)
+      | Fun.Ret_ignore_or_exc ty -> (match ty with
+          | State -> Some (Lin.Var.next ()), or_exn unit
+          | _     -> None, or_exn unit)
       | Fun.Fn (_, fdesc_rem) -> ret_type fdesc_rem
 
   let rec show_args : type a r. (a,r,t) Fun.fn -> (a,r) Args.args -> string list = fun fdesc args ->
     match fdesc,args with
     | _, Args.(Ret _ | Ret_or_exc _ | Ret_ignore _ | Ret_ignore_or_exc _) -> []
-    | Fun.(Fn (State, fdesc_rem)), Args.(FnState args_rem) ->
-        "t"::show_args fdesc_rem args_rem
+    | Fun.(Fn (State, fdesc_rem)), Args.(FnState (index,args_rem)) ->
+        (Lin.Var.show index)::(show_args fdesc_rem args_rem)
     | Fun.(Fn ((GenDeconstr _ | Gen _ as ty), fdesc_rem)), Args.(Fn (value, args_rem)) ->
         (print ty value)::show_args fdesc_rem args_rem
     | Fun.(Fn (State, _)), Args.(Fn _)
@@ -228,8 +236,10 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
       | Fun.Ret_ignore_or_exc _ty -> Shrink.nil
       | Fun.Ret_ignore _ty -> Shrink.nil
       | Fun.(Fn (State, fdesc_rem)) ->
-          (function (Args.FnState args) ->
-             Iter.map (fun args -> Args.FnState args) (gen_shrinker_of_desc fdesc_rem args)
+          (function (Args.FnState (index,args)) ->
+            Iter.(map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args)
+                  <+>
+                  map (fun index -> Args.FnState (index,args)) (Lin.Var.shrink index))
                   | _ -> failwith "FnState: should not happen")
       | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
           (match arg_arb.shrink with
@@ -244,16 +254,16 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
                    (map (fun args -> Args.Fn (a,args)) (gen_shrinker_of_desc fdesc_rem args))
                             | _ -> failwith "Fn/Some: should not happen"))
 
-  let api =
+  let api gen_t_var =
     List.map (fun (wgt, Elem (name, fdesc, f)) ->
-        let rty = ret_type fdesc in
+        let print = gen_printer name fdesc in
+        let shrink = gen_shrinker_of_desc fdesc in
         let open QCheck.Gen in
-        (wgt, gen_args_of_desc fdesc >>= fun args ->
-         let print = gen_printer name fdesc in
-         let shrink = gen_shrinker_of_desc fdesc in
-         return (Cmd (name, args, rty, print, shrink, f)))) ApiSpec.api
+        (wgt, gen_args_of_desc fdesc gen_t_var >>= fun args ->
+         let opt_var, rty = ret_type fdesc in
+         return (opt_var, Cmd (name, args, rty, print, shrink, f)))) ApiSpec.api
 
-  let gen_cmd : cmd QCheck.Gen.t = QCheck.Gen.frequency api
+  let gen_cmd gen_t_var : ('a option * cmd) QCheck.Gen.t = QCheck.Gen.frequency (api gen_t_var)
 
   let show_cmd (Cmd (_,args,_,print,_,_)) = print args
 
@@ -273,7 +283,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
     | GenDeconstr (_, print, _) -> print value
 
   let rec apply_f
-    : type a r. a -> (a, r) Args.args -> t -> r = fun f args state ->
+    : type a r. a -> (a, r) Args.args -> t array -> Lin.Var.t option -> r = fun f args state opt_target ->
       match args with
       | Ret _ ->
           (* This happens only if there was a non-function value in the API,
@@ -291,24 +301,33 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
           (* This happens only if there was a non-function value in the API,
              which I'm not sure makes sense *)
           raise (Invalid_argument "apply_f")
-      | FnState (Ret _) ->
-          f state
-      | FnState (Ret_or_exc _) ->
-          begin
-            try Ok (f state)
-            with e -> Error e
-          end
-      | FnState (Ret_ignore _) ->
-          ignore (f state)
-      | FnState (Ret_ignore_or_exc _) ->
+      | FnState (index, Ret _) ->
+          f state.(index)
+      | FnState (index, Ret_or_exc _) ->
           begin
-            try Ok (ignore @@ f state)
+            try Ok (f state.(index))
             with e -> Error e
           end
-      | FnState (Fn _ as rem) ->
-          apply_f (f state) rem state
-      | FnState (FnState _ as rem) ->
-          apply_f (f state) rem state
+      | FnState (index, Ret_ignore ty) ->
+        (match ty,opt_target with
+         | State, Some tgt -> state.(tgt) <- (f state.(index))
+         | _               -> ignore (f state.(index)))
+      | FnState (index, Ret_ignore_or_exc ty) ->
+        (match ty,opt_target with
+         | State, Some tgt ->
+           begin
+             try Ok (state.(tgt) <- f state.(index))
+             with e -> Error e
+           end
+         | _ ->
+           begin
+             try Ok (ignore @@ f state.(index))
+             with e -> Error e
+           end)
+      | FnState (index, (Fn _ as rem)) ->
+          apply_f (f state.(index)) rem state opt_target
+      | FnState (index, (FnState _ as rem)) ->
+          apply_f (f state.(index)) rem state opt_target
       | Fn (arg, Ret _) ->
           f arg
       | Fn (arg, Ret_or_exc _) ->
@@ -324,13 +343,13 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
             with e -> Error e
           end
       | Fn (arg, (Fn _ as rem)) ->
-          apply_f (f arg) rem state
+          apply_f (f arg) rem state opt_target
       | Fn (arg, (FnState _ as rem)) ->
-          apply_f (f arg) rem state
+          apply_f (f arg) rem state opt_target
 
-  let run cmd state =
+  let run (opt_target,cmd) state =
     let Cmd (_, args, rty, _, _, f) = cmd in
-    Res (rty, apply_f f args state)
+    Res (rty, apply_f f args state opt_target)
 
 end
 
diff --git a/lib/lin_api.mli b/lib/lin_api.mli
index 0abb3cccb..3654e4f61 100644
--- a/lib/lin_api.mli
+++ b/lib/lin_api.mli
@@ -19,6 +19,15 @@ type noncombinable
 (** Type definition to denote that a described type cannot be composed with
     other combinators such as [list]. *)
 
+(** The (_,_,_,_) ty describes the type of type combinators.
+   These are accepted by the [@->], [returning], [returning_], [returning_or_exc], and [returning_or_exc_] combinators
+   The four type parameters:
+   - 1st: the type of the produced values
+   - 2nd: indicating whether the type is constructible (generatable) or deconstructible by equality testing
+   - 3rd: indicating the type of the underlying state
+   - 4th: indicating whether the type is combinable with other combinators, e.g., [list].
+          Note: [state]/[t] is currently [noncombinable].
+*)
 type (_, _, _, _) ty
 (** Type definition for type-describing combinators. *)
 
@@ -128,6 +137,7 @@ val list : ('a, 'c, 's, combinable) ty -> ('a list, 'c, 's, combinable) ty
     and have their elements generated by the [t] combinator.
     It is based on [QCheck.list]. *)
 
+(* FIXME: shouldn't be deconstructible? *)
 val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
 (** The [array] combinator represents the [array] type.
     The generated arrays from [array t] have a length resulting from [QCheck.Gen.nat]
@@ -174,27 +184,28 @@ end
 
 val returning :
   ('a, deconstructible, 'b, combinable) ty -> ('a, 'a, 'b) Fun.fn
-(** [returning t] represents a pure return type. *)
+(** [returning comb] indicates the return type [comb] to be compared to the corresponding sequential result.
+    For this reason [comb] has to be [deconstructible]. *)
 
 val returning_or_exc :
   ('a, deconstructible, 'b, combinable) ty ->
   ('a, ('a, exn) result, 'b) Fun.fn
-(** [returning_or_exc t] represents a return type of a function that may raise an exception. *)
+(** [returning_or_exc comb] indicates that the function may raise an exception and that the return type is [comb].
+    In either case the result is compared to the corresponding sequential result and hence [comb] has to be [deconstructible]. *)
 
 val returning_ : ('a, 'b, 'c, combinable) ty -> ('a, unit, 'c) Fun.fn
-(** [returning_ t] represents a return type that should be ignored. *)
+(** [returning comb] indicates the return type [comb] which is ignored. *)
 
 val returning_or_exc_ :
   ('a, 'b, 'c, combinable) ty -> ('a, (unit, exn) result, 'c) Fun.fn
-(** [returning_or_exc_ t] represents a return type that should be ignored of a function
-    that may raise an exception. *)
+(** [returning_or_exc comb] indicates that the function may raise an exception and that the return type is [comb].
+    In both cases the result is ignored. *)
 
 val ( @-> ) :
   ('a, constructible, 'b, 'c) ty ->
   ('d, 'e, 'b) Fun.fn -> ('a -> 'd, 'e, 'b) Fun.fn
-(** [at @-> rt] represents a function type expecting an argument [at]
-    and returning [rt]. *)
-
+(** [arg_typ @-> res_typ] indicates a function signature expecting [arg_typ] and returning [res_typ].
+    Note: eventually has to end in one of the [returning] combinators. *)
 
 (** {1 API description} *)
 

From 403d9145d15c8799de89e881a05a3f1bf58f06c7 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 15 Aug 2022 19:36:32 +0200
Subject: [PATCH 07/57] update Array tests to multiple ts

---
 src/array/dune             | 2 +-
 src/array/lin_tests_dsl.ml | 9 ++++++---
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/array/dune b/src/array/dune
index f05e0ae7e..aab13edd5 100644
--- a/src/array/dune
+++ b/src/array/dune
@@ -26,7 +26,7 @@
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/array/lin_tests_dsl.ml b/src/array/lin_tests_dsl.ml
index 92ba68326..efb7de3ef 100644
--- a/src/array/lin_tests_dsl.ml
+++ b/src/array/lin_tests_dsl.ml
@@ -5,7 +5,7 @@ module AConf =
 struct
   type t = char array
 
-  let array_size = 16
+  let array_size = 2
   let init () = Array.make array_size 'a'
   let cleanup _ = ()
 
@@ -16,10 +16,13 @@ struct
     [ val_ "Array.length"   Array.length   (t @-> returning int);
       val_ "Array.get"      Array.get      (t @-> int @-> returning_or_exc char);
       val_ "Array.set"      Array.set      (t @-> int @-> char @-> returning_or_exc unit);
-      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc (array char));
-      val_ "Array.copy"     Array.copy     (t @-> returning (array char));
+      val_ "Array.append"   Array.append   (t @-> t @-> returning_ t);
+      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc_ t);
+      val_ "Array.copy"     Array.copy     (t @-> returning_ t);
       val_ "Array.fill"     Array.fill     (t @-> int @-> int @-> char @-> returning_or_exc unit);
+      val_ "Array.blit"     Array.blit     (t @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
       val_ "Array.to_list"  Array.to_list  (t @-> returning (list char));
+      val_ "Array.of_list"  Array.of_list  (list char @-> returning_ t);
       val_ "Array.mem"      Array.mem      (char @-> t @-> returning bool);
       val_ "Array.sort"     (Array.sort Char.compare) (t @-> returning unit);
       val_ "Array.to_seq"   array_to_seq   (t @-> returning (seq char));

From 9ecbb37511b76a48c2ac4559e50b447469985357 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 15 Aug 2022 19:52:02 +0200
Subject: [PATCH 08/57] update Hashtbl tests with multiple ts support

---
 src/hashtbl/dune             | 2 +-
 src/hashtbl/lin_tests_dsl.ml | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/hashtbl/dune b/src/hashtbl/dune
index 27d9d13ba..2122421fe 100644
--- a/src/hashtbl/dune
+++ b/src/hashtbl/dune
@@ -26,7 +26,7 @@
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/hashtbl/lin_tests_dsl.ml b/src/hashtbl/lin_tests_dsl.ml
index 4eeff1bd1..bfa135e89 100644
--- a/src/hashtbl/lin_tests_dsl.ml
+++ b/src/hashtbl/lin_tests_dsl.ml
@@ -12,6 +12,7 @@ struct
   let int,char = nat_small,char_printable
   let api =
     [ val_ "Hashtbl.clear"    Hashtbl.clear    (t @-> returning unit);
+      val_ "Hashtbl.copy"     Hashtbl.copy     (t @-> returning_ t);
       val_ "Hashtbl.add"      Hashtbl.add      (t @-> char @-> int @-> returning unit);
       val_ "Hashtbl.remove"   Hashtbl.remove   (t @-> char @-> returning unit);
       val_ "Hashtbl.find"     Hashtbl.find     (t @-> char @-> returning_or_exc int);

From c51da9c1ec8422e94ba302e7ca2903e15da18d1a Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 11:47:44 +0200
Subject: [PATCH 09/57] update atomic tests to multiple ts

---
 src/atomic/dune             |  4 +--
 src/atomic/lin_tests.ml     | 58 ++++++++++++++++++++++++-------------
 src/atomic/lin_tests_dsl.ml |  4 ++-
 3 files changed, 43 insertions(+), 23 deletions(-)

diff --git a/src/atomic/dune b/src/atomic/dune
index 65566c1c2..6b6b9e28f 100644
--- a/src/atomic/dune
+++ b/src/atomic/dune
@@ -22,14 +22,14 @@
  (action (run ./%{deps} --verbose)))
 
 
-;; Linearizability tests of Atomic, utilizing ppx_deriving_qcheck
+;; Linearizability tests of Atomic
 
 (executable
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml
index 95e454552..bb2f29a40 100644
--- a/src/atomic/lin_tests.ml
+++ b/src/atomic/lin_tests.ml
@@ -6,44 +6,61 @@ open QCheck
 module AConf =
 struct
   type t = int Atomic.t
-
+  open Lin
   type cmd =
-    | Get
-    | Set of int'
-    | Exchange of int'
-    | Compare_and_set of int' * int'
-    | Fetch_and_add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
+    | Make of int
+    | Get of Var.t
+    | Set of Var.t * int
+    | Exchange of Var.t * int
+    | Compare_and_set of Var.t * int * int
+    | Fetch_and_add of Var.t * int
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun i ->     (Some (Var.next()), Make i)) gen_int;
+        map  (fun t ->     (None, Get t)) gen_var;
+        map2 (fun t i ->   (None, Set (t,i))) gen_var gen_int;
+        map2 (fun t i ->   (None, Exchange (t,i))) gen_var gen_int;
+        map3 (fun t i j -> (None, Compare_and_set (t,i,j))) gen_var gen_int gen_int;
+        map2 (fun t i ->   (None, Fetch_and_add (t,i))) gen_var gen_int;
+        map  (fun t ->     (None, Incr t)) gen_var;
+        map  (fun t ->     (None, Decr t)) gen_var;
+      ])
 
   let shrink_cmd = Shrink.nil
 
   type res =
+    | RMake of unit
     | RGet of int
-    | RSet
+    | RSet of unit
     | RExchange of int
     | RFetch_and_add of int
     | RCompare_and_set of bool
-    | RIncr
-    | RDecr [@@deriving show { with_path = false }, eq]
+    | RIncr of unit
+    | RDecr of unit [@@deriving show { with_path = false }, eq]
 
   let init () = Atomic.make 0
 
   let run c r = match c with
-    | Get                      -> RGet (Atomic.get r)
-    | Set i                    -> (Atomic.set r i; RSet)
-    | Exchange i               -> RExchange (Atomic.exchange r i)
-    | Fetch_and_add i          -> RFetch_and_add (Atomic.fetch_and_add r i)
-    | Compare_and_set (seen,v) -> RCompare_and_set (Atomic.compare_and_set r seen v)
-    | Incr                     -> (Atomic.incr r; RIncr)
-    | Decr                     -> (Atomic.decr r; RDecr)
+    | Some t, Make i                   -> RMake (r.(t) <- Atomic.make i)
+    | None, Get t                      -> RGet (Atomic.get r.(t))
+    | None, Set (t,i)                  -> RSet (Atomic.set r.(t) i)
+    | None, Exchange (t,i)             -> RExchange (Atomic.exchange r.(t) i)
+    | None, Fetch_and_add (t,i)        -> RFetch_and_add (Atomic.fetch_and_add r.(t) i)
+    | None, Compare_and_set (t,seen,v) -> RCompare_and_set (Atomic.compare_and_set r.(t) seen v)
+    | None, Incr t                     -> RIncr (Atomic.incr r.(t))
+    | None, Decr t                     -> RDecr (Atomic.decr r.(t))
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
 
 module AT = Lin.Make(AConf)
 
+(*
 (** A variant of the above with 3 Atomics *)
 module A3Conf =
 struct
@@ -86,10 +103,11 @@ struct
 end
 
 module A3T = Lin.Make(A3Conf)
+*)
 ;;
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main [
   AT.lin_test     `Domain ~count:1000 ~name:"Lin Atomic test with Domain";
-  A3T.lin_test    `Domain ~count:1000 ~name:"Lin Atomic3 test with Domain";
+(* A3T.lin_test    `Domain ~count:1000 ~name:"Lin Atomic3 test with Domain"; *)
 ]
diff --git a/src/atomic/lin_tests_dsl.ml b/src/atomic/lin_tests_dsl.ml
index 86584456b..8e4abe9bc 100644
--- a/src/atomic/lin_tests_dsl.ml
+++ b/src/atomic/lin_tests_dsl.ml
@@ -3,8 +3,10 @@ module Atomic_spec : Lin_api.ApiSpec = struct
   type t = int Atomic.t
   let init () = Atomic.make 0
   let cleanup _ = ()
+  let int = int_small
   let api =
-    [ val_ "Atomic.get"             Atomic.get             (t @-> returning int);
+    [ val_ "Atomic.make"            Atomic.make            (int @-> returning_ t);
+      val_ "Atomic.get"             Atomic.get             (t @-> returning int);
       val_ "Atomic.set"             Atomic.set             (t @-> int @-> returning unit);
       val_ "Atomic.exchange"        Atomic.exchange        (t @-> int @-> returning int);
       val_ "Atomic.fetch_and_add"   Atomic.fetch_and_add   (t @-> int @-> returning int);

From f3c7786b376795b65216c2bcea5195f3998a4286 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 12:38:30 +0200
Subject: [PATCH 10/57] update Bytes tests to multiple ts

---
 src/bytes/lin_tests_dsl.ml | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index fabb37278..c69f2efa0 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -3,16 +3,28 @@
 (* ********************************************************************** *)
 module BConf = struct
   type t = Bytes.t
-  let init () = Stdlib.Bytes.make 42 '0'
+  let init () = Bytes.make 8 '0'
   let cleanup _ = ()
 
   open Lin_api
+  let int = nat_small
+(*let int = int_bound 10*)
   let api = [
+    val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
+    val_ "Bytes.set"         Bytes.set         (t @-> int @-> char @-> returning_or_exc unit);
+ (* val_ "Bytes.create"      Bytes.create      (int @-> returning_or_exc_ t); *) (* result contains arbitrary bytes, hence non-det. output! *)
+    val_ "Bytes.make"        Bytes.make        (int @-> char @-> returning_or_exc_ t);
+ (* val_ "Bytes.empty"       Bytes.empty       (returning_ t); *)
+    val_ "Bytes.copy"        Bytes.copy        (t @-> returning_ t);
+    val_ "Bytes.of_string"   Bytes.of_string   (string @-> returning_ t);
+    val_ "Bytes.to_string"   Bytes.to_string   (t @-> returning string);
     val_ "Bytes.sub_string"  Bytes.sub_string  (t @-> int @-> int @-> returning_or_exc string);
-    val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
     val_ "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
+    val_ "Bytes.trim"        Bytes.trim        (t @-> returning_ t);
+    val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t);
+    val_ "Bytes.index"       Bytes.index       (t @-> char @-> returning_or_exc int);
     val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int)]
 end
 

From 5c699a17c9ba3d08798d4c01cae468b6e58ed507 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 13:42:41 +0200
Subject: [PATCH 11/57] update internal tests to multiple ts

---
 src/internal/cleanup_lin.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/internal/cleanup_lin.ml b/src/internal/cleanup_lin.ml
index 646d248cd..c0d354542 100644
--- a/src/internal/cleanup_lin.ml
+++ b/src/internal/cleanup_lin.ml
@@ -8,18 +8,18 @@ struct
   type status = Inited | Cleaned
 
   type cmd =
-    | Get
-    | Set of int
-    | Add of int [@@deriving show { with_path = false }]
+    | Get of Lin.Var.t
+    | Set of Lin.Var.t * int
+    | Add of Lin.Var.t * int [@@deriving show { with_path = false }]
 
   type t = (status ref) * (int ref)
 
-  let gen_cmd =
+  let gen_cmd gen_var =
     let int_gen = Gen.nat in
       (Gen.oneof
-         [Gen.return Get;
-	  Gen.map (fun i -> Set i) int_gen;
-	  Gen.map (fun i -> Add i) int_gen;
+         [Gen.map  (fun t ->   None, Get t) gen_var;
+	  Gen.map2 (fun t i -> None, Set (t,i)) gen_var int_gen;
+	  Gen.map2 (fun t i -> None, Add (t,i)) gen_var int_gen;
          ])
 
   let shrink_cmd = Shrink.nil
@@ -33,10 +33,11 @@ struct
 
   type res = RGet of int | RSet | RAdd [@@deriving show { with_path = false }, eq]
 
-  let run c (_,r) = match c with
-    | Get   -> RGet (!r)
-    | Set i -> (r:=i; RSet)
-    | Add i -> (let old = !r in r := i + old; RAdd) (* buggy: not atomic *)
+  let run c s = match c with
+    | None, Get t     -> RGet (!(snd s.(t)))
+    | None, Set (t,i) -> ((snd s.(t)):=i; RSet)
+    | None, Add (t,i) -> (let old = !(snd (s.(t))) in snd (s.(t)) := i + old; RAdd) (* buggy: not atomic *)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 module RT = Lin.Make(RConf)

From 3b63ae417d5419db75bbb3f70492e4f4170524c4 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 14:08:09 +0200
Subject: [PATCH 12/57] update kcas tests to multiple ts

---
 src/kcas/dune         |   2 +-
 src/kcas/lin_tests.ml | 105 +++++++++++++++++++++++++++---------------
 2 files changed, 68 insertions(+), 39 deletions(-)

diff --git a/src/kcas/dune b/src/kcas/dune
index 7bd96018a..097f463ce 100644
--- a/src/kcas/dune
+++ b/src/kcas/dune
@@ -11,7 +11,7 @@
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin kcas)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; disable kcas test for now
 ; (rule
diff --git a/src/kcas/lin_tests.ml b/src/kcas/lin_tests.ml
index 6a9dad2a5..09447a946 100644
--- a/src/kcas/lin_tests.ml
+++ b/src/kcas/lin_tests.ml
@@ -7,18 +7,32 @@ module KConf =
 struct
   type t = int Kcas.ref
 
+  open Lin
   (* missing: equal, is_on_ref, kCAS -- mk_cas, commit (already tested as [set] *)
   type cmd =
-    | Get
-    | Set of int'
-    | Cas of int' * int'
-    | TryMapNone
-    (*| TryMapSome*) (* Seq,exec cannot fail - hence not linearizable with [try_map] *)
-    | MapNone
-    | MapSome
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = (int [@gen Gen.nat])
+    | Get of Var.t
+    | Set of Var.t * int
+    | Cas of Var.t * int * int
+    | TryMapNone of Var.t
+    (*| TryMapSome of Var.t *) (* Seq,exec cannot fail - hence not linearizable with [try_map] *)
+    | MapNone of Var.t
+    | MapSome of Var.t
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t     -> None, Get t) gen_var;
+        map2 (fun t i   -> None, Set (t,i)) gen_var gen_int;
+        map3 (fun t i j -> None, Cas (t,i,j)) gen_var gen_int gen_int;
+        map  (fun t     -> None, TryMapNone t) gen_var;
+      (*map  (fun t     -> None, TryMapSone t) gen_var;*)
+        map  (fun t     -> None, MapNone t) gen_var;
+        map  (fun t     -> None, MapSome t) gen_var;
+        map  (fun t     -> None, Incr t) gen_var;
+        map  (fun t     -> None, Decr t) gen_var;
+      ])
 
   let shrink_cmd = Shrink.nil
 
@@ -41,15 +55,16 @@ struct
   let init () = Kcas.ref 0
 
   let run c r = match c with
-    | Get        -> RGet (Kcas.get r)
-    | Set i      -> (Kcas.set r i; RSet)
-    | Cas (i,j)  -> RCas (Kcas.cas r i j)
-    | TryMapNone -> RTryMapNone (Kcas.try_map r (fun _ -> None))
-    (*| TryMapSome -> RTryMapSome (Kcas.try_map r (fun i -> Some i))*)
-    | MapNone    -> RMapNone (Kcas.map r (fun _ -> None))
-    | MapSome    -> RMapSome (Kcas.map r (fun i -> Some i))
-    | Incr       -> (Kcas.incr r; RIncr)
-    | Decr       -> (Kcas.decr r; RDecr)
+    | None, Get t        -> RGet (Kcas.get r.(t))
+    | None, Set (t,i)    -> (Kcas.set r.(t) i; RSet)
+    | None, Cas (t,i,j)  -> RCas (Kcas.cas r.(t) i j)
+    | None, TryMapNone t -> RTryMapNone (Kcas.try_map r.(t) (fun _ -> None))
+  (*| None, TryMapSome t -> RTryMapSome (Kcas.try_map r.(t) (fun i -> Some i))*)
+    | None, MapNone t    -> RMapNone (Kcas.map r.(t) (fun _ -> None))
+    | None, MapSome t    -> RMapSome (Kcas.map r.(t) (fun i -> Some i))
+    | None, Incr t       -> (Kcas.incr r.(t); RIncr)
+    | None, Decr t       -> (Kcas.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   let cleanup _ = ()
 end
 
@@ -63,17 +78,30 @@ module KW1Conf =
 struct
   type t = int Kcas.W1.ref
 
+  open Lin
   type cmd =
-    | Get
-    | Set of int'
-    | Cas of int' * int'
-    | TryMapNone
-    (*| TryMapSome*) (* Seq,exec cannot fail - hence not linearizable with [try_map] *)
-    | MapNone
-    | MapSome
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = (int [@gen Gen.nat])
+    | Get of Var.t
+    | Set of Var.t * int
+    | Cas of Var.t * int * int
+    | TryMapNone of Var.t
+  (*| TryMapSome of Var.t *) (* Seq,exec cannot fail - hence not linearizable with [try_map] *)
+    | MapNone of Var.t
+    | MapSome of Var.t
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> None,Get t) gen_var;
+        map2 (fun t i -> None,Set (t,i)) gen_var gen_int;
+        map3 (fun t i j -> None,Cas (t,i,j)) gen_var gen_int gen_int;
+        map  (fun t -> None,TryMapNone t) gen_var;
+      (*map  (fun t -> None,TryMapSome t) gen_var;*)
+        map  (fun t -> None,MapNone t) gen_var;
+        map  (fun t -> None,MapSome t) gen_var;
+        map  (fun t -> None,Incr t) gen_var;
+        map  (fun t -> None,Decr t) gen_var;
+      ])
 
   let shrink_cmd = Shrink.nil
 
@@ -96,15 +124,16 @@ struct
   let init () = Kcas.W1.ref 0
 
   let run c r = match c with
-    | Get        -> RGet (Kcas.W1.get r)
-    | Set i      -> (Kcas.W1.set r i; RSet)
-    | Cas (i,j)  -> RCas (Kcas.W1.cas r i j)
-    | TryMapNone -> RTryMapNone (Kcas.W1.try_map r (fun _ -> None))
-    (*| TryMapSome -> RTryMapSome (Kcas.W1.try_map r (fun i -> Some i))*)
-    | MapNone    -> RMapNone (Kcas.W1.map r (fun _ -> None))
-    | MapSome    -> RMapSome (Kcas.W1.map r (fun i -> Some i))
-    | Incr       -> (Kcas.W1.incr r; RIncr)
-    | Decr       -> (Kcas.W1.decr r; RDecr)
+    | None,Get t        -> RGet (Kcas.W1.get r.(t))
+    | None,Set (t,i)    -> (Kcas.W1.set r.(t) i; RSet)
+    | None,Cas (t,i,j)  -> RCas (Kcas.W1.cas r.(t) i j)
+    | None,TryMapNone t -> RTryMapNone (Kcas.W1.try_map r.(t) (fun _ -> None))
+  (*| None,TryMapSome t -> RTryMapSome (Kcas.W1.try_map r.(t) (fun i -> Some i))*)
+    | None,MapNone t    -> RMapNone (Kcas.W1.map r.(t) (fun _ -> None))
+    | None,MapSome t    -> RMapSome (Kcas.W1.map r.(t) (fun i -> Some i))
+    | None,Incr t       -> (Kcas.W1.incr r.(t); RIncr)
+    | None,Decr t       -> (Kcas.W1.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   let cleanup _ = ()
 end
 

From af1de5a3b1812db77042d10b76bb7c38b4e1ec23 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 14:34:09 +0200
Subject: [PATCH 13/57] update Lazy tests to multiple ts

---
 src/lazy/dune         |  2 +-
 src/lazy/lin_tests.ml | 39 +++++++++++++++++++++++++--------------
 2 files changed, 26 insertions(+), 15 deletions(-)

diff --git a/src/lazy/dune b/src/lazy/dune
index d209cb158..9c800fa4a 100644
--- a/src/lazy/dune
+++ b/src/lazy/dune
@@ -22,7 +22,7 @@
  (name lin_tests)
  (modules lin_tests)
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml
index 12a7f574c..fea71a263 100644
--- a/src/lazy/lin_tests.ml
+++ b/src/lazy/lin_tests.ml
@@ -1,5 +1,4 @@
 open QCheck
-open Lin
 
 (** parallel linearization tests of Lazy *)
 
@@ -33,14 +32,25 @@ module Lazy :
 
 module LBase =
 struct
+  open Lin
   type cmd =
-    | Force
-    | Force_val
-    | Is_val
-    | Map of int_fun
-    | Map_val of int_fun [@@deriving qcheck, show { with_path = false }]
-  and int_fun = (int -> int) fun_ [@gen (fun1 Observable.int small_nat).gen][@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+    | Force of Var.t
+    | Force_val of Var.t
+    | Is_val of Var.t
+    | Map of Var.t * int_fun
+    | Map_val of Var.t * int_fun [@@deriving show { with_path = false }]
+  and int_fun = (int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+
+  let int_fun_gen = (fun1 Observable.int small_nat).gen
 
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> None,Force t) gen_var;
+        map  (fun t -> None,Force_val t) gen_var;
+        map  (fun t -> None,Is_val t) gen_var;
+        map2 (fun t f -> None,Map (t,f)) gen_var int_fun_gen;
+        map2 (fun t f -> None,Map_val (t,f)) gen_var int_fun_gen;
+      ])
   (*
   let shrink_cmd c = match c with
     | Force
@@ -65,13 +75,14 @@ struct
     | RMap_val of (int,exn) result [@@deriving show { with_path = false }, eq]
 
   let run c l = match c with
-    | Force               -> RForce (Util.protect Lazy.force l)
-    | Force_val           -> RForce_val (Util.protect Lazy.force_val l)
-    | Is_val              -> RIs_val (Lazy.is_val l)
-    | Map (Fun (_,f))     -> RMap (try Ok (Lazy.force (Lazy.map f l))
-                                   with exn -> Error exn) (*we force the "new lazy"*)
-    | Map_val (Fun (_,f)) -> RMap_val (try Ok (Lazy.force (Lazy.map_val f l))
-                                       with exn -> Error exn) (*we force the "new lazy"*)
+    | None,Force t               -> RForce (Util.protect Lazy.force l.(t))
+    | None,Force_val t           -> RForce_val (Util.protect Lazy.force_val l.(t))
+    | None,Is_val t              -> RIs_val (Lazy.is_val l.(t))
+    | None,Map (t,Fun (_,f))     -> RMap (try Ok (Lazy.force (Lazy.map f l.(t)))
+                                          with exn -> Error exn) (*we force the "new lazy"*)
+    | None,Map_val (t,Fun (_,f)) -> RMap_val (try Ok (Lazy.force (Lazy.map_val f l.(t)))
+                                              with exn -> Error exn) (*we force the "new lazy"*)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 

From 96f4adce2074d62fe5461b467d49ffed084c90eb Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 15:17:35 +0200
Subject: [PATCH 14/57] update src/neg_tests to multiple ts

---
 src/neg_tests/dune                |   2 +-
 src/neg_tests/lin_tests_common.ml | 107 +++++++++++++++++++-----------
 2 files changed, 70 insertions(+), 39 deletions(-)

diff --git a/src/neg_tests/dune b/src/neg_tests/dune
index fd805dec9..1b7098ceb 100644
--- a/src/neg_tests/dune
+++ b/src/neg_tests/dune
@@ -52,7 +52,7 @@
  (name lin_tests_common)
  (modules lin_tests_common)
  (libraries lin CList)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 (executables
  (names domain_lin_tests_dsl thread_lin_tests_dsl)
diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml
index d0a47904c..162d7ace3 100644
--- a/src/neg_tests/lin_tests_common.ml
+++ b/src/neg_tests/lin_tests_common.ml
@@ -24,66 +24,90 @@ module Sut_int64 =
 end
 
 module RConf_int = struct
+  open Lin
+
   type t = int ref
 
   type cmd =
-    | Get
-    | Set of int'
-    | Add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
+    | Get of Var.t
+    | Set of Var.t * int
+    | Add of Var.t * int
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof[
+        map  (fun t -> None,Get t) gen_var;
+        map2 (fun t i -> None,Set (t,i)) gen_var gen_int;
+        map2 (fun t i -> None,Add (t,i)) gen_var gen_int;
+        map  (fun t -> None,Incr t) gen_var;
+        map  (fun t -> None,Decr t) gen_var;
+      ])
 
   let shrink_cmd c = match c with
-    | Get
-    | Incr
-    | Decr -> Iter.empty
-    | Set i -> Iter.map (fun i -> Set i) (Shrink.int i)
-    | Add i -> Iter.map (fun i -> Add i) (Shrink.int i)
+    | Get _
+    | Incr _
+    | Decr _ -> Iter.empty
+    | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int i)
+    | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
 
   type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int.init ()
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int.get r)
-    | Set i -> (Sut_int.set r i; RSet)
-    | Add i -> (Sut_int.add r i; RAdd)
-    | Incr  -> (Sut_int.incr r; RIncr)
-    | Decr  -> (Sut_int.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int.get r.(t))
+    | None,Set (t,i) -> (Sut_int.set r.(t) i; RSet)
+    | None,Add (t,i) -> (Sut_int.add r.(t) i; RAdd)
+    | None,Incr t    -> (Sut_int.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
 
 
 module RConf_int64 = struct
+  open Lin
+
   type t = int64 ref
 
   type cmd =
-    | Get
-    | Set of int'
-    | Add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int64 [@gen Gen.(map Int64.of_int nat)]
+    | Get of Var.t
+    | Set of Var.t * int64
+    | Add of Var.t * int64
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int64 = Gen.(map Int64.of_int nat)
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> None,Get t) gen_var;
+        map2 (fun t i -> None,Set (t,i)) gen_var gen_int64;
+        map2 (fun t i -> None,Add (t,i)) gen_var gen_int64;
+        map  (fun t -> None,Incr t) gen_var;
+        map  (fun t -> None,Decr t) gen_var;
+      ])
 
   let shrink_cmd c = match c with
-    | Get
-    | Incr
-    | Decr -> Iter.empty
-    | Set i -> Iter.map (fun i -> Set i) (Shrink.int64 i)
-    | Add i -> Iter.map (fun i -> Add i) (Shrink.int64 i)
+    | Get _
+    | Incr _
+    | Decr _ -> Iter.empty
+    | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int64 i)
+    | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
 
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int64.init ()
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int64.get r)
-    | Set i -> (Sut_int64.set r i; RSet)
-    | Add i -> (Sut_int64.add r i; RAdd)
-    | Incr  -> (Sut_int64.incr r; RIncr)
-    | Decr  -> (Sut_int64.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int64.get r.(t))
+    | None,Set (t,i) -> (Sut_int64.set r.(t) i; RSet)
+    | None,Add (t,i) -> (Sut_int64.add r.(t) i; RAdd)
+    | None,Incr t    -> (Sut_int64.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int64.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
@@ -109,20 +133,27 @@ struct
   let pp_int' fmt t = Format.fprintf fmt "%s" (T.to_string t)
 
   type cmd =
-    | Add_node of int'
-    | Member of int' [@@deriving qcheck, show { with_path = false }]
+    | Add_node of Lin.Var.t * int'
+    | Member of Lin.Var.t * int' [@@deriving show { with_path = false }]
+
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map2 (fun t i -> None,Add_node (t,i)) gen_var gen_int';
+        map2 (fun t i -> None,Member (t,i)) gen_var gen_int';
+      ])
 
   let shrink_cmd c = match c with
-    | Add_node i -> Iter.map (fun i -> Add_node i) (T.shrink i)
-    | Member i -> Iter.map (fun i -> Member i) (T.shrink i)
+    | Add_node (t,i) -> Iter.map (fun i -> Add_node (t,i)) (T.shrink i)
+    | Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
 
   type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
 
   let init () = CList.list_init T.zero
 
   let run c r = match c with
-    | Add_node i -> RAdd_node (CList.add_node r i)
-    | Member i   -> RMember (CList.member r i)
+    | None,Add_node (t,i) -> RAdd_node (CList.add_node r.(t) i)
+    | None,Member (t,i)   -> RMember (CList.member r.(t) i)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end

From 1e1cdf569d69740583f31b562dd43ce01e079422 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 15:31:22 +0200
Subject: [PATCH 15/57] update Queue tests to multiple ts

---
 src/queue/dune         |   2 +-
 src/queue/lin_tests.ml | 150 +++++++++++++++++++++++------------------
 2 files changed, 84 insertions(+), 68 deletions(-)

diff --git a/src/queue/dune b/src/queue/dune
index 8b2daf773..c5e92792e 100644
--- a/src/queue/dune
+++ b/src/queue/dune
@@ -23,7 +23,7 @@
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml
index 7af3b8960..88e409b43 100644
--- a/src/queue/lin_tests.ml
+++ b/src/queue/lin_tests.ml
@@ -4,35 +4,48 @@ open Lin
 module Spec =
   struct
     type t = int Queue.t
-    let m = Mutex.create ()
 
     type cmd =
-      | Add of int'
-      | Take
-      | Take_opt
-      | Peek
-      | Peek_opt
-      | Clear
-      | Is_empty
-      | Fold of fct * int'
-      | Length [@@deriving qcheck, show { with_path = false }]
-    and int' = int [@gen Gen.nat]
-    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)] [@gen (fun2 Observable.int Observable.int small_int).gen]
+      | Add of Var.t * int
+      | Take of Var.t
+      | Take_opt of Var.t
+      | Peek of Var.t
+      | Peek_opt of Var.t
+      | Clear of Var.t
+      | Is_empty of Var.t
+      | Fold of Var.t * fct * int
+      | Length of Var.t [@@deriving show { with_path = false }]
+    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+
+    let gen_int = Gen.nat
+    let gen_fct = (fun2 Observable.int Observable.int small_int).gen
+    let gen_cmd gen_var =
+      Gen.(oneof [
+          map2 (fun t i -> None,Add (t,i)) gen_var gen_int;
+          map  (fun t -> None, Take t) gen_var;
+          map  (fun t -> None, Take_opt t) gen_var;
+          map  (fun t -> None, Peek t) gen_var;
+          map  (fun t -> None, Peek_opt t) gen_var;
+          map  (fun t -> None, Clear t) gen_var;
+          map  (fun t -> None, Is_empty t) gen_var;
+          map3 (fun t f i -> None,Fold (t,f,i)) gen_var gen_fct gen_int;
+          map  (fun t -> None, Length t) gen_var;
+        ])
 
     let shrink_cmd c = match c with
-      | Take
-      | Take_opt
-      | Peek
-      | Peek_opt
-      | Clear
-      | Is_empty
-      | Length -> Iter.empty
-      | Add i -> Iter.map (fun i -> Add i) (Shrink.int i)
-      | Fold (f,i) ->
+      | Take _
+      | Take_opt _
+      | Peek _
+      | Peek_opt _
+      | Clear _
+      | Is_empty _
+      | Length _ -> Iter.empty
+      | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
+      | Fold (t,f,i) ->
           Iter.(
-            (map (fun f -> Fold (f,i)) (Fn.shrink f))
+            (map (fun f -> Fold (t,f,i)) (Fn.shrink f))
             <+>
-            (map (fun i -> Fold (f,i)) (Shrink.int i)))
+            (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
     type res =
       | RAdd
@@ -53,56 +66,59 @@ module QConf =
   struct
     include Spec
     let run c q = match c with
-      | Add i       -> Queue.add i q; RAdd
-      | Take        -> RTake (Util.protect Queue.take q)
-      | Take_opt    -> RTake_opt (Queue.take_opt q)
-      | Peek        -> RPeek (Util.protect Queue.peek q)
-      | Peek_opt    -> RPeek_opt (Queue.peek_opt q)
-      | Length      -> RLength (Queue.length q)
-      | Is_empty    -> RIs_empty (Queue.is_empty q)
-      | Fold (f, a) -> RFold (Queue.fold (Fn.apply f) a q)
-      | Clear       -> Queue.clear q; RClear
+      | None,Add (t,i)    -> Queue.add i q.(t); RAdd
+      | None,Take t       -> RTake (Util.protect Queue.take q.(t))
+      | None,Take_opt t   -> RTake_opt (Queue.take_opt q.(t))
+      | None,Peek t       -> RPeek (Util.protect Queue.peek q.(t))
+      | None,Peek_opt t   -> RPeek_opt (Queue.peek_opt q.(t))
+      | None,Length t     -> RLength (Queue.length q.(t))
+      | None,Is_empty t   -> RIs_empty (Queue.is_empty q.(t))
+      | None,Fold (t,f,a) -> RFold (Queue.fold (Fn.apply f) a q.(t))
+      | None,Clear t      -> Queue.clear q.(t); RClear
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
    end
 
 module QMutexConf =
   struct
     include Spec
+    let m = Mutex.create ()
     let run c q = match c with
-      | Add i       -> Mutex.lock m;
-                       Queue.add i q;
-                       Mutex.unlock m; RAdd
-      | Take        -> Mutex.lock m;
-                       let r = Util.protect Queue.take q in
-                       Mutex.unlock m;
-                       RTake r
-      | Take_opt    -> Mutex.lock m;
-                       let r = Queue.take_opt q in
-                       Mutex.unlock m;
-                       RTake_opt r
-      | Peek        -> Mutex.lock m;
-                       let r = Util.protect Queue.peek q in
-                       Mutex.unlock m;
-                       RPeek r
-      | Peek_opt    -> Mutex.lock m;
-                       let r = Queue.peek_opt q in
-                       Mutex.unlock m;
-                       RPeek_opt r
-      | Length      -> Mutex.lock m;
-                       let l = Queue.length q in
-                       Mutex.unlock m;
-                       RLength l
-      | Is_empty    -> Mutex.lock m;
-                       let b = Queue.is_empty q in
-                       Mutex.unlock m;
-                       RIs_empty b
-      | Fold (f, a) -> Mutex.lock m;
-                       let r = (Queue.fold (Fn.apply f) a q)  in
-                       Mutex.unlock m;
-                       RFold r
-      | Clear       -> Mutex.lock m;
-                       Queue.clear q;
-                       Mutex.unlock m;
-                       RClear
+      | None,Add (t,i)    -> Mutex.lock m;
+                             Queue.add i q.(t);
+                             Mutex.unlock m; RAdd
+      | None,Take t       -> Mutex.lock m;
+                             let r = Util.protect Queue.take q.(t) in
+                             Mutex.unlock m;
+                             RTake r
+      | None,Take_opt t   -> Mutex.lock m;
+                             let r = Queue.take_opt q.(t) in
+                             Mutex.unlock m;
+                             RTake_opt r
+      | None,Peek t       -> Mutex.lock m;
+                             let r = Util.protect Queue.peek q.(t) in
+                             Mutex.unlock m;
+                             RPeek r
+      | None,Peek_opt t   -> Mutex.lock m;
+                             let r = Queue.peek_opt q.(t) in
+                             Mutex.unlock m;
+                             RPeek_opt r
+      | None,Length t     -> Mutex.lock m;
+                             let l = Queue.length q.(t) in
+                             Mutex.unlock m;
+                             RLength l
+      | None,Is_empty t   -> Mutex.lock m;
+                             let b = Queue.is_empty q.(t) in
+                             Mutex.unlock m;
+                             RIs_empty b
+      | None,Fold (t,f,a) -> Mutex.lock m;
+                             let r = (Queue.fold (Fn.apply f) a q.(t))  in
+                             Mutex.unlock m;
+                             RFold r
+      | None,Clear t      -> Mutex.lock m;
+                             Queue.clear q.(t);
+                             Mutex.unlock m;
+                             RClear
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 module QMT = Lin.Make(QMutexConf)

From f01d59915e67dee9bca8600807a6b64e3e5426b3 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 15:59:45 +0200
Subject: [PATCH 16/57] update Stack tests to multiple ts

---
 src/stack/dune         |   2 +-
 src/stack/lin_tests.ml | 151 +++++++++++++++++++++++------------------
 2 files changed, 85 insertions(+), 68 deletions(-)

diff --git a/src/stack/dune b/src/stack/dune
index d32e1d888..a81fa388d 100644
--- a/src/stack/dune
+++ b/src/stack/dune
@@ -23,7 +23,7 @@
  (modules lin_tests)
  (flags (:standard -w -27))
  (libraries lin)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq)))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq)))
 
 ; (rule
 ;  (alias runtest)
diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml
index eb96db5e9..211043098 100644
--- a/src/stack/lin_tests.ml
+++ b/src/stack/lin_tests.ml
@@ -4,35 +4,49 @@ open Lin
 module Spec =
   struct
     type t = int Stack.t
-    let m = Mutex.create ()
 
     type cmd =
-      | Push of int'
-      | Pop
-      | Pop_opt
-      | Top
-      | Top_opt
-      | Clear
-      | Is_empty
-      | Fold of fct * int'
-      | Length [@@deriving qcheck, show { with_path = false }]
-    and int' = int [@gen Gen.nat]
-    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)] [@gen (fun2 Observable.int Observable.int small_int).gen]
+      | Push of Var.t * int
+      | Pop of Var.t
+      | Pop_opt of Var.t
+      | Top of Var.t
+      | Top_opt of Var.t
+      | Clear of Var.t
+      | Is_empty of Var.t
+      | Fold of Var.t * fct * int
+      | Length of Var.t [@@deriving show { with_path = false }]
+    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+
+    let gen_int = Gen.nat
+    let gen_fct = (fun2 Observable.int Observable.int small_int).gen
+
+    let gen_cmd gen_var =
+      Gen.(oneof [
+          map2 (fun t i -> None,Push (t,i)) gen_var gen_int;
+          map  (fun t -> None, Pop t) gen_var;
+          map  (fun t -> None, Pop_opt t) gen_var;
+          map  (fun t -> None, Top t) gen_var;
+          map  (fun t -> None, Top_opt t) gen_var;
+          map  (fun t -> None, Clear t) gen_var;
+          map  (fun t -> None, Is_empty t) gen_var;
+          map3 (fun t f i -> None,Fold (t,f,i)) gen_var gen_fct gen_int;
+          map  (fun t -> None, Length t) gen_var;
+        ])
 
     let shrink_cmd c = match c with
-      | Pop
-      | Pop_opt
-      | Top
-      | Top_opt
-      | Clear
-      | Is_empty
-      | Length -> Iter.empty
-      | Push i -> Iter.map (fun i -> Push i) (Shrink.int i)
-      | Fold (f,i) ->
+      | Pop _
+      | Pop_opt _
+      | Top _
+      | Top_opt _
+      | Clear _
+      | Is_empty _
+      | Length _ -> Iter.empty
+      | Push (t,i) -> Iter.map (fun i -> Push (t,i)) (Shrink.int i)
+      | Fold (t,f,i) ->
           Iter.(
-            (map (fun f -> Fold (f,i)) (Fn.shrink f))
+            (map (fun f -> Fold (t,f,i)) (Fn.shrink f))
             <+>
-            (map (fun i -> Fold (f,i)) (Shrink.int i)))
+            (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
     type res =
       | RPush
@@ -53,56 +67,59 @@ module SConf =
   struct
     include Spec
     let run c s = match c with
-      | Push i      -> Stack.push i s; RPush
-      | Pop         -> RPop (Util.protect Stack.pop s)
-      | Pop_opt     -> RPop_opt (Stack.pop_opt s)
-      | Top         -> RTop (Util.protect Stack.top s)
-      | Top_opt     -> RTop_opt (Stack.top_opt s)
-      | Clear       -> Stack.clear s; RClear
-      | Is_empty    -> RIs_empty (Stack.is_empty s)
-      | Fold (f, a) -> RFold (Stack.fold (Fn.apply f) a s)
-      | Length      -> RLength (Stack.length s)
+      | None,Push (t,i)   -> Stack.push i s.(t); RPush
+      | None,Pop t        -> RPop (Util.protect Stack.pop s.(t))
+      | None,Pop_opt t    -> RPop_opt (Stack.pop_opt s.(t))
+      | None,Top t        -> RTop (Util.protect Stack.top s.(t))
+      | None,Top_opt t    -> RTop_opt (Stack.top_opt s.(t))
+      | None,Clear t      -> Stack.clear s.(t); RClear
+      | None,Is_empty t   -> RIs_empty (Stack.is_empty s.(t))
+      | None,Fold (t,f,a) -> RFold (Stack.fold (Fn.apply f) a s.(t))
+      | None,Length t     -> RLength (Stack.length s.(t))
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   end
 
 module SMutexConf =
   struct
     include Spec
+    let m = Mutex.create ()
     let run c s = match c with
-      | Push i      -> Mutex.lock m;
-                       Stack.push i s;
-                       Mutex.unlock m; RPush
-      | Pop         -> Mutex.lock m;
-                       let r = Util.protect Stack.pop s in
-                       Mutex.unlock m;
-                       RPop r
-      | Pop_opt     -> Mutex.lock m;
-                       let r = Stack.pop_opt s in
-                       Mutex.unlock m;
-                       RPop_opt r
-      | Top         -> Mutex.lock m;
-                       let r = Util.protect Stack.top s in
-                       Mutex.unlock m;
-                       RTop r
-      | Top_opt     -> Mutex.lock m;
-                       let r = Stack.top_opt s in
-                       Mutex.unlock m;
-                       RTop_opt r
-      | Clear       -> Mutex.lock m;
-                       Stack.clear s;
-                       Mutex.unlock m;
-                       RClear
-      | Is_empty    -> Mutex.lock m;
-                       let b = Stack.is_empty s in
-                       Mutex.unlock m;
-                       RIs_empty b
-      | Fold (f, a) -> Mutex.lock m;
-                       let r  = Stack.fold (Fn.apply f) a s in
-                       Mutex.unlock m;
-                       RFold r
-      | Length      -> Mutex.lock m;
-                       let l = Stack.length s in
-                       Mutex.unlock m;
-                       RLength l
+      | None,Push (t,i)   -> Mutex.lock m;
+                             Stack.push i s.(t);
+                             Mutex.unlock m; RPush
+      | None,Pop t        -> Mutex.lock m;
+                             let r = Util.protect Stack.pop s.(t) in
+                             Mutex.unlock m;
+                             RPop r
+      | None,Pop_opt t    -> Mutex.lock m;
+                             let r = Stack.pop_opt s.(t) in
+                             Mutex.unlock m;
+                             RPop_opt r
+      | None,Top t        -> Mutex.lock m;
+                             let r = Util.protect Stack.top s.(t) in
+                             Mutex.unlock m;
+                             RTop r
+      | None,Top_opt t    -> Mutex.lock m;
+                             let r = Stack.top_opt s.(t) in
+                             Mutex.unlock m;
+                             RTop_opt r
+      | None,Clear t      -> Mutex.lock m;
+                             Stack.clear s.(t);
+                             Mutex.unlock m;
+                             RClear
+      | None,Is_empty t   -> Mutex.lock m;
+                             let b = Stack.is_empty s.(t) in
+                             Mutex.unlock m;
+                             RIs_empty b
+      | None,Fold (t,f,a) -> Mutex.lock m;
+                             let r  = Stack.fold (Fn.apply f) a s.(t) in
+                             Mutex.unlock m;
+                             RFold r
+      | None,Length t     -> Mutex.lock m;
+                             let l = Stack.length s.(t) in
+                             Mutex.unlock m;
+                             RLength l
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   end
 
 module ST = Lin.Make(SConf)

From af70d495af58c6b7a740f869e490d223127737c1 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 16:03:02 +0200
Subject: [PATCH 17/57] omit flush in Var.pp

---
 lib/lin.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 00faa15c4..903fe5cf7 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -16,7 +16,7 @@ struct
     (fun () -> let old = !counter in
       incr counter; old),
     (fun () -> counter := 0)
-  let pp fmt v = Format.fprintf fmt "t%i%!" v
+  let pp fmt v = Format.fprintf fmt "t%i" v
   let show t =
     let buf = Buffer.create 24 in
     let fmt = Format.formatter_of_buffer buf in

From 5754e04e92b464c07f68f434e4f8e686c3fad83f Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 16:04:41 +0200
Subject: [PATCH 18/57] rm opam dependency on ppx_deriving_qcheck

---
 multicoretests.opam | 1 -
 1 file changed, 1 deletion(-)

diff --git a/multicoretests.opam b/multicoretests.opam
index e1f59ea2f..8ec65ef2b 100644
--- a/multicoretests.opam
+++ b/multicoretests.opam
@@ -15,7 +15,6 @@ depends: [
   "domainslib" {>= "0.5.0"}
   "ppx_deriving" {>= "5.2.1"}
   "qcheck-core" {>= "0.19"}
-  "ppx_deriving_qcheck" {>= "0.2.0"}
   "lockfree" {>= "0.13"}
   "qcheck-lin" {= version}
   "qcheck-stm" {= version}

From 406e653f5097bc35eb95a0fe70c6900dfda2ecef Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 17:52:11 +0200
Subject: [PATCH 19/57] print init return value in annotated trace for
 consistency

---
 lib/lin.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 903fe5cf7..6c45d95f7 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -146,6 +146,7 @@ module MakeDomThr(Spec : CmdSpec)
     | Some v -> Printf.sprintf "let %s = %s" (Var.show v) (Spec.show_cmd c)
 
   let init_cmd = "let t0 = init ()"
+  let init_cmd_ret = init_cmd ^ "  : ()"
 
   let arb_cmds_par seq_len par_len =
     let gen_triple st =
@@ -218,7 +219,7 @@ module MakeDomThr(Spec : CmdSpec)
     let seq_sut = init_sut array_size in
     check_seq_cons array_size pref_obs obs1 obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd
+         @@ 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)
 
@@ -238,7 +239,7 @@ module MakeDomThr(Spec : CmdSpec)
       (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
       check_seq_cons array_size pref_obs !obs1 !obs2 seq_sut []
       || Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd
+         @@ 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))
 end
@@ -345,7 +346,7 @@ module Make(Spec : CmdSpec)
        (* exclude [Yield]s from sequential executions when searching for an interleaving *)
        EffTest.check_seq_cons array_size (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
        || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
-       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:EffTest.init_cmd
+       @@ 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))
 

From d765e64c606cc51f9ec29650df72201778e59651 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 16 Aug 2022 18:07:06 +0200
Subject: [PATCH 20/57] fix Var.t printing w/pp and show

---
 lib/lin.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 6c45d95f7..e82366bb0 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -16,14 +16,8 @@ struct
     (fun () -> let old = !counter in
       incr counter; old),
     (fun () -> counter := 0)
-  let pp fmt v = Format.fprintf fmt "t%i" v
-  let show t =
-    let buf = Buffer.create 24 in
-    let fmt = Format.formatter_of_buffer buf in
-    pp fmt t;
-    let str = Buffer.contents buf in
-    Buffer.clear buf;
-    str
+  let show v = Format.sprintf "t%i" v
+  let pp fmt v = Format.fprintf fmt "%s" (show v)
   let shrink = Shrink.int
 end
 

From 0f3b8cb538ec6d26b45d59898a0d142df41dafbb Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 18 Aug 2022 08:54:52 +0200
Subject: [PATCH 21/57] make Bytes test a negative test

---
 src/bytes/lin_tests_dsl.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index c69f2efa0..f5538d779 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -33,6 +33,6 @@ module BT = Lin_api.Make(BConf)
 Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main [
-  BT.lin_test `Domain ~count:1000 ~name:"Lin_api Bytes test with Domain";
-  BT.lin_test `Thread ~count:1000 ~name:"Lin_api Bytes test with Thread";
+  BT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Bytes test with Domain";
+  BT.lin_test     `Thread ~count:1000 ~name:"Lin_api Bytes test with Thread";
 ]

From b80dd9323f351c2f4d8c625c82923759eefd2a97 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 19 Aug 2022 09:30:56 +0200
Subject: [PATCH 22/57] first shrink var, then recurse

---
 lib/lin_api.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 84aedc7c2..58aff433d 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -237,9 +237,9 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
       | Fun.Ret_ignore _ty -> Shrink.nil
       | Fun.(Fn (State, fdesc_rem)) ->
           (function (Args.FnState (index,args)) ->
-            Iter.(map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args)
+            Iter.(map (fun index -> Args.FnState (index,args)) (Lin.Var.shrink index)
                   <+>
-                  map (fun index -> Args.FnState (index,args)) (Lin.Var.shrink index))
+                  map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args))
                   | _ -> failwith "FnState: should not happen")
       | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
           (match arg_arb.shrink with

From 4c6dff8d5a064e430bb20c8b0328de50ae59b43d Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 19 Aug 2022 09:45:33 +0200
Subject: [PATCH 23/57] reduce Bytes Thread test count

---
 src/bytes/lin_tests_dsl.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index f5538d779..979db0141 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -9,6 +9,7 @@ module BConf = struct
   open Lin_api
   let int = nat_small
 (*let int = int_bound 10*)
+
   let api = [
     val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
@@ -34,5 +35,5 @@ Util.set_ci_printing ()
 ;;
 QCheck_base_runner.run_tests_main [
   BT.neg_lin_test `Domain ~count:1000 ~name:"Lin_api Bytes test with Domain";
-  BT.lin_test     `Thread ~count:1000 ~name:"Lin_api Bytes test with Thread";
+  BT.lin_test     `Thread ~count:250  ~name:"Lin_api Bytes test with Thread";
 ]

From 9f61c2087d3a1514510bfad6515fe54e8852ed0f Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 19 Aug 2022 09:46:43 +0200
Subject: [PATCH 24/57] comment out Bytes.escaped causing segfault

---
 src/bytes/lin_tests_dsl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 979db0141..54e06c388 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -24,7 +24,7 @@ module BConf = struct
     val_ "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
     val_ "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
     val_ "Bytes.trim"        Bytes.trim        (t @-> returning_ t);
-    val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t);
+ (* val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t); *)
     val_ "Bytes.index"       Bytes.index       (t @-> char @-> returning_or_exc int);
     val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int)]
 end

From 3e6fa03d000eabd095bd25241313008225ab8689 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 19 Aug 2022 09:48:00 +0200
Subject: [PATCH 25/57] increase frequency of Bytes.{fill,blit_string}

---
 src/bytes/lin_tests_dsl.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 54e06c388..9cda0a4d7 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -21,8 +21,8 @@ module BConf = struct
     val_ "Bytes.of_string"   Bytes.of_string   (string @-> returning_ t);
     val_ "Bytes.to_string"   Bytes.to_string   (t @-> returning string);
     val_ "Bytes.sub_string"  Bytes.sub_string  (t @-> int @-> int @-> returning_or_exc string);
-    val_ "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
-    val_ "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
+    val_freq 2 "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
+    val_freq 2 "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
     val_ "Bytes.trim"        Bytes.trim        (t @-> returning_ t);
  (* val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t); *)
     val_ "Bytes.index"       Bytes.index       (t @-> char @-> returning_or_exc int);

From e409fda3c2321b47b18d00533fd444a283a2946a Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 19 Aug 2022 09:49:56 +0200
Subject: [PATCH 26/57] add Bytes.make

---
 src/bytes/lin_tests_dsl.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 9cda0a4d7..74e54dfb5 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -11,6 +11,7 @@ module BConf = struct
 (*let int = int_bound 10*)
 
   let api = [
+    val_ "Bytes.make"        Bytes.make        (int @-> char @-> returning_ t);
     val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
     val_ "Bytes.set"         Bytes.set         (t @-> int @-> char @-> returning_or_exc unit);

From cbae0eabe4db982c64de522dba87d6757ae240b1 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 22 Sep 2022 09:29:13 +0200
Subject: [PATCH 27/57] update documented Util interface with optional init_cmd

---
 lib/util.mli | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/lib/util.mli b/lib/util.mli
index 53551470c..47df85336 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -28,6 +28,7 @@ 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
@@ -35,6 +36,7 @@ val print_triple_vertical :
     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

From bf7784d58f1243f9350a9e5b30e82f61d3023ff6 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Tue, 4 Oct 2022 18:54:19 +0200
Subject: [PATCH 28/57] Factorise some common code

---
 lib/lin_api.ml | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 58aff433d..234b27d1e 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -285,18 +285,9 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
   let rec apply_f
     : type a r. a -> (a, r) Args.args -> t array -> Lin.Var.t option -> r = fun f args state opt_target ->
       match args with
-      | Ret _ ->
-          (* This happens only if there was a non-function value in the API,
-             which I'm not sure makes sense *)
-          raise (Invalid_argument "apply_f")
-      | Ret_or_exc _ ->
-          (* This happens only if there was a non-function value in the API,
-             which I'm not sure makes sense *)
-          raise (Invalid_argument "apply_f")
-      | Ret_ignore _ ->
-          (* This happens only if there was a non-function value in the API,
-             which I'm not sure makes sense *)
-          raise (Invalid_argument "apply_f")
+      | Ret _
+      | Ret_or_exc _
+      | Ret_ignore _
       | Ret_ignore_or_exc _ ->
           (* This happens only if there was a non-function value in the API,
              which I'm not sure makes sense *)

From 1190f4199f5b4a2967264ecc88951f05597183d4 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Tue, 4 Oct 2022 18:55:29 +0200
Subject: [PATCH 29/57] Factorise some common code

This factorisation removes the explicit pattern matching on the
constructor of `rem`
---
 lib/lin_api.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 234b27d1e..9f2e15522 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -315,9 +315,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
              try Ok (ignore @@ f state.(index))
              with e -> Error e
            end)
-      | FnState (index, (Fn _ as rem)) ->
-          apply_f (f state.(index)) rem state opt_target
-      | FnState (index, (FnState _ as rem)) ->
+      | FnState (index, rem) ->
           apply_f (f state.(index)) rem state opt_target
       | Fn (arg, Ret _) ->
           f arg
@@ -333,9 +331,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
             try Ok (ignore @@ f arg)
             with e -> Error e
           end
-      | Fn (arg, (Fn _ as rem)) ->
-          apply_f (f arg) rem state opt_target
-      | Fn (arg, (FnState _ as rem)) ->
+      | Fn (arg, rem) ->
           apply_f (f arg) rem state opt_target
 
   let run (opt_target,cmd) state =

From a317f9cff85d31d2acb6364e81ef74dfe08475e9 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Tue, 4 Oct 2022 19:28:12 +0200
Subject: [PATCH 30/57] Complete the Bigarray.Array1 tests with multiple `t`s

---
 src/bigarray/lin_tests_dsl.ml | 44 +++++++++++++++++++++++++++++++----
 1 file changed, 40 insertions(+), 4 deletions(-)

diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml
index 0a94644fb..750823889 100644
--- a/src/bigarray/lin_tests_dsl.ml
+++ b/src/bigarray/lin_tests_dsl.ml
@@ -2,26 +2,62 @@
 (*           Tests of thread-unsafe [Bigarray.Array1] of ints             *)
 (* ********************************************************************** *)
 
+(* Bigarray.Array1 API:
+
+    val create : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> ('a, 'b, 'c) t
+    val init : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> (int -> 'a) -> ('a, 'b, 'c) t
+    external dim : ('a, 'b, 'c) t -> int
+    external kind : ('a, 'b, 'c) t -> ('a, 'b) Bigarray.kind
+    external layout : ('a, 'b, 'c) t -> 'c Bigarray.layout
+    val change_layout : ('a, 'b, 'c) t -> 'd Bigarray.layout -> ('a, 'b, 'd) t
+    val size_in_bytes : ('a, 'b, 'c) t -> int
+    external get : ('a, 'b, 'c) t -> int -> 'a
+    external set : ('a, 'b, 'c) t -> int -> 'a -> unit
+    external sub : ('a, 'b, 'c) t -> int -> int -> ('a, 'b, 'c) t
+    val slice : ('a, 'b, 'c) t -> int -> ('a, 'b, 'c) Bigarray.Array0.t
+    external blit : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> unit
+    external fill : ('a, 'b, 'c) t -> 'a -> unit
+    val of_array : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> 'a array -> ('a, 'b, 'c) t
+    external unsafe_get : ('a, 'b, 'c) t -> int -> 'a
+    external unsafe_set : ('a, 'b, 'c) t -> int -> 'a -> unit
+*)
+
 module BA1Conf =
 struct
   open Bigarray
   type t = (int, int_elt, c_layout) Array1.t
 
-  let array_size = 16
-  let init () =
-    let arr = Array1.create int C_layout array_size in
+  let array_create sz =
+    let arr = Array1.create int C_layout sz in
     Array1.fill arr 0 ;
     arr
+  let of_array = Array1.of_array int C_layout
+  let dummy_change_layout arr = Array1.change_layout arr C_layout
+
+  let array_size = 16
+  let init () = array_create array_size
   let cleanup _ = ()
 
   open Lin_api
   let int = int_small
 
   let api =
-    [ val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
+    [ val_ "Bigarray.Array1.create"        array_create         (int @-> returning_ t);
+      (* [Array1.init] requires a function *)
+      val_ "Bigarray.Array1.dim"           Array1.dim           (t @-> returning int);
+      (* [Array1.kind] returns an untestable value *)
+      (* [change_layout]: the layout is fixed in our sut, so we test a dummy version *)
+      val_ "Bigarray.Array1.change_layout" dummy_change_layout  (t @-> returning_ t);
+      val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
       val_ "Bigarray.Array1.get"           Array1.get           (t @-> int @-> returning_or_exc int);
       val_ "Bigarray.Array1.set"           Array1.set           (t @-> int @-> int @-> returning_or_exc unit);
+      val_ "Bigarray.Array1.sub"           Array1.sub           (t @-> int @-> int @-> returning_or_exc_ t);
+      (* [Array1.slice]: cannot be tested since it produces a Bigarray.Array0.t *)
+      val_ "Bigarray.Array1.blit"          Array1.blit          (t @-> t @-> returning unit);
       val_ "Bigarray.Array1.fill"          Array1.fill          (t @-> int @-> returning unit);
+      val_ "Bigarray.Array1.of_array"      of_array             (array int @-> returning_ t);
+      (* [Array1.unsafe_get] and [Array1.unsafe_set] cannot be tested:
+         they can segfault or produce any useless result *)
     ]
 end
 

From f3d1591d9b65db2e6b106e452ba503da4e949871 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Thu, 6 Oct 2022 14:19:46 +0200
Subject: [PATCH 31/57] Lin: Fix commands during shrinking to use existing
 states

During shrinking, commands could be using a state that is no longer
built previously. This adds a `fix_cmd` function to CmdSpec that will
produce possible fixes for a command whenever it uses a state that
disappeared due to shrinking.
---
 lib/lin.ml     | 44 +++++++++++++++++++++++++++++++++++++++++---
 lib/lin_api.ml | 23 +++++++++++++++++++++++
 2 files changed, 64 insertions(+), 3 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index e82366bb0..871e418ae 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -49,6 +49,15 @@ module type CmdSpec = sig
   (** A command shrinker.
       To a first approximation you can use [Shrink.nil]. *)
 
+  val fix_cmd : Env.t -> cmd -> cmd Iter.t
+  (** A command fixer.
+      Fixes the given [cmd] so that it uses only states in the given
+      [Env.t]. If the initial [cmd] used a state that is no longer
+      available, it should iterate over all the lesser states
+      available in [Env.t]. If all the necessary states are still
+      available, it should generate a one-element iterator.
+      Can assume that [Env.t] is sorted in decreasing order. *)
+
   type res
   (** The command result type *)
 
@@ -110,20 +119,47 @@ module MakeDomThr(Spec : CmdSpec)
 
   let shrink_cmd (opt,c) = Iter.map (fun c -> opt,c) (Spec.shrink_cmd c)
 
+  (* Note: the [env] fed to [Spec.fix_cmd] are in reverse (ie should
+     be _decreasing_) order *)
+  let fix_cmds env cmds =
+    let rec aux env cmds =
+      match cmds with
+      | [] -> Iter.return []
+      | (opt,cmd) :: cmds ->
+          let env' = Option.fold ~none:env ~some:(fun i -> i::env) opt in
+          Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)
+    in aux env cmds
+
+  (* Note that the result is built in reverse (ie should be
+     _decreasing_) order *)
+  let rec extract_env env cmds =
+    match cmds with
+    | []                  -> env
+    | (Some i, _) :: cmds -> extract_env (i::env) cmds
+    | (None,   _) :: cmds -> extract_env     env  cmds
+
   let shrink_triple' (seq,p1,p2) =
     let open Iter in
     (* Shrinking heuristic:
        First reduce the cmd list sizes as much as possible, since the interleaving
        is most costly over long cmd lists. *)
-    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
+    let concat_map f it = flatten (map f it) in
+    let fix_seq seq =
+      let seq_env = extract_env [0] seq in
+      let triple seq p1 p2 = (seq,p1,p2) in
+      map triple (fix_cmds [0] seq) <*> fix_cmds seq_env p1 <*> fix_cmds seq_env p2
+    in
+    let seq_env = extract_env [0] seq in
+
+    concat_map fix_seq (Shrink.list_spine seq)
     <+>
     (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
     <+>
     (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
     <+>
-    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
+    concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)
     <+>
-    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
+    concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)
     <+>
     (* Secondly reduce the cmd data of individual list elements *)
     (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
@@ -296,6 +332,8 @@ module Make(Spec : CmdSpec)
          [(3,Gen.return (None,SchedYield));
           (5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
 
+    let fix_cmd _ = Iter.return
+
     let shrink_cmd c = match c with
       | SchedYield -> Iter.empty
       | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)
diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 9f2e15522..c5ab21de3 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -267,6 +267,29 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
 
   let show_cmd (Cmd (_,args,_,print,_,_)) = print args
 
+  let rec list_drop_while cnd xs =
+    match xs with
+    | (x :: xs) when cnd x -> list_drop_while cnd xs
+    | _                    -> xs
+
+  let rec fix_args
+    : type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
+    fun env args ->
+    let open QCheck in
+    let open Args in
+    let fn_state i args = FnState (i,args) in
+    match args with
+    | FnState (i, args) ->
+        ( let env' = list_drop_while (fun i' -> i' > i) env in
+          match env' with
+          | i' :: _ when i = i' -> Iter.map (fn_state i) (fix_args env args)
+          | _                   -> Iter.(map fn_state (of_list env') <*> fix_args env args) )
+    | Fn (x, args) -> Iter.map (fun args -> Fn (x, args)) (fix_args env args)
+    | _            -> Iter.return args
+
+  let fix_cmd env (Cmd (name,args,rty,print,shrink,f)) =
+    QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (fix_args env args)
+
   let shrink_cmd (Cmd (name,args,rty,print,shrink,f)) =
     QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink args)
 

From ca731fa4d886b8401464c63b5416c2e9f450061d Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Thu, 6 Oct 2022 18:36:32 +0200
Subject: [PATCH 32/57] Shorten random arrays to avoid slow tests

---
 src/bigarray/lin_tests_dsl.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml
index 750823889..73b1365f9 100644
--- a/src/bigarray/lin_tests_dsl.ml
+++ b/src/bigarray/lin_tests_dsl.ml
@@ -31,7 +31,9 @@ struct
     let arr = Array1.create int C_layout sz in
     Array1.fill arr 0 ;
     arr
-  let of_array = Array1.of_array int C_layout
+  let of_array arr =
+    Array1.of_array int C_layout
+      (if Array.length arr > 100 then Array.sub arr 0 100 else arr)
   let dummy_change_layout arr = Array1.change_layout arr C_layout
 
   let array_size = 16

From 32c4b9c28a4d1eabe77d5070e3bca67830d24778 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Fri, 7 Oct 2022 18:22:21 +0200
Subject: [PATCH 33/57] Generalise the iterator on valid states for shrinking

---
 lib/lin.ml     |  9 +++++++++
 lib/lin_api.ml | 16 ++++------------
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 871e418ae..09c74e799 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -24,10 +24,19 @@ end
 module Env : sig
   type t = Var.t list
   val gen_t_var : t -> Var.t Gen.t
+  val valid_states : t -> Var.t -> Var.t Iter.t
 end =
 struct
   type t = Var.t list
   let gen_t_var env = Gen.oneofl env
+  let valid_states env v =
+    let rec drop_invalids env =
+      match env with
+      | (v' :: env) when v' > v -> drop_invalids env
+      | _                       -> env in
+    match drop_invalids env with
+    | v' :: _ when v' = v -> Iter.return v
+    | env'                -> Iter.of_list env'
 end
 
 module type CmdSpec = sig
diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index c5ab21de3..45d39263e 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -267,25 +267,17 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
 
   let show_cmd (Cmd (_,args,_,print,_,_)) = print args
 
-  let rec list_drop_while cnd xs =
-    match xs with
-    | (x :: xs) when cnd x -> list_drop_while cnd xs
-    | _                    -> xs
-
   let rec fix_args
     : type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
     fun env args ->
+    let open Lin in
     let open QCheck in
     let open Args in
     let fn_state i args = FnState (i,args) in
     match args with
-    | FnState (i, args) ->
-        ( let env' = list_drop_while (fun i' -> i' > i) env in
-          match env' with
-          | i' :: _ when i = i' -> Iter.map (fn_state i) (fix_args env args)
-          | _                   -> Iter.(map fn_state (of_list env') <*> fix_args env args) )
-    | Fn (x, args) -> Iter.map (fun args -> Fn (x, args)) (fix_args env args)
-    | _            -> Iter.return args
+    | FnState (i, args) -> Iter.(map fn_state (Env.valid_states env i) <*> fix_args env args)
+    | Fn (x, args)      -> Iter.map (fun args -> Fn (x, args)) (fix_args env args)
+    | _                 -> Iter.return args
 
   let fix_cmd env (Cmd (name,args,rty,print,shrink,f)) =
     QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (fix_args env args)

From 13ee694cfab49520296c84d079f319f0fdc2e1c6 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Fri, 7 Oct 2022 18:23:20 +0200
Subject: [PATCH 34/57] Add a bounded_array function

---
 lib/lin_api.ml  | 8 ++++++++
 lib/lin_api.mli | 3 +++
 2 files changed, 11 insertions(+)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 45d39263e..f93cb6e59 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -58,6 +58,14 @@ let array : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable)
   | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.array arb, QCheck.Print.array print, Array.for_all2 eq)
   | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
 
+let bounded_array : type a c s. int -> (a, c, s, combinable) ty -> (a array, c, s, combinable) ty =
+  fun maxsize ty ->
+  let array = QCheck.array_of_size (QCheck.Gen.int_bound maxsize) in
+  match ty with
+  | Gen (arb, print) -> Gen (array arb, QCheck.Print.array print)
+  | GenDeconstr (arb, print, eq) -> GenDeconstr (array arb, QCheck.Print.array print, Array.for_all2 eq)
+  | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
+
 let print_seq pp s =
   let b = Buffer.create 25 in
   Buffer.add_char b '<';
diff --git a/lib/lin_api.mli b/lib/lin_api.mli
index 3654e4f61..c6128ccad 100644
--- a/lib/lin_api.mli
+++ b/lib/lin_api.mli
@@ -144,6 +144,9 @@ 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]. *)
 
+(* FIXME: missing documentation *)
+val bounded_array : int -> ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
+
 val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty
 (** The [seq] combinator represents the [Seq.t] type.
     The generated sequences from [seq t] have a length resulting from [QCheck.Gen.nat]

From c6554911d8735afed28489a64b786b24af6de403 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Fri, 7 Oct 2022 18:26:24 +0200
Subject: [PATCH 35/57] Use bounded_array in bigarray tests

Instead of truncating random arrays when they are too big, generate
arrays of bounded size to begin with
---
 src/bigarray/lin_tests_dsl.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml
index 73b1365f9..c85ebb546 100644
--- a/src/bigarray/lin_tests_dsl.ml
+++ b/src/bigarray/lin_tests_dsl.ml
@@ -31,9 +31,7 @@ struct
     let arr = Array1.create int C_layout sz in
     Array1.fill arr 0 ;
     arr
-  let of_array arr =
-    Array1.of_array int C_layout
-      (if Array.length arr > 100 then Array.sub arr 0 100 else arr)
+  let of_array = Array1.of_array int C_layout
   let dummy_change_layout arr = Array1.change_layout arr C_layout
 
   let array_size = 16
@@ -57,7 +55,7 @@ struct
       (* [Array1.slice]: cannot be tested since it produces a Bigarray.Array0.t *)
       val_ "Bigarray.Array1.blit"          Array1.blit          (t @-> t @-> returning unit);
       val_ "Bigarray.Array1.fill"          Array1.fill          (t @-> int @-> returning unit);
-      val_ "Bigarray.Array1.of_array"      of_array             (array int @-> returning_ t);
+      val_ "Bigarray.Array1.of_array"      of_array             (bounded_array 100 int @-> returning_ t);
       (* [Array1.unsafe_get] and [Array1.unsafe_set] cannot be tested:
          they can segfault or produce any useless result *)
     ]

From d4fc1eb40b64a3c440cfb896411c0225e63a084e Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@rustyne.lautre.net>
Date: Fri, 7 Oct 2022 19:20:01 +0200
Subject: [PATCH 36/57] Define fix_cmd for all existing Lin tests

---
 lib/lin.ml                        |  4 +++-
 src/array/lin_tests.ml            | 13 +++++++++++++
 src/atomic/lin_tests.ml           | 10 ++++++++++
 src/hashtbl/lin_tests.ml          | 12 ++++++++++++
 src/internal/cleanup_lin.ml       |  5 +++++
 src/lazy/lin_tests.ml             |  7 +++++++
 src/neg_tests/lin_tests_common.ml | 18 ++++++++++++++++++
 src/queue/lin_tests.ml            | 11 +++++++++++
 src/stack/lin_tests.ml            | 11 +++++++++++
 9 files changed, 90 insertions(+), 1 deletion(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 09c74e799..67966d9fb 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -341,7 +341,9 @@ module Make(Spec : CmdSpec)
          [(3,Gen.return (None,SchedYield));
           (5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
 
-    let fix_cmd _ = Iter.return
+    let fix_cmd env = function
+      | SchedYield -> Iter.return SchedYield
+      | UserCmd cmd -> Iter.map (fun c -> UserCmd c) (Spec.fix_cmd env cmd)
 
     let shrink_cmd c = match c with
       | SchedYield -> Iter.empty
diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml
index ea95150c2..65fccbca5 100644
--- a/src/array/lin_tests.ml
+++ b/src/array/lin_tests.ml
@@ -58,6 +58,19 @@ struct
     | Sort v      -> Iter.map (fun v -> Sort v)      (Var.shrink v)
     | To_seq v    -> Iter.map (fun v -> To_seq v)    (Var.shrink v)
 
+  let fix_cmd env = function
+    | Length i       -> Iter.map (fun i -> Length i      ) (Env.valid_states env i)
+    | Get (i,x)      -> Iter.map (fun i -> Get (i,x)     ) (Env.valid_states env i)
+    | Set (i,x,z)    -> Iter.map (fun i -> Set (i,x,z)   ) (Env.valid_states env i)
+    | Sub (i,x,y)    -> Iter.map (fun i -> Sub (i,x,y)   ) (Env.valid_states env i)
+    | Copy i         -> Iter.map (fun i -> Copy i        ) (Env.valid_states env i)
+    | Fill (i,x,y,z) -> Iter.map (fun i -> Fill (i,x,y,z)) (Env.valid_states env i)
+    | To_list i      -> Iter.map (fun i -> To_list i     ) (Env.valid_states env i)
+    | Mem (i,z)      -> Iter.map (fun i -> Mem (i,z)     ) (Env.valid_states env i)
+    | Sort i         -> Iter.map (fun i -> Sort i        ) (Env.valid_states env i)
+    | To_seq i       -> Iter.map (fun i -> To_seq i      ) (Env.valid_states env i)
+    | Append (i,j)   -> Iter.(map (fun i j -> Append (i,j)) (Env.valid_states env i) <*> (Env.valid_states env j))
+
   open Util
   (*let pp_exn = Util.pp_exn*)
   let pp fmt t = Format.fprintf fmt "%s" (QCheck.Print.(array char) t)
diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml
index bb2f29a40..6c6051150 100644
--- a/src/atomic/lin_tests.ml
+++ b/src/atomic/lin_tests.ml
@@ -32,6 +32,16 @@ struct
 
   let shrink_cmd = Shrink.nil
 
+  let fix_cmd env = function
+    | Make x as cmd           -> Iter.return cmd
+    | Get i                   -> Iter.map (fun i -> Get i                  ) (Env.valid_states env i)
+    | Set (i,x)               -> Iter.map (fun i -> Set (i,x)              ) (Env.valid_states env i)
+    | Exchange (i,x)          -> Iter.map (fun i -> Exchange (i,x)         ) (Env.valid_states env i)
+    | Compare_and_set (i,x,y) -> Iter.map (fun i -> Compare_and_set (i,x,y)) (Env.valid_states env i)
+    | Fetch_and_add (i,x)     -> Iter.map (fun i -> Fetch_and_add (i,x)    ) (Env.valid_states env i)
+    | Incr i                  -> Iter.map (fun i -> Incr i                 ) (Env.valid_states env i)
+    | Decr i                  -> Iter.map (fun i -> Decr i                 ) (Env.valid_states env i)
+
   type res =
     | RMake of unit
     | RGet of int
diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml
index 527adafcc..783a39c8d 100644
--- a/src/hashtbl/lin_tests.ml
+++ b/src/hashtbl/lin_tests.ml
@@ -53,6 +53,18 @@ struct
     | Mem (v,c) -> Iter.map (fun c -> Mem (v,c)) (Shrink.char c)
     | Length _ -> Iter.empty
 
+  let fix_cmd env = function
+    | Clear i         -> Iter.map (fun i -> Clear i        ) (Env.valid_states env i)
+    | Copy i          -> Iter.map (fun i -> Copy i         ) (Env.valid_states env i)
+    | Add (i,x,y)     -> Iter.map (fun i -> Add (i,x,y)    ) (Env.valid_states env i)
+    | Remove (i,x)    -> Iter.map (fun i -> Remove (i,x)   ) (Env.valid_states env i)
+    | Find (i,x)      -> Iter.map (fun i -> Find (i,x)     ) (Env.valid_states env i)
+    | Find_opt (i,x)  -> Iter.map (fun i -> Find_opt (i,x) ) (Env.valid_states env i)
+    | Find_all (i,x)  -> Iter.map (fun i -> Find_all (i,x) ) (Env.valid_states env i)
+    | Replace (i,x,y) -> Iter.map (fun i -> Replace (i,x,y)) (Env.valid_states env i)
+    | Mem (i,x)       -> Iter.map (fun i -> Mem (i,x)      ) (Env.valid_states env i)
+    | Length i        -> Iter.map (fun i -> Length i       ) (Env.valid_states env i)
+
   type res =
     | RClear
     | RCopy
diff --git a/src/internal/cleanup_lin.ml b/src/internal/cleanup_lin.ml
index c0d354542..98ffe6eef 100644
--- a/src/internal/cleanup_lin.ml
+++ b/src/internal/cleanup_lin.ml
@@ -24,6 +24,11 @@ struct
 
   let shrink_cmd = Shrink.nil
 
+  let fix_cmd env = function
+    | Get i     -> Iter.map (fun i -> Get i    ) (Lin.Env.valid_states env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Lin.Env.valid_states env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Lin.Env.valid_states env i)
+
   let init () = (ref Inited, ref 0)
 
   let cleanup (status,_) =
diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml
index fea71a263..f4a53a59d 100644
--- a/src/lazy/lin_tests.ml
+++ b/src/lazy/lin_tests.ml
@@ -62,6 +62,13 @@ struct
   (* the Lazy tests already take a while to run - so better avoid spending extra time shrinking *)
   let shrink_cmd = Shrink.nil
 
+  let fix_cmd env = function
+    | Force i       -> Iter.map (fun i -> Force i      ) (Env.valid_states env i)
+    | Force_val i   -> Iter.map (fun i -> Force_val i  ) (Env.valid_states env i)
+    | Is_val i      -> Iter.map (fun i -> Is_val i     ) (Env.valid_states env i)
+    | Map (i,f)     -> Iter.map (fun i -> Map (i,f)    ) (Env.valid_states env i)
+    | Map_val (i,f) -> Iter.map (fun i -> Map_val (i,f)) (Env.valid_states env i)
+
   type t = int Lazy.t
 
   let cleanup _ = ()
diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml
index 162d7ace3..1088c238f 100644
--- a/src/neg_tests/lin_tests_common.ml
+++ b/src/neg_tests/lin_tests_common.ml
@@ -52,6 +52,13 @@ module RConf_int = struct
     | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int i)
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
 
+  let fix_cmd env = function
+    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_states env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_states env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_states env i)
+    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_states env i)
+    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_states env i)
+
   type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int.init ()
@@ -97,6 +104,13 @@ module RConf_int64 = struct
     | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int64 i)
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
 
+  let fix_cmd env = function
+    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_states env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_states env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_states env i)
+    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_states env i)
+    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_states env i)
+
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int64.init ()
@@ -146,6 +160,10 @@ struct
     | Add_node (t,i) -> Iter.map (fun i -> Add_node (t,i)) (T.shrink i)
     | Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
 
+  let fix_cmd env = function
+    | Add_node (i,x) -> Iter.map (fun i -> Add_node (i,x)) (Lin.Env.valid_states env i)
+    | Member (i,x)   -> Iter.map (fun i -> Member (i,x)  ) (Lin.Env.valid_states env i)
+
   type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
 
   let init () = CList.list_init T.zero
diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml
index 88e409b43..ce5481ad4 100644
--- a/src/queue/lin_tests.ml
+++ b/src/queue/lin_tests.ml
@@ -47,6 +47,17 @@ module Spec =
             <+>
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
+    let fix_cmd env = function
+      | Add (i,x)    -> Iter.map (fun i -> Add (i,x)   ) (Env.valid_states env i)
+      | Take i       -> Iter.map (fun i -> Take i      ) (Env.valid_states env i)
+      | Take_opt i   -> Iter.map (fun i -> Take_opt i  ) (Env.valid_states env i)
+      | Peek i       -> Iter.map (fun i -> Peek i      ) (Env.valid_states env i)
+      | Peek_opt i   -> Iter.map (fun i -> Peek_opt i  ) (Env.valid_states env i)
+      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_states env i)
+      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_states env i)
+      | Fold (i,x,y) -> Iter.map (fun i -> Fold (i,x,y)) (Env.valid_states env i)
+      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_states env i)
+
     type res =
       | RAdd
       | RTake of ((int, exn) result [@equal (=)])
diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml
index 211043098..7b00a5d2b 100644
--- a/src/stack/lin_tests.ml
+++ b/src/stack/lin_tests.ml
@@ -48,6 +48,17 @@ module Spec =
             <+>
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
+    let fix_cmd env = function
+      | Push (i,x)   -> Iter.map (fun i -> Push (i,x)  ) (Env.valid_states env i)
+      | Pop i        -> Iter.map (fun i -> Pop i       ) (Env.valid_states env i)
+      | Pop_opt i    -> Iter.map (fun i -> Pop_opt i   ) (Env.valid_states env i)
+      | Top i        -> Iter.map (fun i -> Top i       ) (Env.valid_states env i)
+      | Top_opt i    -> Iter.map (fun i -> Top_opt i   ) (Env.valid_states env i)
+      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_states env i)
+      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_states env i)
+      | Fold (i,f,x) -> Iter.map (fun i -> Fold (i,f,x)) (Env.valid_states env i)
+      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_states env i)
+
     type res =
       | RPush
       | RPop of ((int, exn) result [@equal (=)])

From d05a7e6d2f93112f6c99ac7d180d5015fcfd280d Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 13 Oct 2022 18:50:42 +0200
Subject: [PATCH 37/57] rename valid_states, omit drop_invalids

---
 lib/lin.ml                        | 10 +++-------
 lib/lin_api.ml                    |  2 +-
 src/array/lin_tests.ml            | 22 +++++++++++-----------
 src/atomic/lin_tests.ml           | 14 +++++++-------
 src/hashtbl/lin_tests.ml          | 20 ++++++++++----------
 src/lazy/lin_tests.ml             | 10 +++++-----
 src/neg_tests/lin_tests_common.ml | 24 ++++++++++++------------
 src/queue/lin_tests.ml            | 18 +++++++++---------
 src/stack/lin_tests.ml            | 18 +++++++++---------
 9 files changed, 67 insertions(+), 71 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 67966d9fb..b7b10e241 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -24,17 +24,13 @@ end
 module Env : sig
   type t = Var.t list
   val gen_t_var : t -> Var.t Gen.t
-  val valid_states : t -> Var.t -> Var.t Iter.t
+  val valid_t_vars : t -> Var.t -> Var.t Iter.t
 end =
 struct
   type t = Var.t list
   let gen_t_var env = Gen.oneofl env
-  let valid_states env v =
-    let rec drop_invalids env =
-      match env with
-      | (v' :: env) when v' > v -> drop_invalids env
-      | _                       -> env in
-    match drop_invalids env with
+  let valid_t_vars env v =
+    match List.filter (fun v' -> v' <= v) env with
     | v' :: _ when v' = v -> Iter.return v
     | env'                -> Iter.of_list env'
 end
diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index f93cb6e59..1f67c77b0 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -283,7 +283,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
     let open Args in
     let fn_state i args = FnState (i,args) in
     match args with
-    | FnState (i, args) -> Iter.(map fn_state (Env.valid_states env i) <*> fix_args env args)
+    | FnState (i, args) -> Iter.(map fn_state (Env.valid_t_vars env i) <*> fix_args env args)
     | Fn (x, args)      -> Iter.map (fun args -> Fn (x, args)) (fix_args env args)
     | _                 -> Iter.return args
 
diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml
index 65fccbca5..0e8eb793b 100644
--- a/src/array/lin_tests.ml
+++ b/src/array/lin_tests.ml
@@ -59,17 +59,17 @@ struct
     | To_seq v    -> Iter.map (fun v -> To_seq v)    (Var.shrink v)
 
   let fix_cmd env = function
-    | Length i       -> Iter.map (fun i -> Length i      ) (Env.valid_states env i)
-    | Get (i,x)      -> Iter.map (fun i -> Get (i,x)     ) (Env.valid_states env i)
-    | Set (i,x,z)    -> Iter.map (fun i -> Set (i,x,z)   ) (Env.valid_states env i)
-    | Sub (i,x,y)    -> Iter.map (fun i -> Sub (i,x,y)   ) (Env.valid_states env i)
-    | Copy i         -> Iter.map (fun i -> Copy i        ) (Env.valid_states env i)
-    | Fill (i,x,y,z) -> Iter.map (fun i -> Fill (i,x,y,z)) (Env.valid_states env i)
-    | To_list i      -> Iter.map (fun i -> To_list i     ) (Env.valid_states env i)
-    | Mem (i,z)      -> Iter.map (fun i -> Mem (i,z)     ) (Env.valid_states env i)
-    | Sort i         -> Iter.map (fun i -> Sort i        ) (Env.valid_states env i)
-    | To_seq i       -> Iter.map (fun i -> To_seq i      ) (Env.valid_states env i)
-    | Append (i,j)   -> Iter.(map (fun i j -> Append (i,j)) (Env.valid_states env i) <*> (Env.valid_states env j))
+    | Length i       -> Iter.map (fun i -> Length i      ) (Env.valid_t_vars env i)
+    | Get (i,x)      -> Iter.map (fun i -> Get (i,x)     ) (Env.valid_t_vars env i)
+    | Set (i,x,z)    -> Iter.map (fun i -> Set (i,x,z)   ) (Env.valid_t_vars env i)
+    | Sub (i,x,y)    -> Iter.map (fun i -> Sub (i,x,y)   ) (Env.valid_t_vars env i)
+    | Copy i         -> Iter.map (fun i -> Copy i        ) (Env.valid_t_vars env i)
+    | Fill (i,x,y,z) -> Iter.map (fun i -> Fill (i,x,y,z)) (Env.valid_t_vars env i)
+    | To_list i      -> Iter.map (fun i -> To_list i     ) (Env.valid_t_vars env i)
+    | Mem (i,z)      -> Iter.map (fun i -> Mem (i,z)     ) (Env.valid_t_vars env i)
+    | Sort i         -> Iter.map (fun i -> Sort i        ) (Env.valid_t_vars env i)
+    | To_seq i       -> Iter.map (fun i -> To_seq i      ) (Env.valid_t_vars env i)
+    | Append (i,j)   -> Iter.(map (fun i j -> Append (i,j)) (Env.valid_t_vars env i) <*> (Env.valid_t_vars env j))
 
   open Util
   (*let pp_exn = Util.pp_exn*)
diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml
index 6c6051150..76dd5b25c 100644
--- a/src/atomic/lin_tests.ml
+++ b/src/atomic/lin_tests.ml
@@ -34,13 +34,13 @@ struct
 
   let fix_cmd env = function
     | Make x as cmd           -> Iter.return cmd
-    | Get i                   -> Iter.map (fun i -> Get i                  ) (Env.valid_states env i)
-    | Set (i,x)               -> Iter.map (fun i -> Set (i,x)              ) (Env.valid_states env i)
-    | Exchange (i,x)          -> Iter.map (fun i -> Exchange (i,x)         ) (Env.valid_states env i)
-    | Compare_and_set (i,x,y) -> Iter.map (fun i -> Compare_and_set (i,x,y)) (Env.valid_states env i)
-    | Fetch_and_add (i,x)     -> Iter.map (fun i -> Fetch_and_add (i,x)    ) (Env.valid_states env i)
-    | Incr i                  -> Iter.map (fun i -> Incr i                 ) (Env.valid_states env i)
-    | Decr i                  -> Iter.map (fun i -> Decr i                 ) (Env.valid_states env i)
+    | Get i                   -> Iter.map (fun i -> Get i                  ) (Env.valid_t_vars env i)
+    | Set (i,x)               -> Iter.map (fun i -> Set (i,x)              ) (Env.valid_t_vars env i)
+    | Exchange (i,x)          -> Iter.map (fun i -> Exchange (i,x)         ) (Env.valid_t_vars env i)
+    | Compare_and_set (i,x,y) -> Iter.map (fun i -> Compare_and_set (i,x,y)) (Env.valid_t_vars env i)
+    | Fetch_and_add (i,x)     -> Iter.map (fun i -> Fetch_and_add (i,x)    ) (Env.valid_t_vars env i)
+    | Incr i                  -> Iter.map (fun i -> Incr i                 ) (Env.valid_t_vars env i)
+    | Decr i                  -> Iter.map (fun i -> Decr i                 ) (Env.valid_t_vars env i)
 
   type res =
     | RMake of unit
diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml
index 783a39c8d..ed66564fc 100644
--- a/src/hashtbl/lin_tests.ml
+++ b/src/hashtbl/lin_tests.ml
@@ -54,16 +54,16 @@ struct
     | Length _ -> Iter.empty
 
   let fix_cmd env = function
-    | Clear i         -> Iter.map (fun i -> Clear i        ) (Env.valid_states env i)
-    | Copy i          -> Iter.map (fun i -> Copy i         ) (Env.valid_states env i)
-    | Add (i,x,y)     -> Iter.map (fun i -> Add (i,x,y)    ) (Env.valid_states env i)
-    | Remove (i,x)    -> Iter.map (fun i -> Remove (i,x)   ) (Env.valid_states env i)
-    | Find (i,x)      -> Iter.map (fun i -> Find (i,x)     ) (Env.valid_states env i)
-    | Find_opt (i,x)  -> Iter.map (fun i -> Find_opt (i,x) ) (Env.valid_states env i)
-    | Find_all (i,x)  -> Iter.map (fun i -> Find_all (i,x) ) (Env.valid_states env i)
-    | Replace (i,x,y) -> Iter.map (fun i -> Replace (i,x,y)) (Env.valid_states env i)
-    | Mem (i,x)       -> Iter.map (fun i -> Mem (i,x)      ) (Env.valid_states env i)
-    | Length i        -> Iter.map (fun i -> Length i       ) (Env.valid_states env i)
+    | Clear i         -> Iter.map (fun i -> Clear i        ) (Env.valid_t_vars env i)
+    | Copy i          -> Iter.map (fun i -> Copy i         ) (Env.valid_t_vars env i)
+    | Add (i,x,y)     -> Iter.map (fun i -> Add (i,x,y)    ) (Env.valid_t_vars env i)
+    | Remove (i,x)    -> Iter.map (fun i -> Remove (i,x)   ) (Env.valid_t_vars env i)
+    | Find (i,x)      -> Iter.map (fun i -> Find (i,x)     ) (Env.valid_t_vars env i)
+    | Find_opt (i,x)  -> Iter.map (fun i -> Find_opt (i,x) ) (Env.valid_t_vars env i)
+    | Find_all (i,x)  -> Iter.map (fun i -> Find_all (i,x) ) (Env.valid_t_vars env i)
+    | Replace (i,x,y) -> Iter.map (fun i -> Replace (i,x,y)) (Env.valid_t_vars env i)
+    | Mem (i,x)       -> Iter.map (fun i -> Mem (i,x)      ) (Env.valid_t_vars env i)
+    | Length i        -> Iter.map (fun i -> Length i       ) (Env.valid_t_vars env i)
 
   type res =
     | RClear
diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml
index f4a53a59d..31b41ca3e 100644
--- a/src/lazy/lin_tests.ml
+++ b/src/lazy/lin_tests.ml
@@ -63,11 +63,11 @@ struct
   let shrink_cmd = Shrink.nil
 
   let fix_cmd env = function
-    | Force i       -> Iter.map (fun i -> Force i      ) (Env.valid_states env i)
-    | Force_val i   -> Iter.map (fun i -> Force_val i  ) (Env.valid_states env i)
-    | Is_val i      -> Iter.map (fun i -> Is_val i     ) (Env.valid_states env i)
-    | Map (i,f)     -> Iter.map (fun i -> Map (i,f)    ) (Env.valid_states env i)
-    | Map_val (i,f) -> Iter.map (fun i -> Map_val (i,f)) (Env.valid_states env i)
+    | Force i       -> Iter.map (fun i -> Force i      ) (Env.valid_t_vars env i)
+    | Force_val i   -> Iter.map (fun i -> Force_val i  ) (Env.valid_t_vars env i)
+    | Is_val i      -> Iter.map (fun i -> Is_val i     ) (Env.valid_t_vars env i)
+    | Map (i,f)     -> Iter.map (fun i -> Map (i,f)    ) (Env.valid_t_vars env i)
+    | Map_val (i,f) -> Iter.map (fun i -> Map_val (i,f)) (Env.valid_t_vars env i)
 
   type t = int Lazy.t
 
diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml
index 1088c238f..138974e84 100644
--- a/src/neg_tests/lin_tests_common.ml
+++ b/src/neg_tests/lin_tests_common.ml
@@ -53,11 +53,11 @@ module RConf_int = struct
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
 
   let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_states env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_states env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_states env i)
-    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_states env i)
-    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_states env i)
+    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_t_vars env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
+    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_t_vars env i)
+    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_t_vars env i)
 
   type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
@@ -105,11 +105,11 @@ module RConf_int64 = struct
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
 
   let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_states env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_states env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_states env i)
-    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_states env i)
-    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_states env i)
+    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_t_vars env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
+    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_t_vars env i)
+    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_t_vars env i)
 
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
@@ -161,8 +161,8 @@ struct
     | Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
 
   let fix_cmd env = function
-    | Add_node (i,x) -> Iter.map (fun i -> Add_node (i,x)) (Lin.Env.valid_states env i)
-    | Member (i,x)   -> Iter.map (fun i -> Member (i,x)  ) (Lin.Env.valid_states env i)
+    | Add_node (i,x) -> Iter.map (fun i -> Add_node (i,x)) (Lin.Env.valid_t_vars env i)
+    | Member (i,x)   -> Iter.map (fun i -> Member (i,x)  ) (Lin.Env.valid_t_vars env i)
 
   type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
 
diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml
index ce5481ad4..82762698f 100644
--- a/src/queue/lin_tests.ml
+++ b/src/queue/lin_tests.ml
@@ -48,15 +48,15 @@ module Spec =
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
     let fix_cmd env = function
-      | Add (i,x)    -> Iter.map (fun i -> Add (i,x)   ) (Env.valid_states env i)
-      | Take i       -> Iter.map (fun i -> Take i      ) (Env.valid_states env i)
-      | Take_opt i   -> Iter.map (fun i -> Take_opt i  ) (Env.valid_states env i)
-      | Peek i       -> Iter.map (fun i -> Peek i      ) (Env.valid_states env i)
-      | Peek_opt i   -> Iter.map (fun i -> Peek_opt i  ) (Env.valid_states env i)
-      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_states env i)
-      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_states env i)
-      | Fold (i,x,y) -> Iter.map (fun i -> Fold (i,x,y)) (Env.valid_states env i)
-      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_states env i)
+      | Add (i,x)    -> Iter.map (fun i -> Add (i,x)   ) (Env.valid_t_vars env i)
+      | Take i       -> Iter.map (fun i -> Take i      ) (Env.valid_t_vars env i)
+      | Take_opt i   -> Iter.map (fun i -> Take_opt i  ) (Env.valid_t_vars env i)
+      | Peek i       -> Iter.map (fun i -> Peek i      ) (Env.valid_t_vars env i)
+      | Peek_opt i   -> Iter.map (fun i -> Peek_opt i  ) (Env.valid_t_vars env i)
+      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_t_vars env i)
+      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_t_vars env i)
+      | Fold (i,x,y) -> Iter.map (fun i -> Fold (i,x,y)) (Env.valid_t_vars env i)
+      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_t_vars env i)
 
     type res =
       | RAdd
diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml
index 7b00a5d2b..486a598aa 100644
--- a/src/stack/lin_tests.ml
+++ b/src/stack/lin_tests.ml
@@ -49,15 +49,15 @@ module Spec =
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
     let fix_cmd env = function
-      | Push (i,x)   -> Iter.map (fun i -> Push (i,x)  ) (Env.valid_states env i)
-      | Pop i        -> Iter.map (fun i -> Pop i       ) (Env.valid_states env i)
-      | Pop_opt i    -> Iter.map (fun i -> Pop_opt i   ) (Env.valid_states env i)
-      | Top i        -> Iter.map (fun i -> Top i       ) (Env.valid_states env i)
-      | Top_opt i    -> Iter.map (fun i -> Top_opt i   ) (Env.valid_states env i)
-      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_states env i)
-      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_states env i)
-      | Fold (i,f,x) -> Iter.map (fun i -> Fold (i,f,x)) (Env.valid_states env i)
-      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_states env i)
+      | Push (i,x)   -> Iter.map (fun i -> Push (i,x)  ) (Env.valid_t_vars env i)
+      | Pop i        -> Iter.map (fun i -> Pop i       ) (Env.valid_t_vars env i)
+      | Pop_opt i    -> Iter.map (fun i -> Pop_opt i   ) (Env.valid_t_vars env i)
+      | Top i        -> Iter.map (fun i -> Top i       ) (Env.valid_t_vars env i)
+      | Top_opt i    -> Iter.map (fun i -> Top_opt i   ) (Env.valid_t_vars env i)
+      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_t_vars env i)
+      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_t_vars env i)
+      | Fold (i,f,x) -> Iter.map (fun i -> Fold (i,f,x)) (Env.valid_t_vars env i)
+      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_t_vars env i)
 
     type res =
       | RPush

From c1c122043b5ea7da5d81085391b2e1a99a39902c Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 13 Oct 2022 18:57:13 +0200
Subject: [PATCH 38/57] eliminate a few let opens

---
 lib/lin_api.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index 1f67c77b0..bfcf8c60c 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -278,13 +278,11 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
   let rec fix_args
     : type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
     fun env args ->
-    let open Lin in
     let open QCheck in
-    let open Args in
-    let fn_state i args = FnState (i,args) in
+    let fn_state i args = Args.FnState (i,args) in
     match args with
-    | FnState (i, args) -> Iter.(map fn_state (Env.valid_t_vars env i) <*> fix_args env args)
-    | Fn (x, args)      -> Iter.map (fun args -> Fn (x, args)) (fix_args env args)
+    | FnState (i, args) -> Iter.(map fn_state (Lin.Env.valid_t_vars env i) <*> fix_args env args)
+    | Fn (x, args)      -> Iter.map (fun args -> Args.Fn (x, args)) (fix_args env args)
     | _                 -> Iter.return args
 
   let fix_cmd env (Cmd (name,args,rty,print,shrink,f)) =

From aedc4265b86f31e1e9a7cf036f1b9b1f1f8e2742 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <jan@tarides.com>
Date: Thu, 13 Oct 2022 19:07:41 +0200
Subject: [PATCH 39/57] Update out-of-date `run` comment in lib/lin.ml

Co-authored-by: shym <shym@users.noreply.github.com>
---
 lib/lin.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index b7b10e241..fb59208b6 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -79,7 +79,7 @@ module type CmdSpec = sig
       e.g., for closing sockets, files, or resetting global parameters *)
 
   val run : (Var.t option * cmd) -> t array -> res
-  (** [run (opt,c) t] should interpret the command [c] over the system under test [t] (typically side-effecting).
+  (** [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
 

From 0591d4474a0263c482a273e7f32de1b8a372eeb4 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 13 Oct 2022 21:54:24 +0200
Subject: [PATCH 40/57] forgot to rename in internal/cleanup.ml

---
 src/internal/cleanup_lin.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/internal/cleanup_lin.ml b/src/internal/cleanup_lin.ml
index 98ffe6eef..b1bb61952 100644
--- a/src/internal/cleanup_lin.ml
+++ b/src/internal/cleanup_lin.ml
@@ -25,9 +25,9 @@ struct
   let shrink_cmd = Shrink.nil
 
   let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Lin.Env.valid_states env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Lin.Env.valid_states env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Lin.Env.valid_states env i)
+    | Get i     -> Iter.map (fun i -> Get i    ) (Lin.Env.valid_t_vars env i)
+    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Lin.Env.valid_t_vars env i)
+    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Lin.Env.valid_t_vars env i)
 
   let init () = (ref Inited, ref 0)
 

From 18cda2ee7bef0c78af52adf0ab63c58a3ae24b6e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 14 Oct 2022 17:28:23 +0200
Subject: [PATCH 41/57] remove duplicate Bytes.make

---
 src/bytes/lin_tests_dsl.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 74e54dfb5..9cda0a4d7 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -11,7 +11,6 @@ module BConf = struct
 (*let int = int_bound 10*)
 
   let api = [
-    val_ "Bytes.make"        Bytes.make        (int @-> char @-> returning_ t);
     val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
     val_ "Bytes.set"         Bytes.set         (t @-> int @-> char @-> returning_or_exc unit);

From 6670815b8c948e9f3c2610399e83d8a1a9bf70eb Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 14 Oct 2022 17:31:46 +0200
Subject: [PATCH 42/57] restore init size

---
 src/bytes/lin_tests_dsl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 9cda0a4d7..77227216f 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -3,7 +3,7 @@
 (* ********************************************************************** *)
 module BConf = struct
   type t = Bytes.t
-  let init () = Bytes.make 8 '0'
+  let init () = Bytes.make 42 '0'
   let cleanup _ = ()
 
   open Lin_api

From 64251294e65d908049edab946acf2fed7af7c60f Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 14 Oct 2022 17:50:38 +0200
Subject: [PATCH 43/57] reenable Bytes.escaped which has been patched

---
 src/bytes/lin_tests_dsl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 77227216f..8b3f11873 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -24,7 +24,7 @@ module BConf = struct
     val_freq 2 "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
     val_freq 2 "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
     val_ "Bytes.trim"        Bytes.trim        (t @-> returning_ t);
- (* val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t); *)
+    val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t);
     val_ "Bytes.index"       Bytes.index       (t @-> char @-> returning_or_exc int);
     val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int)]
 end

From 128911980185607f63191df2098ca7677b191b3a Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 14 Oct 2022 18:29:45 +0200
Subject: [PATCH 44/57] faster valid_t_vars shrinker/iterator, using clever
 array-indexing from @shym to shrink towards t0

remove commented out line
---
 lib/lin.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index fb59208b6..6fff0567f 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -32,7 +32,10 @@ struct
   let valid_t_vars env v =
     match List.filter (fun v' -> v' <= v) env with
     | v' :: _ when v' = v -> Iter.return v
-    | env'                -> Iter.of_list env'
+    | env'                ->
+      let a = Array.of_list env' in
+      let length = Array.length a in
+      Iter.map (fun i -> a.(length - i - 1)) (Shrink.int length)
 end
 
 module type CmdSpec = sig

From 5a6ad691295a8fecec50c1965b23ae7a724ac94e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 20 Oct 2022 22:01:46 +0200
Subject: [PATCH 45/57] update print signature

---
 lib/lin_api.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/lin_api.mli b/lib/lin_api.mli
index c6128ccad..dd99e0b3c 100644
--- a/lib/lin_api.mli
+++ b/lib/lin_api.mli
@@ -170,7 +170,7 @@ val print_result :
 (** [print_result pa pb] creates a to-string function for a [(a,b) result] type
     given two to-string functions for [a]s and [b]s, respectively. *)
 
-val print : ('a, 'c, 's, 'comb) ty -> 'a -> string
+val print : ('a, 'c, 's, combinable) ty -> 'a -> string
 (** Given a description of type ['a], print a value of type ['a]. *)
 
 val equal : ('a, deconstructible, 's, 'comb) ty -> 'a -> 'a -> bool

From 7104612277248d18c35747f3802bad00313ce67c Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 20 Oct 2022 22:11:01 +0200
Subject: [PATCH 46/57] update returning_ and returning_or_exc_ signatures

---
 lib/lin_api.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/lin_api.mli b/lib/lin_api.mli
index dd99e0b3c..446bfb42d 100644
--- a/lib/lin_api.mli
+++ b/lib/lin_api.mli
@@ -196,11 +196,11 @@ val returning_or_exc :
 (** [returning_or_exc comb] indicates that the function may raise an exception and that the return type is [comb].
     In either case the result is compared to the corresponding sequential result and hence [comb] has to be [deconstructible]. *)
 
-val returning_ : ('a, 'b, 'c, combinable) ty -> ('a, unit, 'c) Fun.fn
+val returning_ : ('a, 'b, 'c, 'd) ty -> ('a, unit, 'c) Fun.fn
 (** [returning comb] indicates the return type [comb] which is ignored. *)
 
 val returning_or_exc_ :
-  ('a, 'b, 'c, combinable) ty -> ('a, (unit, exn) result, 'c) Fun.fn
+  ('a, 'b, 'c, 'd) ty -> ('a, (unit, exn) result, 'c) Fun.fn
 (** [returning_or_exc comb] indicates that the function may raise an exception and that the return type is [comb].
     In both cases the result is ignored. *)
 

From 5e460ad6110babf8a646a7cfda9ffa7e77deaa5c Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 28 Oct 2022 10:24:21 +0200
Subject: [PATCH 47/57] clarify returning_ combinator semantics

---
 lib/lin_api.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/lib/lin_api.mli b/lib/lin_api.mli
index 446bfb42d..28b1924b6 100644
--- a/lib/lin_api.mli
+++ b/lib/lin_api.mli
@@ -197,12 +197,13 @@ val returning_or_exc :
     In either case the result is compared to the corresponding sequential result and hence [comb] has to be [deconstructible]. *)
 
 val returning_ : ('a, 'b, 'c, 'd) ty -> ('a, unit, 'c) Fun.fn
-(** [returning comb] indicates the return type [comb] which is ignored. *)
+(** [returning comb] indicates that the return type is [comb] and that it should
+    not be compared to the corresponding sequential result. *)
 
 val returning_or_exc_ :
   ('a, 'b, 'c, 'd) ty -> ('a, (unit, exn) result, 'c) Fun.fn
 (** [returning_or_exc comb] indicates that the function may raise an exception and that the return type is [comb].
-    In both cases the result is ignored. *)
+    In both cases the result is not compared to the corresponding sequential result. *)
 
 val ( @-> ) :
   ('a, constructible, 'b, 'c) ty ->

From cf7312acd93818d45cfbe4512954dedee6e2f017 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 31 Oct 2022 18:00:15 +0100
Subject: [PATCH 48/57] attempt to speed-up tvar-index shrinking

---
 lib/lin.ml | 30 ++++++++++++++++++++++++------
 1 file changed, 24 insertions(+), 6 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 6fff0567f..de89eb0e4 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -30,6 +30,7 @@ struct
   type t = Var.t list
   let gen_t_var env = Gen.oneofl env
   let valid_t_vars env v =
+    if v = 0 then Iter.empty else
     match List.filter (fun v' -> v' <= v) env with
     | v' :: _ when v' = v -> Iter.return v
     | env'                ->
@@ -135,7 +136,11 @@ module MakeDomThr(Spec : CmdSpec)
       | [] -> Iter.return []
       | (opt,cmd) :: cmds ->
           let env' = Option.fold ~none:env ~some:(fun i -> i::env) opt in
-          Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)
+          (*Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)*)
+          Iter.(
+            (map (fun cmd  -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd))
+            <+>
+            (map (fun cmds -> (opt,cmd)::cmds) (aux env' cmds)))
     in aux env cmds
 
   (* Note that the result is built in reverse (ie should be
@@ -151,25 +156,38 @@ module MakeDomThr(Spec : CmdSpec)
     (* Shrinking heuristic:
        First reduce the cmd list sizes as much as possible, since the interleaving
        is most costly over long cmd lists. *)
+    (*
     let concat_map f it = flatten (map f it) in
     let fix_seq seq =
+*)
       let seq_env = extract_env [0] seq in
+(*
       let triple seq p1 p2 = (seq,p1,p2) in
       map triple (fix_cmds [0] seq) <*> fix_cmds seq_env p1 <*> fix_cmds seq_env p2
     in
     let seq_env = extract_env [0] seq in
-
-    concat_map fix_seq (Shrink.list_spine seq)
-    <+>
+    *)
+(*  concat_map fix_seq (Shrink.list_spine seq)
+    <+> *)
     (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
     <+>
     (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
     <+>
-    concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)
+    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
+    <+>
+    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
+    (*concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)*)
     <+>
-    concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)
+    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
+    (*concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)*)
     <+>
     (* Secondly reduce the cmd data of individual list elements *)
+    (map (fun seq -> (seq,p1,p2)) (fix_cmds [0] seq))
+    <+>
+    (map (fun p1  -> (seq,p1,p2)) (fix_cmds seq_env p1))
+    <+>
+    (map (fun p2  -> (seq,p1,p2)) (fix_cmds seq_env p2))
+    <+>
     (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
     <+>
     (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems shrink_cmd p1))

From 7dbb92a8a83d8bd3b3920469b9c8eae718d41c78 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 1 Nov 2022 10:27:10 +0100
Subject: [PATCH 49/57] simplifed approach: rename only invalid t_vars to 0 -
 as they represent

---
 lib/lin.ml | 32 +++++++++-----------------------
 1 file changed, 9 insertions(+), 23 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index de89eb0e4..353c903f6 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -30,6 +30,8 @@ struct
   type t = Var.t list
   let gen_t_var env = Gen.oneofl env
   let valid_t_vars env v =
+    if List.mem v env then Iter.return v else Iter.return 0
+(*
     if v = 0 then Iter.empty else
     match List.filter (fun v' -> v' <= v) env with
     | v' :: _ when v' = v -> Iter.return v
@@ -37,6 +39,7 @@ struct
       let a = Array.of_list env' in
       let length = Array.length a in
       Iter.map (fun i -> a.(length - i - 1)) (Shrink.int length)
+*)
 end
 
 module type CmdSpec = sig
@@ -136,11 +139,7 @@ module MakeDomThr(Spec : CmdSpec)
       | [] -> Iter.return []
       | (opt,cmd) :: cmds ->
           let env' = Option.fold ~none:env ~some:(fun i -> i::env) opt in
-          (*Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)*)
-          Iter.(
-            (map (fun cmd  -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd))
-            <+>
-            (map (fun cmds -> (opt,cmd)::cmds) (aux env' cmds)))
+          Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)
     in aux env cmds
 
   (* Note that the result is built in reverse (ie should be
@@ -156,38 +155,25 @@ module MakeDomThr(Spec : CmdSpec)
     (* Shrinking heuristic:
        First reduce the cmd list sizes as much as possible, since the interleaving
        is most costly over long cmd lists. *)
-    (*
     let concat_map f it = flatten (map f it) in
     let fix_seq seq =
-*)
       let seq_env = extract_env [0] seq in
-(*
       let triple seq p1 p2 = (seq,p1,p2) in
       map triple (fix_cmds [0] seq) <*> fix_cmds seq_env p1 <*> fix_cmds seq_env p2
     in
     let seq_env = extract_env [0] seq in
-    *)
-(*  concat_map fix_seq (Shrink.list_spine seq)
-    <+> *)
+
+    concat_map fix_seq (Shrink.list_spine seq)
+    <+>
     (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
     <+>
     (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
     <+>
-    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
-    <+>
-    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
-    (*concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)*)
+    concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)
     <+>
-    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
-    (*concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)*)
+    concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)
     <+>
     (* Secondly reduce the cmd data of individual list elements *)
-    (map (fun seq -> (seq,p1,p2)) (fix_cmds [0] seq))
-    <+>
-    (map (fun p1  -> (seq,p1,p2)) (fix_cmds seq_env p1))
-    <+>
-    (map (fun p2  -> (seq,p1,p2)) (fix_cmds seq_env p2))
-    <+>
     (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
     <+>
     (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems shrink_cmd p1))

From d2ca78d37edefc856e5fcc603fab5d61d4eb0f77 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 8 Nov 2022 16:42:10 +0100
Subject: [PATCH 50/57] shrinker improvements

---
 lib/lin.ml     | 114 ++++++++++++++++++++++++-------------------------
 lib/lin_api.ml |  46 ++++++++++++--------
 2 files changed, 84 insertions(+), 76 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 353c903f6..cd4b6b58b 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -7,7 +7,6 @@ module Var : sig
   val reset : unit -> unit
   val pp : Format.formatter -> t -> unit
   val show : t -> string
-  val shrink : t Shrink.t
 end =
 struct
   type t = int
@@ -18,7 +17,6 @@ struct
     (fun () -> counter := 0)
   let show v = Format.sprintf "t%i" v
   let pp fmt v = Format.fprintf fmt "%s" (show v)
-  let shrink = Shrink.int
 end
 
 module Env : sig
@@ -30,16 +28,8 @@ struct
   type t = Var.t list
   let gen_t_var env = Gen.oneofl env
   let valid_t_vars env v =
-    if List.mem v env then Iter.return v else Iter.return 0
-(*
     if v = 0 then Iter.empty else
-    match List.filter (fun v' -> v' <= v) env with
-    | v' :: _ when v' = v -> Iter.return v
-    | env'                ->
-      let a = Array.of_list env' in
-      let length = Array.length a in
-      Iter.map (fun i -> a.(length - i - 1)) (Shrink.int length)
-*)
+      Iter.of_list (List.rev (List.filter (fun v' -> v' < v) env))
 end
 
 module type CmdSpec = sig
@@ -57,18 +47,13 @@ module type CmdSpec = sig
       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 Shrink.t
+  val shrink_cmd : Env.t -> cmd Shrink.t
   (** A command shrinker.
-      To a first approximation you can use [Shrink.nil]. *)
+      It accepts the current environment as its argument.
+      To a first approximation you can use [fun _env -> Shrink.nil]. *)
 
-  val fix_cmd : Env.t -> cmd -> cmd Iter.t
-  (** A command fixer.
-      Fixes the given [cmd] so that it uses only states in the given
-      [Env.t]. If the initial [cmd] used a state that is no longer
-      available, it should iterate over all the lesser states
-      available in [Env.t]. If all the necessary states are still
-      available, it should generate a one-element iterator.
-      Can assume that [Env.t] is sorted in decreasing order. *)
+  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 *)
@@ -129,19 +114,6 @@ module MakeDomThr(Spec : CmdSpec)
 
   let gen_cmds_size env size_gen = Gen.sized_size size_gen (gen_cmds env)
 
-  let shrink_cmd (opt,c) = Iter.map (fun c -> opt,c) (Spec.shrink_cmd c)
-
-  (* Note: the [env] fed to [Spec.fix_cmd] are in reverse (ie should
-     be _decreasing_) order *)
-  let fix_cmds env cmds =
-    let rec aux env cmds =
-      match cmds with
-      | [] -> Iter.return []
-      | (opt,cmd) :: cmds ->
-          let env' = Option.fold ~none:env ~some:(fun i -> i::env) opt in
-          Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)
-    in aux env cmds
-
   (* Note that the result is built in reverse (ie should be
      _decreasing_) order *)
   let rec extract_env env cmds =
@@ -150,45 +122,71 @@ module MakeDomThr(Spec : CmdSpec)
     | (Some i, _) :: cmds -> extract_env (i::env) cmds
     | (None,   _) :: cmds -> extract_env     env  cmds
 
+  let cmds_use_var var cmds =
+    List.exists (fun (_,c) -> Spec.cmd_uses_var var c) cmds
+
+  let ctx_doesnt_use_var _var = false
+
+  let rec shrink_cmd_list_spine cmds ctx_uses_var = match cmds with
+    | [] -> Iter.empty
+    | c::cs ->
+      let open Iter in
+      (match fst c with
+       | None -> (* shrink tail first as fewer other vars should depend on it *)
+         (map (fun cs -> c::cs) (shrink_cmd_list_spine cs ctx_uses_var)
+          <+>
+          return cs) (* not a t-assignment, so try without it *)
+       | Some i -> (* shrink tail first as fewer other vars should depend on it *)
+         (map (fun cs -> c::cs) (shrink_cmd_list_spine cs ctx_uses_var)
+         <+>
+         if cmds_use_var i cs || ctx_uses_var i
+         then empty
+         else return cs)) (* t_var not used, so try without it *)
+
+  let rec shrink_individual_cmds env cmds = match cmds with
+    | [] -> Iter.empty
+    | (opt,cmd) :: cmds ->
+      let env' = match opt with None -> env | Some i -> i::env in
+      let open Iter in
+      map (fun cmds -> (opt,cmd)::cmds) (shrink_individual_cmds env' cmds)
+      <+>
+      map (fun cmd -> (opt,cmd)::cmds) (Spec.shrink_cmd env cmd)
+
   let shrink_triple' (seq,p1,p2) =
     let open Iter in
     (* Shrinking heuristic:
        First reduce the cmd list sizes as much as possible, since the interleaving
        is most costly over long cmd lists. *)
-    let concat_map f it = flatten (map f it) in
-    let fix_seq seq =
-      let seq_env = extract_env [0] seq in
-      let triple seq p1 p2 = (seq,p1,p2) in
-      map triple (fix_cmds [0] seq) <*> fix_cmds seq_env p1 <*> fix_cmds seq_env p2
-    in
-    let seq_env = extract_env [0] seq in
-
-    concat_map fix_seq (Shrink.list_spine seq)
+    map (fun seq -> (seq,p1,p2)) (shrink_cmd_list_spine seq (fun var -> cmds_use_var var p1 || cmds_use_var var p2))
     <+>
-    (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
+    map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list_spine p1 ctx_doesnt_use_var)
     <+>
-    (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
+    map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list_spine p2 ctx_doesnt_use_var)
     <+>
-    concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)
+    (fun yield -> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) yield)
     <+>
-    concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)
+    (fun yield -> (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s)) yield)
     <+>
     (* Secondly reduce the cmd data of individual list elements *)
-    (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
-    <+>
-    (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems shrink_cmd p1))
+    (fun yield ->
+       let seq_env = extract_env [0] seq in (* only extract_env if needed *)
+       (Iter.map (fun p1  -> (seq,p1,p2)) (shrink_individual_cmds (*(extract_env [0] seq)*) seq_env p1)
+        <+>
+        Iter.map (fun p2  -> (seq,p1,p2)) (shrink_individual_cmds (*(extract_env [0] seq)*) seq_env p2))
+         yield)
     <+>
-    (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems shrink_cmd p2))
+    Iter.map (fun seq -> (seq,p1,p2)) (shrink_individual_cmds [0] seq)
 
   let shrink_triple (size,t) =
     Iter.map (fun t -> (size,t)) (shrink_triple' t)
 
+
   let show_cmd (opt,c) = match opt with
     | None   -> Spec.show_cmd c
     | Some v -> Printf.sprintf "let %s = %s" (Var.show v) (Spec.show_cmd c)
 
   let init_cmd = "let t0 = init ()"
-  let init_cmd_ret = init_cmd ^ "  : ()"
+  let init_cmd_ret = init_cmd ^ " : ()"
 
   let arb_cmds_par seq_len par_len =
     let gen_triple st =
@@ -344,13 +342,13 @@ module Make(Spec : CmdSpec)
          [(3,Gen.return (None,SchedYield));
           (5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
 
-    let fix_cmd env = function
-      | SchedYield -> Iter.return SchedYield
-      | UserCmd cmd -> Iter.map (fun c -> UserCmd c) (Spec.fix_cmd env cmd)
-
-    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
 
diff --git a/lib/lin_api.ml b/lib/lin_api.ml
index bfcf8c60c..dfff2c1f6 100644
--- a/lib/lin_api.ml
+++ b/lib/lin_api.ml
@@ -245,9 +245,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
       | Fun.Ret_ignore _ty -> Shrink.nil
       | Fun.(Fn (State, fdesc_rem)) ->
           (function (Args.FnState (index,args)) ->
-            Iter.(map (fun index -> Args.FnState (index,args)) (Lin.Var.shrink index)
-                  <+>
-                  map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args))
+            Iter.map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args)
                   | _ -> failwith "FnState: should not happen")
       | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
           (match arg_arb.shrink with
@@ -256,10 +254,10 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
                   Iter.map (fun args -> Args.Fn (a,args)) (gen_shrinker_of_desc fdesc_rem args)
                        | _ -> failwith "Fn/None: should not happen")
            | Some shrk ->
-               Iter.(function (Args.Fn (a,args)) ->
-                   (map (fun a -> Args.Fn (a,args)) (shrk a))
-                   <+>
+               Iter.(function (Args.Fn (a,args)) -> (* heuristic: shrink last args first *)
                    (map (fun args -> Args.Fn (a,args)) (gen_shrinker_of_desc fdesc_rem args))
+                   <+>
+                   (map (fun a -> Args.Fn (a,args)) (shrk a))
                             | _ -> failwith "Fn/Some: should not happen"))
 
   let api gen_t_var =
@@ -275,21 +273,33 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
 
   let show_cmd (Cmd (_,args,_,print,_,_)) = print args
 
-  let rec fix_args
-    : type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
-    fun env args ->
-    let open QCheck in
-    let fn_state i args = Args.FnState (i,args) in
+  let rec args_use_var
+    : type a r. Lin.Var.t -> (a, r) Args.args -> bool =
+    fun var args ->
     match args with
-    | FnState (i, args) -> Iter.(map fn_state (Lin.Env.valid_t_vars env i) <*> fix_args env args)
-    | Fn (x, args)      -> Iter.map (fun args -> Args.Fn (x, args)) (fix_args env args)
-    | _                 -> Iter.return args
+    | FnState (i, args') -> i=var || args_use_var var args'
+    | Fn (_, args')      -> args_use_var var args'
+    | _                  -> false
 
-  let fix_cmd env (Cmd (name,args,rty,print,shrink,f)) =
-    QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (fix_args env args)
+  let cmd_uses_var var (Cmd (_,args,_,_,_,_)) = args_use_var var args
 
-  let shrink_cmd (Cmd (name,args,rty,print,shrink,f)) =
-    QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink args)
+  let rec shrink_t_vars
+    : type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
+    fun env args ->
+    match args with
+    | FnState (i,args') ->
+      QCheck.Iter.(map (fun i -> Args.FnState (i,args')) (Lin.Env.valid_t_vars env i)
+                   <+>
+                   map (fun args' -> Args.FnState (i, args')) (shrink_t_vars env args'))
+    | Fn (a,args') -> QCheck.Iter.map (fun args' -> Args.Fn (a, args')) (shrink_t_vars env args')
+    | _            -> QCheck.Iter.empty
+
+  let shrink_cmd env (Cmd (name,args,rty,print,shrink,f)) =
+    QCheck.Iter.( (* reduce t-vars first as it can trigger removal of other cmds *)
+      map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink_t_vars env args)
+      <+> (* only secondly reduce char/int/... arguments *)
+      map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink args)
+    )
 
   (* Unsafe if called on two [res] whose internal values are of different
      types. *)

From affe328787fe79c189dccabbd0cf8220e99c2f1e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 8 Nov 2022 17:21:34 +0100
Subject: [PATCH 51/57] update lin_test.mls to interface

---
 src/array/lin_tests.ml            | 50 +++++++++++++++----------------
 src/atomic/lin_tests.ml           | 22 +++++++-------
 src/bytes/lin_tests_dsl.ml        |  1 +
 src/hashtbl/lin_tests.ml          | 24 +++++++--------
 src/kcas/lin_tests.ml             | 26 ++++++++++++++--
 src/lazy/lin_tests.ml             | 14 ++++-----
 src/neg_tests/lin_tests_common.ml | 36 +++++++++++-----------
 src/queue/lin_tests.ml            | 22 +++++++-------
 src/stack/lin_tests.ml            | 22 +++++++-------
 9 files changed, 120 insertions(+), 97 deletions(-)

diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml
index 0e8eb793b..6dd395c86 100644
--- a/src/array/lin_tests.ml
+++ b/src/array/lin_tests.ml
@@ -42,34 +42,34 @@ struct
         map  (fun v -> (None, To_seq v)) gen_var;
       ])
 
-  let shrink_cmd c = match c with
-    | Length v     -> Iter.map (fun v -> Length v)    (Var.shrink v)
-    | Get (v,i)    -> Iter.map (fun v -> Get (v,i))   (Var.shrink v)
-    | Set (v,i,c)  -> Iter.map (fun v -> Set (v,i,c)) (Var.shrink v)
+  let shrink_cmd env c = match c with
+    | Length v     -> Iter.map (fun v -> Length v)    (Env.valid_t_vars env v)
+    | Get (v,i)    -> Iter.map (fun v -> Get (v,i))   (Env.valid_t_vars env v)
+    | Set (v,i,c)  -> Iter.map (fun v -> Set (v,i,c)) (Env.valid_t_vars env v)
     | Append (v,w) ->
-      Iter.(map (fun v -> Append (v,w)) (Var.shrink v)
+      Iter.(map (fun v -> Append (v,w)) (Env.valid_t_vars env v)
             <+>
-            map (fun w -> Append (v,w)) (Var.shrink w))
-    | Sub (v,i,l) -> Iter.map (fun v -> Sub (v,i,l)) (Var.shrink v)
-    | Copy v      -> Iter.map (fun v -> Copy v)      (Var.shrink v)
-    | Fill (v,i,l,c) -> Iter.map (fun v -> Fill (v,i,l,c)) (Var.shrink v)
-    | To_list v   -> Iter.map (fun v -> To_list v)   (Var.shrink v)
-    | Mem (v,c)   -> Iter.map (fun v -> Mem (v,c))   (Var.shrink v)
-    | Sort v      -> Iter.map (fun v -> Sort v)      (Var.shrink v)
-    | To_seq v    -> Iter.map (fun v -> To_seq v)    (Var.shrink v)
+            map (fun w -> Append (v,w)) (Env.valid_t_vars env w))
+    | Sub (v,i,l) -> Iter.map (fun v -> Sub (v,i,l)) (Env.valid_t_vars env v)
+    | Copy v      -> Iter.map (fun v -> Copy v)      (Env.valid_t_vars env v)
+    | Fill (v,i,l,c) -> Iter.map (fun v -> Fill (v,i,l,c)) (Env.valid_t_vars env v)
+    | To_list v   -> Iter.map (fun v -> To_list v)   (Env.valid_t_vars env v)
+    | Mem (v,c)   -> Iter.map (fun v -> Mem (v,c))   (Env.valid_t_vars env v)
+    | Sort v      -> Iter.map (fun v -> Sort v)      (Env.valid_t_vars env v)
+    | To_seq v    -> Iter.map (fun v -> To_seq v)    (Env.valid_t_vars env v)
 
-  let fix_cmd env = function
-    | Length i       -> Iter.map (fun i -> Length i      ) (Env.valid_t_vars env i)
-    | Get (i,x)      -> Iter.map (fun i -> Get (i,x)     ) (Env.valid_t_vars env i)
-    | Set (i,x,z)    -> Iter.map (fun i -> Set (i,x,z)   ) (Env.valid_t_vars env i)
-    | Sub (i,x,y)    -> Iter.map (fun i -> Sub (i,x,y)   ) (Env.valid_t_vars env i)
-    | Copy i         -> Iter.map (fun i -> Copy i        ) (Env.valid_t_vars env i)
-    | Fill (i,x,y,z) -> Iter.map (fun i -> Fill (i,x,y,z)) (Env.valid_t_vars env i)
-    | To_list i      -> Iter.map (fun i -> To_list i     ) (Env.valid_t_vars env i)
-    | Mem (i,z)      -> Iter.map (fun i -> Mem (i,z)     ) (Env.valid_t_vars env i)
-    | Sort i         -> Iter.map (fun i -> Sort i        ) (Env.valid_t_vars env i)
-    | To_seq i       -> Iter.map (fun i -> To_seq i      ) (Env.valid_t_vars env i)
-    | Append (i,j)   -> Iter.(map (fun i j -> Append (i,j)) (Env.valid_t_vars env i) <*> (Env.valid_t_vars env j))
+  let cmd_uses_var v c = match c with
+    | Length i
+    | Get (i,_)
+    | Set (i,_,_)
+    | Sub (i,_,_)
+    | Copy i
+    | Fill (i,_,_,_)
+    | To_list i
+    | Mem (i,_)
+    | Sort i
+    | To_seq i -> i=v
+    | Append (i,j) -> i=v || j=v
 
   open Util
   (*let pp_exn = Util.pp_exn*)
diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml
index 76dd5b25c..56d733614 100644
--- a/src/atomic/lin_tests.ml
+++ b/src/atomic/lin_tests.ml
@@ -30,17 +30,17 @@ struct
         map  (fun t ->     (None, Decr t)) gen_var;
       ])
 
-  let shrink_cmd = Shrink.nil
-
-  let fix_cmd env = function
-    | Make x as cmd           -> Iter.return cmd
-    | Get i                   -> Iter.map (fun i -> Get i                  ) (Env.valid_t_vars env i)
-    | Set (i,x)               -> Iter.map (fun i -> Set (i,x)              ) (Env.valid_t_vars env i)
-    | Exchange (i,x)          -> Iter.map (fun i -> Exchange (i,x)         ) (Env.valid_t_vars env i)
-    | Compare_and_set (i,x,y) -> Iter.map (fun i -> Compare_and_set (i,x,y)) (Env.valid_t_vars env i)
-    | Fetch_and_add (i,x)     -> Iter.map (fun i -> Fetch_and_add (i,x)    ) (Env.valid_t_vars env i)
-    | Incr i                  -> Iter.map (fun i -> Incr i                 ) (Env.valid_t_vars env i)
-    | Decr i                  -> Iter.map (fun i -> Decr i                 ) (Env.valid_t_vars env i)
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Make _ -> false
+    | Get i
+    | Set (i,_)
+    | Exchange (i,_)
+    | Compare_and_set (i,_,_)
+    | Fetch_and_add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res =
     | RMake of unit
diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 8b3f11873..098ba5cc3 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -8,6 +8,7 @@ module BConf = struct
 
   open Lin_api
   let int = nat_small
+  let string = string_small
 (*let int = int_bound 10*)
 
   let api = [
diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml
index ed66564fc..9af1da25b 100644
--- a/src/hashtbl/lin_tests.ml
+++ b/src/hashtbl/lin_tests.ml
@@ -35,7 +35,7 @@ struct
         map2 (fun v c -> None,Mem (v,c)) gen_var gen_char;
         map  (fun v -> None,Length v) gen_var;
       ])
-  let shrink_cmd c = match c with
+  let shrink_cmd _env c = match c with
     | Clear _ -> Iter.empty
     | Copy _ -> Iter.empty
     | Add (v,c,i) ->
@@ -53,17 +53,17 @@ struct
     | Mem (v,c) -> Iter.map (fun c -> Mem (v,c)) (Shrink.char c)
     | Length _ -> Iter.empty
 
-  let fix_cmd env = function
-    | Clear i         -> Iter.map (fun i -> Clear i        ) (Env.valid_t_vars env i)
-    | Copy i          -> Iter.map (fun i -> Copy i         ) (Env.valid_t_vars env i)
-    | Add (i,x,y)     -> Iter.map (fun i -> Add (i,x,y)    ) (Env.valid_t_vars env i)
-    | Remove (i,x)    -> Iter.map (fun i -> Remove (i,x)   ) (Env.valid_t_vars env i)
-    | Find (i,x)      -> Iter.map (fun i -> Find (i,x)     ) (Env.valid_t_vars env i)
-    | Find_opt (i,x)  -> Iter.map (fun i -> Find_opt (i,x) ) (Env.valid_t_vars env i)
-    | Find_all (i,x)  -> Iter.map (fun i -> Find_all (i,x) ) (Env.valid_t_vars env i)
-    | Replace (i,x,y) -> Iter.map (fun i -> Replace (i,x,y)) (Env.valid_t_vars env i)
-    | Mem (i,x)       -> Iter.map (fun i -> Mem (i,x)      ) (Env.valid_t_vars env i)
-    | Length i        -> Iter.map (fun i -> Length i       ) (Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Clear i
+    | Copy i
+    | Add (i,_,_)
+    | Remove (i,_)
+    | Find (i,_)
+    | Find_opt (i,_)
+    | Find_all (i,_)
+    | Replace (i,_,_)
+    | Mem (i,_)
+    | Length i -> i=v
 
   type res =
     | RClear
diff --git a/src/kcas/lin_tests.ml b/src/kcas/lin_tests.ml
index 09447a946..ce71ee4f1 100644
--- a/src/kcas/lin_tests.ml
+++ b/src/kcas/lin_tests.ml
@@ -34,7 +34,18 @@ struct
         map  (fun t     -> None, Decr t) gen_var;
       ])
 
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Cas (i,_,_)
+    | TryMapNone i
+    (*| TryMapSome i *)
+    | MapNone i
+    | MapSome i
+    | Incr i
+    | Decr i -> i=v
 
   type res =
     | RGet of int
@@ -103,7 +114,18 @@ struct
         map  (fun t -> None,Decr t) gen_var;
       ])
 
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Cas (i,_,_)
+    | TryMapNone i
+    (*| TryMapSome i *)
+    | MapNone i
+    | MapSome i
+    | Incr i
+    | Decr i -> i=v
 
   type res =
     | RGet of int
diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml
index 31b41ca3e..4f851eb82 100644
--- a/src/lazy/lin_tests.ml
+++ b/src/lazy/lin_tests.ml
@@ -60,14 +60,14 @@ struct
     | Map_val f -> Iter.map (fun f -> Map_val f) (Fn.shrink f)
   *)
   (* the Lazy tests already take a while to run - so better avoid spending extra time shrinking *)
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
 
-  let fix_cmd env = function
-    | Force i       -> Iter.map (fun i -> Force i      ) (Env.valid_t_vars env i)
-    | Force_val i   -> Iter.map (fun i -> Force_val i  ) (Env.valid_t_vars env i)
-    | Is_val i      -> Iter.map (fun i -> Is_val i     ) (Env.valid_t_vars env i)
-    | Map (i,f)     -> Iter.map (fun i -> Map (i,f)    ) (Env.valid_t_vars env i)
-    | Map_val (i,f) -> Iter.map (fun i -> Map_val (i,f)) (Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Force i
+    | Force_val i
+    | Is_val i
+    | Map (i,_)
+    | Map_val (i,_) -> i=v
 
   type t = int Lazy.t
 
diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml
index 138974e84..bdd92a993 100644
--- a/src/neg_tests/lin_tests_common.ml
+++ b/src/neg_tests/lin_tests_common.ml
@@ -45,19 +45,19 @@ module RConf_int = struct
         map  (fun t -> None,Decr t) gen_var;
       ])
 
-  let shrink_cmd c = match c with
+  let shrink_cmd _env c = match c with
     | Get _
     | Incr _
     | Decr _ -> Iter.empty
     | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int i)
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
 
-  let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_t_vars env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
-    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_t_vars env i)
-    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
@@ -97,19 +97,19 @@ module RConf_int64 = struct
         map  (fun t -> None,Decr t) gen_var;
       ])
 
-  let shrink_cmd c = match c with
+  let shrink_cmd _env c = match c with
     | Get _
     | Incr _
     | Decr _ -> Iter.empty
     | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int64 i)
     | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
 
-  let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Env.valid_t_vars env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
-    | Incr i    -> Iter.map (fun i -> Incr i   ) (Env.valid_t_vars env i)
-    | Decr i    -> Iter.map (fun i -> Decr i   ) (Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
@@ -156,13 +156,13 @@ struct
         map2 (fun t i -> None,Member (t,i)) gen_var gen_int';
       ])
 
-  let shrink_cmd c = match c with
+  let shrink_cmd _env c = match c with
     | Add_node (t,i) -> Iter.map (fun i -> Add_node (t,i)) (T.shrink i)
     | Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
 
-  let fix_cmd env = function
-    | Add_node (i,x) -> Iter.map (fun i -> Add_node (i,x)) (Lin.Env.valid_t_vars env i)
-    | Member (i,x)   -> Iter.map (fun i -> Member (i,x)  ) (Lin.Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Add_node (i,_)
+    | Member (i,_) -> v=i
 
   type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
 
diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml
index 82762698f..3a69e0673 100644
--- a/src/queue/lin_tests.ml
+++ b/src/queue/lin_tests.ml
@@ -32,7 +32,7 @@ module Spec =
           map  (fun t -> None, Length t) gen_var;
         ])
 
-    let shrink_cmd c = match c with
+    let shrink_cmd _env c = match c with
       | Take _
       | Take_opt _
       | Peek _
@@ -47,16 +47,16 @@ module Spec =
             <+>
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
-    let fix_cmd env = function
-      | Add (i,x)    -> Iter.map (fun i -> Add (i,x)   ) (Env.valid_t_vars env i)
-      | Take i       -> Iter.map (fun i -> Take i      ) (Env.valid_t_vars env i)
-      | Take_opt i   -> Iter.map (fun i -> Take_opt i  ) (Env.valid_t_vars env i)
-      | Peek i       -> Iter.map (fun i -> Peek i      ) (Env.valid_t_vars env i)
-      | Peek_opt i   -> Iter.map (fun i -> Peek_opt i  ) (Env.valid_t_vars env i)
-      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_t_vars env i)
-      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_t_vars env i)
-      | Fold (i,x,y) -> Iter.map (fun i -> Fold (i,x,y)) (Env.valid_t_vars env i)
-      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_t_vars env i)
+    let cmd_uses_var v = function
+      | Add (i,_)
+      | Take i
+      | Take_opt i
+      | Peek i
+      | Peek_opt i
+      | Clear i
+      | Is_empty i
+      | Fold (i,_,_)
+      | Length i -> i=v
 
     type res =
       | RAdd
diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml
index 486a598aa..88de8e416 100644
--- a/src/stack/lin_tests.ml
+++ b/src/stack/lin_tests.ml
@@ -33,7 +33,7 @@ module Spec =
           map  (fun t -> None, Length t) gen_var;
         ])
 
-    let shrink_cmd c = match c with
+    let shrink_cmd _env c = match c with
       | Pop _
       | Pop_opt _
       | Top _
@@ -48,16 +48,16 @@ module Spec =
             <+>
             (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
 
-    let fix_cmd env = function
-      | Push (i,x)   -> Iter.map (fun i -> Push (i,x)  ) (Env.valid_t_vars env i)
-      | Pop i        -> Iter.map (fun i -> Pop i       ) (Env.valid_t_vars env i)
-      | Pop_opt i    -> Iter.map (fun i -> Pop_opt i   ) (Env.valid_t_vars env i)
-      | Top i        -> Iter.map (fun i -> Top i       ) (Env.valid_t_vars env i)
-      | Top_opt i    -> Iter.map (fun i -> Top_opt i   ) (Env.valid_t_vars env i)
-      | Clear i      -> Iter.map (fun i -> Clear i     ) (Env.valid_t_vars env i)
-      | Is_empty i   -> Iter.map (fun i -> Is_empty i  ) (Env.valid_t_vars env i)
-      | Fold (i,f,x) -> Iter.map (fun i -> Fold (i,f,x)) (Env.valid_t_vars env i)
-      | Length i     -> Iter.map (fun i -> Length i    ) (Env.valid_t_vars env i)
+    let cmd_uses_var v c = match c with
+      | Push (i,_)
+      | Pop i
+      | Pop_opt i
+      | Top i
+      | Top_opt i
+      | Clear i
+      | Is_empty i
+      | Fold (i,_,_)
+      | Length i -> i=v
 
     type res =
       | RPush

From d35745e0977fdb174e6da58f3cd48e3f81ea2759 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 8 Nov 2022 18:15:05 +0100
Subject: [PATCH 52/57] update src/internal too

---
 src/internal/cleanup_lin.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/internal/cleanup_lin.ml b/src/internal/cleanup_lin.ml
index b1bb61952..c9e997ee2 100644
--- a/src/internal/cleanup_lin.ml
+++ b/src/internal/cleanup_lin.ml
@@ -22,12 +22,12 @@ struct
 	  Gen.map2 (fun t i -> None, Add (t,i)) gen_var int_gen;
          ])
 
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
 
-  let fix_cmd env = function
-    | Get i     -> Iter.map (fun i -> Get i    ) (Lin.Env.valid_t_vars env i)
-    | Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Lin.Env.valid_t_vars env i)
-    | Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Lin.Env.valid_t_vars env i)
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_) -> i=v
 
   let init () = (ref Inited, ref 0)
 

From 94649b9a955128c1e0d69f7b2ea240900d1e683e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 11 Nov 2022 14:51:16 +0100
Subject: [PATCH 53/57] Add comment to clarify eta expansion

---
 lib/lin.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index cd4b6b58b..22e234eea 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -162,7 +162,7 @@ module MakeDomThr(Spec : CmdSpec)
     map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list_spine p1 ctx_doesnt_use_var)
     <+>
     map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list_spine p2 ctx_doesnt_use_var)
-    <+>
+    <+> (* eta-expand the following two to lazily compute the match and @ until/if needed *)
     (fun yield -> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) yield)
     <+>
     (fun yield -> (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s)) yield)

From 03171767b065a4faa32649c4e187a8695d6a22d4 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Fri, 11 Nov 2022 14:52:12 +0100
Subject: [PATCH 54/57] remove commented-out extract_envs

---
 lib/lin.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 22e234eea..09381069e 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -170,9 +170,9 @@ module MakeDomThr(Spec : CmdSpec)
     (* Secondly reduce the cmd data of individual list elements *)
     (fun yield ->
        let seq_env = extract_env [0] seq in (* only extract_env if needed *)
-       (Iter.map (fun p1  -> (seq,p1,p2)) (shrink_individual_cmds (*(extract_env [0] seq)*) seq_env p1)
+       (Iter.map (fun p1  -> (seq,p1,p2)) (shrink_individual_cmds seq_env p1)
         <+>
-        Iter.map (fun p2  -> (seq,p1,p2)) (shrink_individual_cmds (*(extract_env [0] seq)*) seq_env p2))
+        Iter.map (fun p2  -> (seq,p1,p2)) (shrink_individual_cmds seq_env p2))
          yield)
     <+>
     Iter.map (fun seq -> (seq,p1,p2)) (shrink_individual_cmds [0] seq)

From 43d5f8a01a6477a824323c9e6b002cbb2519c50e Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Thu, 2 Feb 2023 13:38:58 +0100
Subject: [PATCH 55/57] fix test/cleanup.ml

---
 test/cleanup.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/test/cleanup.ml b/test/cleanup.ml
index fe443e6b5..a64e4a667 100644
--- a/test/cleanup.ml
+++ b/test/cleanup.ml
@@ -7,13 +7,15 @@ let cleanup_counter = Atomic.make 0
 
 module RConf =
 struct
+  open Lin.Internal [@@alert "-internal"]
+
   exception Already_cleaned
   type status = Inited | Cleaned
 
   type cmd =
-    | Get of Lin.Var.t
-    | Set of Lin.Var.t * int
-    | Add of Lin.Var.t * int [@@deriving show { with_path = false }]
+    | Get of Var.t
+    | Set of Var.t * int
+    | Add of Var.t * int [@@deriving show { with_path = false }]
 
   type t = (status ref) * (int ref)
 

From a1dc261c4b4756f6c64984602d8bbcfaf8997b4a Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Mon, 27 Feb 2023 16:17:45 +0100
Subject: [PATCH 56/57] Introduce Lin.Internal.cmd_triple and simplify
 signatures

---
 lib/lin.ml         | 45 +++++++++++++++++++++++++--------------------
 lib/lin.mli        | 12 +++++++++---
 lib/lin_domain.ml  |  4 ++--
 lib/lin_domain.mli |  4 ++--
 lib/lin_effect.ml  |  4 ++--
 lib/lin_effect.mli |  4 ++--
 lib/lin_thread.ml  |  4 ++--
 lib/lin_thread.mli |  4 ++--
 8 files changed, 46 insertions(+), 35 deletions(-)

diff --git a/lib/lin.ml b/lib/lin.ml
index 924e29552..0d6c18fa6 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -67,11 +67,17 @@ struct
         [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; }
+
+
   (** A functor to create test setups, for all backends (Domain, Thread and Effect).
       We use it below, but it can also be used independently *)
   module Make(Spec : CmdSpec)
   = struct
-
     (* plain interpreter of a cmd list *)
     let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs
 
@@ -127,34 +133,30 @@ end
         <+>
         map (fun cmd -> (opt,cmd)::cmds) (Spec.shrink_cmd env cmd)
 
-    let shrink_triple' (seq,p1,p2) =
+    let shrink_triple ({ env_size=_; seq_prefix=seq; tail_left=p1; tail_right=p2 } as t) =
       let open Iter in
       (* Shrinking heuristic:
          First reduce the cmd list sizes as much as possible, since the interleaving
          is most costly over long cmd lists. *)
-      map (fun seq -> (seq,p1,p2)) (shrink_cmd_list_spine seq (fun var -> cmds_use_var var p1 || cmds_use_var var p2))
+      map (fun seq -> { t with seq_prefix=seq }) (shrink_cmd_list_spine seq (fun var -> cmds_use_var var p1 || cmds_use_var var p2))
       <+>
-      map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list_spine p1 ctx_doesnt_use_var)
+      map (fun p1 -> { t with tail_left=p1 }) (shrink_cmd_list_spine p1 ctx_doesnt_use_var)
       <+>
-      map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list_spine p2 ctx_doesnt_use_var)
+      map (fun p2 -> { t with tail_right=p2 }) (shrink_cmd_list_spine p2 ctx_doesnt_use_var)
       <+> (* eta-expand the following two to lazily compute the match and @ until/if needed *)
-      (fun yield -> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) yield)
+      (fun yield -> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return { t with seq_prefix=seq@[c1]; tail_left=c1s}) yield)
       <+>
-      (fun yield -> (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s)) yield)
+      (fun yield -> (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return { t with seq_prefix=seq@[c2]; tail_right=c2s}) yield)
       <+>
       (* Secondly reduce the cmd data of individual list elements *)
       (fun yield ->
          let seq_env = extract_env [0] seq in (* only extract_env if needed *)
-         (Iter.map (fun p1  -> (seq,p1,p2)) (shrink_individual_cmds seq_env p1)
+         (Iter.map (fun p1 -> { t with tail_left=p1 }) (shrink_individual_cmds seq_env p1)
           <+>
-          Iter.map (fun p2  -> (seq,p1,p2)) (shrink_individual_cmds seq_env p2))
+          Iter.map (fun p2 -> { t with tail_right=p2 }) (shrink_individual_cmds seq_env p2))
            yield)
       <+>
-      Iter.map (fun seq -> (seq,p1,p2)) (shrink_individual_cmds [0] seq)
-
-    let shrink_triple (size,t) =
-      Iter.map (fun t -> (size,t)) (shrink_triple' t)
-
+      Iter.map (fun seq -> { t with seq_prefix=seq }) (shrink_individual_cmds [0] seq)
 
     let show_cmd (opt,c) = match opt with
       | None   -> Spec.show_cmd c
@@ -163,6 +165,9 @@ end
     let init_cmd = "let t0 = init ()"
     let init_cmd_ret = init_cmd ^ " : ()"
 
+    let print_triple { seq_prefix; tail_left; tail_right; _ } =
+      print_triple_vertical ~init_cmd show_cmd (seq_prefix, tail_left, tail_right)
+
     let arb_cmds_triple seq_len par_len =
       let gen_triple st =
         Var.reset ();
@@ -170,13 +175,13 @@ end
         assert (init_var = 0);
         Gen.(int_range 2 (2*par_len) >>= fun dbl_plen ->
              let par_len1 = dbl_plen/2 in
-             gen_cmds_size [init_var] (int_bound seq_len) >>= fun (env,seq_pref) ->
-             gen_cmds_size env (return par_len1) >>= fun (_env1,par1) ->
-             gen_cmds_size env (return (dbl_plen - par_len1)) >>= fun (_env2,par2) ->
-             let array_size = Var.next () in
-             return (array_size,(seq_pref,par1,par2))) st
+             gen_cmds_size [init_var] (int_bound seq_len) >>= fun (env,seq_prefix) ->
+             gen_cmds_size env (return par_len1) >>= fun (_env1,tail_left) ->
+             gen_cmds_size env (return (dbl_plen - par_len1)) >>= fun (_env2,tail_right) ->
+             let env_size = Var.next () in
+             return { env_size; seq_prefix; tail_left; tail_right }) st
       in
-      make ~print:(fun (_,t) -> print_triple_vertical ~init_cmd show_cmd t) ~shrink:shrink_triple gen_triple
+      make ~print:print_triple ~shrink:shrink_triple gen_triple
 
     let init_sut array_size =
       let sut = Spec.init () in
diff --git a/lib/lin.mli b/lib/lin.mli
index 143d10886..be3bb7a9f 100644
--- a/lib/lin.mli
+++ b/lib/lin.mli
@@ -65,16 +65,22 @@ module Internal : sig
         [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 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 -> (int * ((Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list)) QCheck.arbitrary
+    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:(int * ((Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list) -> bool) -> QCheck.Test.t
-    val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(int * ((Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list * (Var.t option * Spec.cmd) list) -> bool) -> QCheck.Test.t
+    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
diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml
index b30775a0e..8c025d6c8 100644
--- a/lib/lin_domain.ml
+++ b/lib/lin_domain.ml
@@ -11,7 +11,7 @@ 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 (array_size, (seq_pref,cmds1,cmds2)) =
+  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
@@ -27,7 +27,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ 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)
+              (pref_obs,obs1,obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli
index ce70a6cbd..50aeada9d 100644
--- a/lib/lin_domain.mli
+++ b/lib/lin_domain.mli
@@ -3,8 +3,8 @@ open Lin
 (** functor to build an internal module representing parallel tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   [@@@alert "-internal"]
-  val arb_cmds_triple : int -> int -> (int * ((Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list)) QCheck.arbitrary
-  val lin_prop : int * ((Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list) -> bool
+  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
diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml
index 7874a1164..525e079b5 100644
--- a/lib/lin_effect.ml
+++ b/lib/lin_effect.ml
@@ -97,7 +97,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
 
   (* Concurrent agreement property based on effect-handler scheduler *)
   let lin_prop =
-    (fun (array_size,(seq_pref,cmds1,cmds2)) ->
+    (fun { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } ->
        let sut = EffTest.init_sut array_size in
        (* exclude [Yield]s from sequential prefix *)
        let pref_obs = EffTest.interp_plain sut (List.filter (fun (_,c) -> c <> EffSpec.SchedYield) seq_pref) in
@@ -113,7 +113,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
        || QCheck.Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
        @@ 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))
+         (pref_obs,!obs1,!obs2))[@@alert "-internal"]
 
   let lin_test ~count ~name =
     let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in
diff --git a/lib/lin_effect.mli b/lib/lin_effect.mli
index 35ade018d..453e370db 100644
--- a/lib/lin_effect.mli
+++ b/lib/lin_effect.mli
@@ -6,8 +6,8 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
     type cmd
   end
   [@@@alert "-internal"]
-  val arb_cmds_triple : int -> int -> (int * ((Internal.Var.t option * EffSpec.cmd) list * (Internal.Var.t option * EffSpec.cmd) list * (Internal.Var.t option * EffSpec.cmd) list)) QCheck.arbitrary
-  val lin_prop : int * ((Internal.Var.t option * EffSpec.cmd) list * (Internal.Var.t option * EffSpec.cmd) list * (Internal.Var.t option * EffSpec.cmd) list) -> bool
+  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
diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml
index 10b105844..c30e6d5f6 100644
--- a/lib/lin_thread.ml
+++ b/lib/lin_thread.ml
@@ -19,7 +19,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
 
   (* Linearization property based on [Thread] *)
   let lin_prop =
-    (fun (array_size, (seq_pref, cmds1, cmds2)) ->
+    (fun { 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 [], ref [] in
       let pref_obs = interp_plain sut seq_pref in
@@ -35,7 +35,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ 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))
+              (pref_obs,!obs1,!obs2))[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop
diff --git a/lib/lin_thread.mli b/lib/lin_thread.mli
index 810c35513..abbcba5c7 100644
--- a/lib/lin_thread.mli
+++ b/lib/lin_thread.mli
@@ -3,8 +3,8 @@ open Lin
 (** functor to build an internal module representing concurrent tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   [@@@alert "-internal"]
-  val arb_cmds_triple : int -> int -> (int * ((Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list)) QCheck.arbitrary
-  val lin_prop : int * ((Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list * (Internal.Var.t option * Spec.cmd) list) -> bool
+  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

From 457a4930785df339db0ed7ab45480dbab64b2d36 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 7 Mar 2023 14:20:43 +0100
Subject: [PATCH 57/57] increase chance of Bigarray.Array1.get to observe diffs

---
 src/bigarray/lin_tests_dsl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml
index 6d3607b34..7103de980 100644
--- a/src/bigarray/lin_tests_dsl.ml
+++ b/src/bigarray/lin_tests_dsl.ml
@@ -49,7 +49,7 @@ struct
       (* [change_layout]: the layout is fixed in our sut, so we test a dummy version *)
       val_ "Bigarray.Array1.change_layout" dummy_change_layout  (t @-> returning_ t);
       val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
-      val_ "Bigarray.Array1.get"           Array1.get           (t @-> int @-> returning_or_exc int);
+      val_freq 4 "Bigarray.Array1.get"     Array1.get           (t @-> int @-> returning_or_exc int);
       val_ "Bigarray.Array1.set"           Array1.set           (t @-> int @-> int @-> returning_or_exc unit);
       val_ "Bigarray.Array1.sub"           Array1.sub           (t @-> int @-> int @-> returning_or_exc_ t);
       (* [Array1.slice]: cannot be tested since it produces a Bigarray.Array0.t *)