Add QCheck-STM test for Accumulator

test/kcas_data/accumulator_test_stm.ml

@@ -0,0 +1,53 @@
+open QCheck
+open STM
+open Kcas_data
+
+module Spec = struct
+  type cmd = Incr | Decr | Get | Set of int
+
+  let show_cmd = function
+    | Incr -> "Incr"
+    | Decr -> "Decr"
+    | Get -> "Get"
+    | Set v -> "Set " ^ string_of_int v
+
+  type state = int
+  type sut = Accumulator.t
+
+  let arb_cmd _s =
+    [
+      Gen.return Incr;
+      Gen.return Decr;
+      Gen.return Get;
+      Gen.map (fun i -> Set i) Gen.nat;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
+
+  let init_state = 0
+  let init_sut () = Accumulator.make 0
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with Incr -> s + 1 | Decr -> s - 1 | Get -> s | Set v -> v
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Incr -> Res (unit, Accumulator.incr d)
+    | Decr -> Res (unit, Accumulator.decr d)
+    | Get -> Res (int, Accumulator.get d)
+    | Set v -> Res (unit, Accumulator.set d v)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Incr, Res ((Unit, _), ()) -> true
+    | Decr, Res ((Unit, _), ()) -> true
+    | Set _, Res ((Unit, _), ()) -> true
+    | Get, Res ((Int, _), res) -> res = s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Accumulator" (module Spec)
+  |> exit

test/kcas_data/dune

@@ -11,6 +11,7 @@
 
 (tests
  (names
+  accumulator_test_stm
   dllist_test
   hashtbl_test
   lru_cache_example

test/kcas_data/stack_test_stm.ml

@@ -1,3 +1,5 @@
+open QCheck
+open STM
 open Kcas_data
 
 module Spec = struct
@@ -13,14 +15,13 @@ module Spec = struct
   type sut = int Stack.t
 
   let arb_cmd _s =
-    QCheck.(
-      [
-        Gen.int |> Gen.map (fun x -> Push x);
-        Gen.return Pop_opt;
-        Gen.return Top_opt;
-        Gen.return Length;
-      ]
-      |> Gen.oneof |> make ~print:show_cmd)
+    [
+      Gen.int |> Gen.map (fun x -> Push x);
+      Gen.return Pop_opt;
+      Gen.return Top_opt;
+      Gen.return Length;
+    ]
+    |> Gen.oneof |> make ~print:show_cmd
 
   let init_state = []
   let init_sut () = Stack.create ()
@@ -36,15 +37,13 @@ module Spec = struct
   let precond _ _ = true
 
   let run c d =
-    let open STM in
     match c with
     | Push x -> Res (unit, Stack.push x d)
     | Pop_opt -> Res (option int, Stack.pop_opt d)
     | Top_opt -> Res (option int, Stack.top_opt d)
     | Length -> Res (int, Stack.length d)
 
   let postcond c (s : state) res =
-    let open STM in
     match (c, res) with
     | Push _x, Res ((Unit, _), ()) -> true
     | Pop_opt, Res ((Option Int, _), res) -> (