From f9f9d13bbcc279cb3a63abb83c4f7a9a497becd4 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 7 Nov 2023 12:09:58 +0100
Subject: [PATCH] Add some tests

---
 plugins/qcheck-stm/test/sequence_model.ml     |  7 +++
 plugins/qcheck-stm/test/sequence_model.mli    |  7 +++
 .../test/sequence_model_stm_tests.expected.ml | 57 ++++++++++++++++---
 3 files changed, 64 insertions(+), 7 deletions(-)

diff --git a/plugins/qcheck-stm/test/sequence_model.ml b/plugins/qcheck-stm/test/sequence_model.ml
index 847555d7..09af067f 100644
--- a/plugins/qcheck-stm/test/sequence_model.ml
+++ b/plugins/qcheck-stm/test/sequence_model.ml
@@ -2,3 +2,10 @@ type 'a t = 'a list ref
 
 let create () = ref []
 let add x s = s := x :: !s
+
+let remove s =
+  match !s with
+  | [] -> None
+  | x :: xs ->
+      s := xs;
+      Some x
diff --git a/plugins/qcheck-stm/test/sequence_model.mli b/plugins/qcheck-stm/test/sequence_model.mli
index 939ae4be..b1dc1b2d 100644
--- a/plugins/qcheck-stm/test/sequence_model.mli
+++ b/plugins/qcheck-stm/test/sequence_model.mli
@@ -9,3 +9,10 @@ val add : 'a -> 'a t -> unit
 (*@ add v t
     modifies t.contents
     ensures t.contents = Sequence.cons v (old t.contents) *)
+
+val remove : 'a t -> 'a option
+(*@ o = remove t
+    modifies t.contents
+    ensures t.contents = match Sequence.length (old t.contents) with
+                          | 0 -> Sequence.empty
+                          | _ -> Sequence.tl (old t.contents) *)
diff --git a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
index a51d50f9..d107dfad 100644
--- a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml
@@ -6,9 +6,11 @@ module Spec =
     type sut = char t
     type cmd =
       | Add of char 
+      | Remove 
     let show_cmd cmd__001_ =
       match cmd__001_ with
       | Add v -> Format.asprintf "%s %a" "add" (Util.Pp.pp_char true) v
+      | Remove -> Format.asprintf "%s" "remove"
     type nonrec state = {
       contents: char Ortac_runtime.Gospelstdlib.sequence }
     let init_state =
@@ -43,7 +45,8 @@ module Spec =
     let arb_cmd _ =
       let open QCheck in
         make ~print:show_cmd
-          (let open Gen in oneof [(pure (fun v -> Add v)) <*> char])
+          (let open Gen in
+             oneof [(pure (fun v -> Add v)) <*> char; pure Remove])
     let next_state cmd__002_ state__003_ =
       match cmd__002_ with
       | Add v ->
@@ -74,14 +77,54 @@ module Spec =
                                }
                            }))))
           }
-    let precond cmd__008_ state__009_ = match cmd__008_ with | Add v -> 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
+      | Remove ->
+          {
+            contents =
+              ((try
+                  match Ortac_runtime.Gospelstdlib.Sequence.length
+                          state__003_.contents
+                  with
+                  | __x__004_ when
+                      (=) __x__004_
+                        (Ortac_runtime.Gospelstdlib.integer_of_int 0)
+                      -> Ortac_runtime.Gospelstdlib.Sequence.empty
+                  | _ ->
+                      Ortac_runtime.Gospelstdlib.Sequence.tl
+                        state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "sequence_model.mli";
+                                 pos_lnum = 16;
+                                 pos_bol = 732;
+                                 pos_cnum = 757
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "sequence_model.mli";
+                                 pos_lnum = 18;
+                                 pos_bol = 849;
+                                 pos_cnum = 910
+                               }
+                           }))))
+          }
+    let precond cmd__009_ state__010_ =
+      match cmd__009_ with | Add v -> true | Remove -> true
+    let postcond cmd__005_ state__006_ res__007_ =
+      let new_state__008_ = lazy (next_state cmd__005_ state__006_) in
+      match (cmd__005_, res__007_) with
       | (Add v, Res ((Unit, _), _)) -> true
+      | (Remove, Res ((Option (Char), _), o)) -> true
       | _ -> true
-    let run cmd__010_ sut__011_ =
-      match cmd__010_ with | Add v -> Res (unit, (add v sut__011_))
+    let run cmd__011_ sut__012_ =
+      match cmd__011_ with
+      | Add v -> Res (unit, (add v sut__012_))
+      | Remove -> Res ((option char), (remove sut__012_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
 let _ =