Add more QCheck-STM tests

test/kcas_data/dllist_test_stm.ml

@@ -0,0 +1,87 @@
+open QCheck
+open STM
+open Kcas_data
+
+module Spec = struct
+  type cmd = Add_l of int | Take_opt_l | Add_r of int | Take_opt_r
+
+  let show_cmd = function
+    | Add_l x -> "Add_l " ^ string_of_int x
+    | Take_opt_l -> "Take_opt_l"
+    | Add_r x -> "Add_r " ^ string_of_int x
+    | Take_opt_r -> "Take_opt_r"
+
+  module State = struct
+    type t = int list * int list
+
+    let push_l x (l, r) = (x :: l, r)
+    let push_r x (l, r) = (l, x :: r)
+
+    let drop_l (l, r) =
+      match l with
+      | _ :: l -> (l, r)
+      | [] -> begin
+          match List.rev r with [] -> ([], []) | _ :: l -> (l, [])
+        end
+
+    let drop_r (l, r) =
+      match r with
+      | _ :: r -> (l, r)
+      | [] -> begin
+          match List.rev l with [] -> ([], []) | _ :: r -> ([], r)
+        end
+
+    let peek_opt_l (l, r) =
+      match l with
+      | x :: _ -> Some x
+      | [] -> begin match List.rev r with x :: _ -> Some x | [] -> None end
+
+    let peek_opt_r (l, r) =
+      match r with
+      | x :: _ -> Some x
+      | [] -> begin match List.rev l with x :: _ -> Some x | [] -> None end
+  end
+
+  type state = State.t
+  type sut = int Dllist.t
+
+  let arb_cmd _s =
+    [
+      Gen.int |> Gen.map (fun x -> Add_l x);
+      Gen.return Take_opt_l;
+      Gen.int |> Gen.map (fun x -> Add_r x);
+      Gen.return Take_opt_r;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
+
+  let init_state = ([], [])
+  let init_sut () = Dllist.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Add_l x -> State.push_l x s
+    | Take_opt_l -> State.drop_l s
+    | Add_r x -> State.push_r x s
+    | Take_opt_r -> State.drop_r s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Add_l x -> Res (unit, Dllist.add_l x d |> ignore)
+    | Take_opt_l -> Res (option int, Dllist.take_opt_l d)
+    | Add_r x -> Res (unit, Dllist.add_r x d |> ignore)
+    | Take_opt_r -> Res (option int, Dllist.take_opt_r d)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Add_l _x, Res ((Unit, _), ()) -> true
+    | Take_opt_l, Res ((Option Int, _), res) -> res = State.peek_opt_l s
+    | Add_r _x, Res ((Unit, _), ()) -> true
+    | Take_opt_r, Res ((Option Int, _), res) -> res = State.peek_opt_r s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Dllist" (module Spec) |> exit

test/kcas_data/dune

@@ -13,10 +13,13 @@
  (names
   accumulator_test_stm
   dllist_test
+  dllist_test_stm
   hashtbl_test
+  hashtbl_test_stm
   lru_cache_example
   mvar_test
   queue_test
+  queue_test_stm
   stack_test
   stack_test_stm
   xt_test)

test/kcas_data/hashtbl_test_stm.ml

@@ -0,0 +1,61 @@
+open QCheck
+open STM
+open Kcas_data
+
+module Spec = struct
+  type cmd = Add of int | Mem of int | Remove of int | Length
+
+  let show_cmd = function
+    | Add x -> "Add " ^ string_of_int x
+    | Mem x -> "Mem " ^ string_of_int x
+    | Remove x -> "Remove " ^ string_of_int x
+    | Length -> "Length"
+
+  type state = int list
+  type sut = (int, unit) Hashtbl.t
+
+  let arb_cmd _s =
+    [
+      Gen.int_bound 10 |> Gen.map (fun x -> Add x);
+      Gen.int_bound 10 |> Gen.map (fun x -> Mem x);
+      Gen.int_bound 10 |> Gen.map (fun x -> Remove x);
+      Gen.return Length;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
+
+  let init_state = []
+  let init_sut () = Hashtbl.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Add x -> x :: s
+    | Mem _ -> s
+    | Remove x ->
+        let[@tail_mod_cons] rec drop_first = function
+          | [] -> []
+          | x' :: xs -> if x = x' then xs else x' :: drop_first xs
+        in
+        drop_first s
+    | Length -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Add x -> Res (unit, Hashtbl.add d x ())
+    | Mem x -> Res (bool, Hashtbl.mem d x)
+    | Remove x -> Res (unit, Hashtbl.remove d x)
+    | Length -> Res (int, Hashtbl.length d)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Add _x, Res ((Unit, _), ()) -> true
+    | Mem x, Res ((Bool, _), res) -> res = List.exists (( = ) x) s
+    | Remove _x, Res ((Unit, _), ()) -> true
+    | Length, Res ((Int, _), res) -> res = List.length s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Hashtbl" (module Spec) |> exit

test/kcas_data/queue_test_stm.ml

@@ -0,0 +1,68 @@
+open QCheck
+open STM
+open Kcas_data
+
+module Spec = struct
+  type cmd = Push of int | Take_opt | Peek_opt | Length
+
+  let show_cmd = function
+    | Push x -> "Push " ^ string_of_int x
+    | Take_opt -> "Take_opt"
+    | Peek_opt -> "Peek_opt"
+    | Length -> "Length"
+
+  module State = struct
+    type t = int list * int list
+
+    let push x (h, t) = if h == [] then ([ x ], []) else (h, x :: t)
+    let peek_opt (h, _) = match h with x :: _ -> Some x | [] -> None
+
+    let drop ((h, t) as s) =
+      match h with [] -> s | [ _ ] -> (List.rev t, []) | _ :: h -> (h, t)
+
+    let length (h, t) = List.length h + List.length t
+  end
+
+  type state = State.t
+  type sut = int Queue.t
+
+  let arb_cmd _s =
+    [
+      Gen.int |> Gen.map (fun x -> Push x);
+      Gen.return Take_opt;
+      Gen.return Peek_opt;
+      Gen.return Length;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
+
+  let init_state = ([], [])
+  let init_sut () = Queue.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Push x -> State.push x s
+    | Take_opt -> State.drop s
+    | Peek_opt -> s
+    | Length -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Push x -> Res (unit, Queue.push x d)
+    | Take_opt -> Res (option int, Queue.take_opt d)
+    | Peek_opt -> Res (option int, Queue.peek_opt d)
+    | Length -> Res (int, Queue.length d)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Push _x, Res ((Unit, _), ()) -> true
+    | Take_opt, Res ((Option Int, _), res) -> res = State.peek_opt s
+    | Peek_opt, Res ((Option Int, _), res) -> res = State.peek_opt s
+    | Length, Res ((Int, _), res) -> res = State.length s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Queue" (module Spec) |> exit