Add some tests

plugins/qcheck-stm/test/dune.inc

@@ -316,3 +316,56 @@
  (action
   (run %{dep:sequence_model_stm_tests.exe} -v)))
 
+(library
+ (name invariants)
+ (modules invariants))
+
+(rule
+ (target invariants_stm_tests.ml)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm))
+ (action
+  (setenv
+   ORTAC_ONLY_PLUGIN
+   qcheck-stm
+   (with-stderr-to
+    invariants_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:invariants.mli}
+     "create 42" "int t"
+     -o
+     %{target})))))
+
+(test
+ (name invariants_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules invariants_stm_tests)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime
+  invariants)
+ (action
+  (echo
+   "\n%{dep:invariants_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff invariants_errors.expected invariants_errors)
+   (diff invariants_stm_tests.expected.ml invariants_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:invariants_stm_tests.exe} -v)))
+

plugins/qcheck-stm/test/dune_gen.args

@@ -10,3 +10,5 @@ conjunctive_clauses
 "make 42 'a'" "char t"
 sequence_model
 "create ()" "char t"
+invariants
+"create 42" "int t"

plugins/qcheck-stm/test/invariants.ml

@@ -0,0 +1,4 @@
+type 'a t = 'a list ref
+
+let create a = ref [ a ]
+let push a t = t := a :: !t

plugins/qcheck-stm/test/invariants.mli

@@ -0,0 +1,13 @@
+type 'a t
+(*@ mutable model contents : 'a list
+    with x
+    invariant List.length x.contents > 0 *)
+
+val create : 'a -> 'a t
+(*@ t = create a
+    ensures t.contents = a :: [] *)
+
+val push : 'a -> 'a t -> unit
+(*@ push a t
+    modifies t
+    ensures t.contents = a :: (old t.contents) *)

plugins/qcheck-stm/test/invariants_errors.expected

@@ -1,4 +0,0 @@
-File "invariants.mli", line 4, characters 4-14:
-4 |     invariants List.length x.contents > 0 *)
-        ^^^^^^^^^^
-Error: Gospel error: Syntax error.

plugins/qcheck-stm/test/invariants_stm_tests.expected.ml

@@ -0,0 +1,148 @@
+open Invariants
+module Spec =
+  struct
+    open STM
+    [@@@ocaml.warning "-26-27"]
+    type sut = int t
+    type cmd =
+      | Push of int 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Push a_1 -> Format.asprintf "%s %a" "push" (Util.Pp.pp_int true) a_1
+    type nonrec state = {
+      contents: int list }
+    let init_state =
+      let a_2 = 42 in
+      {
+        contents =
+          (try a_2 :: []
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "invariants.mli";
+                            pos_lnum = 8;
+                            pos_bol = 292;
+                            pos_cnum = 317
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "invariants.mli";
+                            pos_lnum = 8;
+                            pos_bol = 292;
+                            pos_cnum = 324
+                          }
+                      })))
+      }
+    let init_sut () = create 42
+    let cleanup _ = ()
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd
+          (let open Gen in oneof [(pure (fun a_1 -> Push a_1)) <*> int])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Push a_1 ->
+          {
+            contents =
+              ((try a_1 :: state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "invariants.mli";
+                                 pos_lnum = 13;
+                                 pos_bol = 476;
+                                 pos_cnum = 501
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "invariants.mli";
+                                 pos_lnum = 13;
+                                 pos_bol = 476;
+                                 pos_cnum = 522
+                               }
+                           }))))
+          }
+    let precond cmd__008_ state__009_ =
+      match cmd__008_ with | Push a_1 -> true
+    let postcond cmd__004_ state__005_ res__006_ =
+      let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
+      match (cmd__004_, res__006_) with
+      | (Push a_1, Res ((Unit, _), _)) ->
+          (try
+             Ortac_runtime.Gospelstdlib.(>)
+               (Ortac_runtime.Gospelstdlib.List.length
+                  (Lazy.force new_state__007_).contents)
+               (Ortac_runtime.Gospelstdlib.integer_of_int 0)
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "invariants.mli";
+                            pos_lnum = 4;
+                            pos_bol = 110;
+                            pos_cnum = 124
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "invariants.mli";
+                            pos_lnum = 4;
+                            pos_bol = 110;
+                            pos_cnum = 150
+                          }
+                      })))
+      | _ -> true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with | Push a_1 -> Res (unit, (push a_1 sut__011_))
+  end
+module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () =
+  let __state__012_ = Spec.init_state in
+  if
+    try
+      Ortac_runtime.Gospelstdlib.(>)
+        (Ortac_runtime.Gospelstdlib.List.length __state__012_.contents)
+        (Ortac_runtime.Gospelstdlib.integer_of_int 0)
+    with
+    | e ->
+        raise
+          (Ortac_runtime.Partial_function
+             (e,
+               {
+                 Ortac_runtime.start =
+                   {
+                     pos_fname = "invariants.mli";
+                     pos_lnum = 4;
+                     pos_bol = 110;
+                     pos_cnum = 124
+                   };
+                 Ortac_runtime.stop =
+                   {
+                     pos_fname = "invariants.mli";
+                     pos_lnum = 4;
+                     pos_bol = 110;
+                     pos_cnum = 150
+                   }
+               }))
+  then __state__012_
+  else QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT"
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
+let _ =
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Invariants STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])