rm STM_spec.AddGC functor

Author: jmid

lib/STM_spec.ml

@@ -105,51 +105,3 @@ sig
       model's result.
       Note: [s] is in this case the model's state prior to command execution. *)
 end
-
-module AddGC(Spec : Spec) : Spec = struct
-  type cmd =
-    | GC_minor
-    | UserCmd of Spec.cmd
-
-  type state = Spec.state
-  type sut   = Spec.sut
-
-  let init_state  = Spec.init_state
-  let init_sut () = Spec.init_sut ()
-  let cleanup sut = Spec.cleanup sut
-
-  let show_cmd c = match c with
-    | GC_minor -> "<GC.minor>"
-    | UserCmd c -> Spec.show_cmd c
-
-  let gen_cmd s =
-    (Gen.frequency
-       [(1,Gen.return GC_minor);
-        (5,Gen.map (fun c -> UserCmd c) (Spec.arb_cmd s).gen)])
-
-  let shrink_cmd s c = match c with
-    | GC_minor  -> Iter.empty
-    | UserCmd c ->
-       match (Spec.arb_cmd s).shrink with
-       | None     -> Iter.empty (* no shrinker provided *)
-       | Some shk -> Iter.map (fun c' -> UserCmd c') (shk c)
-
-  let arb_cmd s = make ~print:show_cmd ~shrink:(shrink_cmd s) (gen_cmd s)
-
-  let next_state c s = match c with
-    | GC_minor  -> s
-    | UserCmd c -> Spec.next_state c s
-
-  let precond c s = match c with
-    | GC_minor  -> true
-    | UserCmd c -> Spec.precond c s
-
-  let run c s = match c with
-    | GC_minor  -> (Gc.minor (); Res (unit, ()))
-    | UserCmd c -> Spec.run c s
-
-  let postcond c s r = match c,r with
-    | GC_minor,  Res ((Unit,_),_) -> true
-    | UserCmd c, r -> Spec.postcond c s r
-    | _,_ -> false
-end

lib/STM_spec.mli

@@ -120,5 +120,3 @@ sig
       model's result. A [postcond] function should be a pure.
       Note: [s] is in this case the model's state prior to command execution. *)
 end
-
-module AddGC : functor (Spec : Spec) -> Spec