Explore conjunctive clauses when looking for state description

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -132,13 +132,15 @@ let split_args config vd args =
 
 let get_state_description_with_index is_t state spec =
   let open Tterm in
-  let pred i t =
+  let rec pred i t =
     match t.t_node with
     | Tapp (ls, [ { t_node = Tfield ({ t_node = Tvar vs; _ }, m); _ }; right ])
       when Symbols.(ls_equal ps_equ ls) && is_t vs ->
         if List.exists (fun (id, _) -> Ident.equal id m.ls_name) state then
           Some (i, Ir.{ model = m.ls_name; description = right })
         else None
+    | Tbinop ((Tand|Tand_asym), l, r) -> (
+        match pred i l with None -> pred i r | o -> o)
     | _ -> None
   in
   List.mapi pred spec.sp_post |> List.filter_map Fun.id

plugins/qcheck-stm/test/conjunctive_clauses.mli

@@ -0,0 +1,14 @@
+type 'a t
+(*@ mutable model contents : 'a list *)
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    ensures true /\ true && t.contents = List.init i (fun _ -> a) *)
+
+(*@ function set_contents (c : 'a list) (i : integer) (a : 'a) : 'a list =
+          List.mapi (fun j x -> if i = j then a else x) c *)
+
+val set : 'a t -> int -> 'a -> unit
+(*@ set t i a
+    modifies t
+    ensures true /\ true && t.contents = set_contents (old t.contents) i a *)

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

@@ -0,0 +1,59 @@
+open Conjunctive_clauses
+let set_contents c i a_1 =
+  Ortac_runtime.Gospelstdlib.List.mapi
+    (fun j -> fun x -> if i = j then a_1 else x) c
+module Spec =
+  struct
+    open STM
+    [@@@ocaml.warning "-26-27"]
+    type sut = char t
+    type cmd =
+      | Set of int * char 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Set (i_1, a_2) ->
+          Format.asprintf "%s %a %a" "set" (Util.Pp.pp_int true) i_1
+            (Util.Pp.pp_char true) a_2
+    type nonrec state = {
+      contents: char list }
+    let init_state =
+      let i_2 = 42
+      and a_3 = 'a' in
+      {
+        contents =
+          (Ortac_runtime.Gospelstdlib.List.init
+             (Ortac_runtime.Gospelstdlib.integer_of_int i_2) (fun _ -> a_3))
+      }
+    let init_sut () = make 42 'a'
+    let cleanup _ = ()
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd
+          (let open Gen in
+             oneof
+               [((pure (fun i_1 -> fun a_2 -> Set (i_1, a_2))) <*> int) <*>
+                  char])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Set (i_1, a_2) ->
+          {
+            contents =
+              (set_contents state__003_.contents
+                 (Ortac_runtime.Gospelstdlib.integer_of_int i_1) a_2)
+          }
+    let precond cmd__008_ state__009_ =
+      match cmd__008_ with | Set (i_1, a_2) -> 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
+      | (Set (i_1, a_2), Res ((Unit, _), _)) -> true
+      | _ -> true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with
+      | Set (i_1, a_2) -> Res (unit, (set sut__011_ i_1 a_2))
+  end
+module STMTests = (STM_sequential.Make)(Spec)
+let _ =
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"STM Lib test sequential"])

plugins/qcheck-stm/test/dune

@@ -226,3 +226,25 @@
  (alias launchtests)
  (action
   (run %{dep:ref_stm_tests.exe} -v)))
+
+(rule
+ (target conjunctive_clauses_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
+    conjunctive_clauses_errors
+    (run ortac qcheck-stm %{dep:conjunctive_clauses.mli} "make 42 'a'" "char t" -o %{target})))))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff conjunctive_clauses_errors.expected conjunctive_clauses_errors)
+   (diff conjunctive_clauses_stm_tests.expected.ml conjunctive_clauses_stm_tests.ml))))