Add some tests.

Fixes ocaml-gospel#171
Non compiling code is not generated anymore, but the user doesn't know
why `next_state` was not generated.

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 pop q =
+  match !q with
+  | [] -> None
+  | x :: xs ->
+      q := xs;
+      Some x

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 pop : 'a t -> 'a option
+(*@ o = pop q
+    modifies q.contents
+    ensures q.contents = match o with
+                          | None -> old q.contents
+                          | Some _ -> Sequence.tl (old q.contents) *)