From 3fa49a1b01ea959ca19db6190303a593b4f67f3c Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 30 Nov 2023 16:26:41 +0100
Subject: [PATCH 01/27] Add fold_left to Reserr

Will need it shortly.
---
 plugins/qcheck-stm/src/reserr.ml  | 12 ++++++++++++
 plugins/qcheck-stm/src/reserr.mli |  1 +
 2 files changed, 13 insertions(+)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 19cd0649..1bb36112 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -278,6 +278,18 @@ let promote_opt r =
       let* _ = warns ws and* _ = filter_errs errs in
       ok None
 
+let rec fold_left (f : 'a -> 'b -> 'a reserr) (acc : 'a) : 'b list -> 'a reserr
+    = function
+  | [] -> ok acc
+  | x :: xs -> (
+      match f acc x with
+      | (Ok _, _) as acc ->
+          let* acc = acc in
+          fold_left f acc xs
+      | Error errs, ws ->
+          let* _ = warns ws and* _ = filter_errs errs in
+          fold_left f acc xs)
+
 let of_option ~default = Option.fold ~none:(error default) ~some:ok
 let to_option = function Ok x, _ -> Some x | _ -> None
 let map f l = List.map f l |> promote
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 02756ce4..834b34cb 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -59,6 +59,7 @@ val promote : 'a reserr list -> 'a list reserr
 val promote_opt : 'a reserr -> 'a option reserr
 (** [promote_opt r] is [promote] for a unique value *)
 
+val fold_left : ('a -> 'b -> 'a reserr) -> 'a -> 'b list -> 'a reserr
 val of_option : default:W.t -> 'a option -> 'a reserr
 val to_option : 'a reserr -> 'a option
 val map : ('a -> 'b reserr) -> 'a list -> 'b list reserr

From 00119f56d1f1614e9f2547cd5f5162706016afe5 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 13:49:46 +0200
Subject: [PATCH 02/27] Reorder warnings in reserr

---
 plugins/qcheck-stm/src/reserr.ml  | 68 +++++++++++++++----------------
 plugins/qcheck-stm/src/reserr.mli | 46 ++++++++++-----------
 2 files changed, 57 insertions(+), 57 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 1bb36112..cda21f9e 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -1,56 +1,56 @@
 module W = Ortac_core.Warnings
 
 type init_state_error =
-  | Not_a_function_call of string
-  | No_specification of string
+  | Mismatch_number_of_arguments of string
   | No_appropriate_specifications of string * string list
+  | No_specification of string
   | No_translatable_specification of string
+  | Not_a_function_call of string
   | Not_returning_sut of string
   | Qualified_name of string
-  | Mismatch_number_of_arguments of string
 
 type W.kind +=
   | Constant_value of string
-  | Returning_sut of string
-  | No_sut_argument of string
-  | Multiple_sut_arguments of string
-  | No_sut_type of string
-  | No_init_function of string
-  | Syntax_error_in_type of string
-  | Syntax_error_in_init_sut of string
-  | Sut_type_not_supported of string
-  | Type_parameter_not_instantiated of string
-  | Type_not_supported_for_sut_parameter of string
-  | Incompatible_type of (string * string)
-  | Sut_type_not_specified of string
-  | No_models of string
-  | No_spec of string
-  | Impossible_term_substitution of
-      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
-  | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
-  | Type_not_supported of string
-  | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
-  | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
+  | Ignored_modifies
+  | Impossible_init_state_generation of init_state_error
+  | Impossible_term_substitution of
+      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
   | Incompatible_sut of string
+  | Incompatible_type of (string * string)
   | Incomplete_ret_val_computation of string
+  | Multiple_sut_arguments of string
+  | No_init_function of string
+  | No_models of string
+  | No_spec of string
+  | No_sut_argument of string
+  | No_sut_type of string
+  | Returned_tuple of string
+  | Returning_sut of string
+  | Sut_type_not_specified of string
+  | Sut_type_not_supported of string
+  | Syntax_error_in_init_sut of string
+  | Syntax_error_in_type of string
+  | Type_not_supported of string
+  | Type_not_supported_for_sut_parameter of string
+  | Type_parameter_not_instantiated of string
 
 let level kind =
   match kind with
-  | Constant_value _ | Returning_sut _ | No_sut_argument _
-  | Multiple_sut_arguments _ | Incompatible_type _ | No_spec _
-  | Impossible_term_substitution _ | Ignored_modifies
-  | Ensures_not_found_for_next_state _ | Type_not_supported _
-  | Functional_argument _ | Returned_tuple _ | Ghost_values _
-  | Incomplete_ret_val_computation _ ->
+  | Constant_value _ | Ensures_not_found_for_next_state _
+  | Functional_argument _ | Ghost_values _ | Ignored_modifies
+  | Impossible_term_substitution _ | Incompatible_type _
+  | Incomplete_ret_val_computation _ | Multiple_sut_arguments _ | No_spec _
+  | No_sut_argument _ | Returned_tuple _ | Returning_sut _
+  | Type_not_supported _ ->
       W.Warning
-  | No_sut_type _ | No_init_function _ | Syntax_error_in_type _
-  | Sut_type_not_supported _ | Type_not_supported_for_sut_parameter _
-  | Syntax_error_in_init_sut _ | Type_parameter_not_instantiated _
-  | Sut_type_not_specified _ | No_models _ | Impossible_init_state_generation _
-  | Incompatible_sut _ ->
+  | Impossible_init_state_generation _ | Incompatible_sut _ | No_init_function _
+  | No_models _ | No_sut_type _ | Sut_type_not_specified _
+  | Sut_type_not_supported _ | Syntax_error_in_init_sut _
+  | Syntax_error_in_type _ | Type_not_supported_for_sut_parameter _
+  | Type_parameter_not_instantiated _ ->
       W.Error
   | _ -> W.level kind
 
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 834b34cb..1c6a3c76 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -1,41 +1,41 @@
 module W = Ortac_core.Warnings
 
 type init_state_error =
-  | Not_a_function_call of string
-  | No_specification of string
+  | Mismatch_number_of_arguments of string
   | No_appropriate_specifications of string * string list
+  | No_specification of string
   | No_translatable_specification of string
+  | Not_a_function_call of string
   | Not_returning_sut of string
   | Qualified_name of string
-  | Mismatch_number_of_arguments of string
 
 type W.kind +=
   | Constant_value of string
-  | Returning_sut of string
-  | No_sut_argument of string
-  | Multiple_sut_arguments of string
-  | No_sut_type of string
-  | No_init_function of string
-  | Syntax_error_in_type of string
-  | Syntax_error_in_init_sut of string
-  | Sut_type_not_supported of string
-  | Type_parameter_not_instantiated of string
-  | Type_not_supported_for_sut_parameter of string
-  | Incompatible_type of (string * string)
-  | Sut_type_not_specified of string
-  | No_models of string
-  | No_spec of string
-  | Impossible_term_substitution of
-      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
-  | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
-  | Type_not_supported of string
-  | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
-  | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
+  | Ignored_modifies
+  | Impossible_init_state_generation of init_state_error
+  | Impossible_term_substitution of
+      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
   | Incompatible_sut of string
+  | Incompatible_type of (string * string)
   | Incomplete_ret_val_computation of string
+  | Multiple_sut_arguments of string
+  | No_init_function of string
+  | No_models of string
+  | No_spec of string
+  | No_sut_argument of string
+  | No_sut_type of string
+  | Returned_tuple of string
+  | Returning_sut of string
+  | Sut_type_not_specified of string
+  | Sut_type_not_supported of string
+  | Syntax_error_in_init_sut of string
+  | Syntax_error_in_type of string
+  | Type_not_supported of string
+  | Type_not_supported_for_sut_parameter of string
+  | Type_parameter_not_instantiated of string
 
 type 'a reserr
 

From e627e3b5bfd764efc670600035352c0498a5c47e Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 13:50:52 +0200
Subject: [PATCH 03/27] Add new reserr errors

---
 plugins/qcheck-stm/src/reserr.ml  | 24 +++++++++++++++++++-----
 plugins/qcheck-stm/src/reserr.mli |  3 +++
 2 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index cda21f9e..53caf9ab 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -21,7 +21,9 @@ type W.kind +=
   | Incompatible_sut of string
   | Incompatible_type of (string * string)
   | Incomplete_ret_val_computation of string
+  | Incomplete_configuration_module of [ `Init_sut | `Sut ]
   | Multiple_sut_arguments of string
+  | No_configuration_file of string
   | No_init_function of string
   | No_models of string
   | No_spec of string
@@ -33,6 +35,7 @@ type W.kind +=
   | Sut_type_not_supported of string
   | Syntax_error_in_init_sut of string
   | Syntax_error_in_type of string
+  | Syntax_error_in_config_module of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string
   | Type_parameter_not_instantiated of string
@@ -46,11 +49,12 @@ let level kind =
   | No_sut_argument _ | Returned_tuple _ | Returning_sut _
   | Type_not_supported _ ->
       W.Warning
-  | Impossible_init_state_generation _ | Incompatible_sut _ | No_init_function _
-  | No_models _ | No_sut_type _ | Sut_type_not_specified _
-  | Sut_type_not_supported _ | Syntax_error_in_init_sut _
-  | Syntax_error_in_type _ | Type_not_supported_for_sut_parameter _
-  | Type_parameter_not_instantiated _ ->
+  | Impossible_init_state_generation _ | Incompatible_sut _
+  | Incomplete_configuration_module _ | No_init_function _ | No_models _
+  | No_sut_type _ | Sut_type_not_specified _ | Sut_type_not_supported _
+  | Syntax_error_in_init_sut _ | Syntax_error_in_type _
+  | Type_not_supported_for_sut_parameter _ | Type_parameter_not_instantiated _
+    ->
       W.Error
   | _ -> W.level kind
 
@@ -166,6 +170,8 @@ let pp_kind ppf kind =
   | No_init_function f -> pf ppf "Function %s not declared in the module" f
   | Syntax_error_in_type t -> pf ppf "Syntax error in type %s" t
   | Syntax_error_in_init_sut s -> pf ppf "Syntax error in OCaml expression %s" s
+  | Syntax_error_in_config_module s ->
+      pf ppf "Syntax error in OCaml configuration module %s" s
   | Sut_type_not_supported ty ->
       pf ppf "Unsupported SUT type %s:@ %a" ty text
         "SUT type must be a type constructor, possibly applied to type \
@@ -179,6 +185,7 @@ let pp_kind ppf kind =
          type"
   | Sut_type_not_specified ty ->
       pf ppf "Missing specification for the SUT type %s" ty
+  | No_configuration_file file -> pf ppf "Missing configuration file %s" file
   | No_models ty -> pf ppf "Missing model(s) for the SUT type %s" ty
   | Impossible_init_state_generation (Not_a_function_call fct) ->
       pf ppf "Unsupported INIT expression %s:@ %a" fct text
@@ -213,6 +220,13 @@ let pp_kind ppf kind =
       pf ppf "Error in INIT expression %s:@ %a" fct text
         "mismatch in the number of arguments between the INIT expression and \
          the function specification"
+  | Incomplete_configuration_module missing ->
+      let what =
+        match missing with
+        | `Init_sut -> "the init_sut value declaration"
+        | `Sut -> "the sut type declaration"
+      in
+      pf ppf "Incomplete configuration module: it is missing %s" what
   | Incompatible_sut t ->
       pf ppf "Incompatible declaration of SUT type:@ %a%s" text
         "the declaration of the SUT type is incompatible with the configured \
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 1c6a3c76..378645df 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -20,8 +20,10 @@ type W.kind +=
       [ `Never | `New | `Old | `NotModel | `OutOfScope ]
   | Incompatible_sut of string
   | Incompatible_type of (string * string)
+  | Incomplete_configuration_module of [ `Init_sut | `Sut ]
   | Incomplete_ret_val_computation of string
   | Multiple_sut_arguments of string
+  | No_configuration_file of string
   | No_init_function of string
   | No_models of string
   | No_spec of string
@@ -33,6 +35,7 @@ type W.kind +=
   | Sut_type_not_supported of string
   | Syntax_error_in_init_sut of string
   | Syntax_error_in_type of string
+  | Syntax_error_in_config_module of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string
   | Type_parameter_not_instantiated of string

From 79a1bb9a0baee88d7f08ba1f9e7dc5fa49c455a8 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 13:43:13 +0200
Subject: [PATCH 04/27] Change command-line interface for a module-base config

This commit also setup how to run the scan of the configuration module,
without implementing any logic yet.
---
 plugins/qcheck-stm/src/config.ml           | 36 ++++++++++++++++++----
 plugins/qcheck-stm/src/ortac_qcheck_stm.ml | 30 +++++-------------
 plugins/qcheck-stm/src/stm_of_ir.ml        | 15 ++-------
 3 files changed, 40 insertions(+), 41 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index 58e59f97..f9614f9f 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -2,6 +2,13 @@ open Gospel
 open Ortac_core
 open Ppxlib
 
+type config_under_construction = {
+  sut_core_type' : Ppxlib.core_type option;
+  init_sut' : Ppxlib.expression option;
+}
+
+let config_under_construction = { sut_core_type' = None; init_sut' = None }
+
 type t = {
   context : Context.t;
   sut_core_type : Ppxlib.core_type;
@@ -9,6 +16,20 @@ type t = {
   init_sut_txt : string;
 }
 
+let mk_config context cfg_uc =
+  let open Reserr in
+  let* sut_core_type =
+    of_option
+      ~default:(Incomplete_configuration_module `Sut, Location.none)
+      cfg_uc.sut_core_type'
+  and* init_sut =
+    of_option
+      ~default:(Incomplete_configuration_module `Init_sut, Location.none)
+      cfg_uc.init_sut'
+  in
+  let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut in
+  ok { context; sut_core_type; init_sut; init_sut_txt }
+
 let get_sut_type_name config =
   let open Ppxlib in
   match config.sut_core_type.ptyp_desc with
@@ -75,11 +96,13 @@ let init_sut_from_string str =
   try Parse.expression (Lexing.from_string str) |> Reserr.ok
   with _ -> Reserr.(error (Syntax_error_in_init_sut str, Location.none))
 
-let init path init_sut_txt sut_str =
+let scan_config cfg_uc _ = Reserr.ok cfg_uc
+
+let init gospel config_module =
   let open Reserr in
   try
-    let module_name = Utils.module_name_of_path path in
-    Parser_frontend.parse_ocaml_gospel path |> Utils.type_check [] path
+    let module_name = Utils.module_name_of_path gospel in
+    Parser_frontend.parse_ocaml_gospel gospel |> Utils.type_check [] gospel
     |> fun (env, sigs) ->
     assert (List.length env = 1);
     let namespace = List.hd env in
@@ -96,8 +119,9 @@ let init path init_sut_txt sut_str =
       | _ -> ctx
     in
     let context = List.fold_left add context sigs in
-    let* sut_core_type = sut_core_type sut_str
-    and* init_sut = init_sut_from_string init_sut_txt in
-    ok (sigs, { context; sut_core_type; init_sut; init_sut_txt })
+    let* config =
+      scan_config config_under_construction config_module >>= mk_config context
+    in
+    ok (sigs, config)
   with Gospel.Warnings.Error (l, k) ->
     error (Ortac_core.Warnings.GospelError k, l)
diff --git a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml
index 345d4fd0..991dc530 100644
--- a/plugins/qcheck-stm/src/ortac_qcheck_stm.ml
+++ b/plugins/qcheck-stm/src/ortac_qcheck_stm.ml
@@ -4,14 +4,14 @@ module Ir_of_gospel = Ir_of_gospel
 module Reserr = Reserr
 module Stm_of_ir = Stm_of_ir
 
-let main path init sut include_ output quiet () =
+let main path config output quiet () =
   let open Reserr in
   let fmt = Registration.get_out_formatter output in
   let pp = pp quiet Ppxlib_ast.Pprintast.structure fmt in
   pp
-    (let* sigs, config = Config.init path init sut in
+    (let* sigs, config = Config.init path config in
      let* ir = Ir_of_gospel.run sigs config in
-     Stm_of_ir.stm include_ config ir)
+     Stm_of_ir.stm config ir)
 
 open Cmdliner
 
@@ -22,33 +22,19 @@ end = struct
     Cmd.info "qcheck-stm"
       ~doc:"Generate QCheck-stm test file according to Gospel specifications."
 
-  let sut =
-    Arg.(
-      required
-      & pos 2 (some string) None
-      & info [] ~doc:"Build the qcheck-stm tests with SUT." ~docv:"SUT")
-
-  let init =
+  let config =
     Arg.(
       required
       & pos 1 (some string) None
       & info []
           ~doc:
-            "Build the qcheck-stm tests using INIT function to initialize the \
-             system under test."
-          ~docv:"INIT")
+            "Build the qcheck-stm tests using CONFIG module as configuration \
+             file."
+          ~docv:"CONFIG")
 
   let term =
     let open Registration in
-    Term.(
-      const main
-      $ ocaml_file
-      $ init
-      $ sut
-      $ include_
-      $ output_file
-      $ quiet
-      $ setup_log)
+    Term.(const main $ ocaml_file $ config $ output_file $ quiet $ setup_log)
 
   let cmd = Cmd.v info term
 end
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index c3d785fc..064beeba 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -932,23 +932,12 @@ let agree_prop =
       check_init_state ();
       STMTests.agree_prop cs]
 
-let stm include_ config ir =
+let stm config ir =
   let open Reserr in
   let* ghost_types = ghost_types config ir.ghost_types in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
   let warn = [%stri [@@@ocaml.warning "-26-27"]] in
-  let incl =
-    Option.map
-      (fun m ->
-        let open Ast_helper in
-        String.capitalize_ascii m
-        |> lident
-        |> Mod.ident
-        |> Incl.mk
-        |> pstr_include)
-      include_
-    |> Option.to_list
-  in
+  let incl = [] in
   let sut = sut_type config in
   let cmd = cmd_type ir in
   let* cmd_show = cmd_show config ir in

From 48d160c766e00a683f8b20f40833f377920718fc Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 14:23:24 +0200
Subject: [PATCH 05/27] Setup parsing parsing of the configuration module

---
 plugins/qcheck-stm/src/config.ml | 37 ++++++++++++++++++--------------
 1 file changed, 21 insertions(+), 16 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index f9614f9f..8ea28b9d 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -54,11 +54,6 @@ let dump ppf t =
     pf ppf "sut_core_type: %a; init_sut: %a@." Ppxlib_ast.Pprintast.expression
       t.init_sut Ppxlib_ast.Pprintast.core_type t.sut_core_type)
 
-let core_type_of_string t =
-  let open Reserr in
-  try Ppxlib.Parse.core_type (Lexing.from_string t) |> ok
-  with _ -> error (Syntax_error_in_type t, Location.none)
-
 let rec acceptable_type_parameter param =
   let open Ppxlib in
   let open Reserr in
@@ -85,18 +80,28 @@ let core_type_is_a_well_formed_sut (core_type : Ppxlib.core_type) =
       let str = Fmt.str "%a" Ppxlib_ast.Pprintast.core_type core_type in
       error (Sut_type_not_supported str, Location.none)
 
-let sut_core_type str =
+let scan_config cfg_uc config_mod =
   let open Reserr in
-  let* sut_core_type = core_type_of_string str in
-  let* _ = core_type_is_a_well_formed_sut sut_core_type in
-  ok sut_core_type
-
-let init_sut_from_string str =
-  let open Ppxlib in
-  try Parse.expression (Lexing.from_string str) |> Reserr.ok
-  with _ -> Reserr.(error (Syntax_error_in_init_sut str, Location.none))
-
-let scan_config cfg_uc _ = Reserr.ok cfg_uc
+  let* ic =
+    try ok @@ open_in config_mod
+    with _ -> error (No_configuration_file config_mod, Location.none)
+  in
+  let lb = Lexing.from_channel ic in
+  let () = Lexing.set_filename lb config_mod in
+  let* _ast =
+    try ok @@ Ppxlib.Parse.implementation lb
+    with _ ->
+      error
+        ( Syntax_error_in_config_module config_mod,
+          Location.
+            {
+              loc_start = lb.lex_start_p;
+              loc_end = lb.lex_curr_p;
+              loc_ghost = false;
+            } )
+  in
+  close_in ic;
+  ok cfg_uc
 
 let init gospel config_module =
   let open Reserr in

From 719995ae7966044aa6e57beb20c6943c872ec075 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 14:24:04 +0200
Subject: [PATCH 06/27] Remove unused errors from reserr

---
 plugins/qcheck-stm/src/reserr.ml  | 10 +++-------
 plugins/qcheck-stm/src/reserr.mli |  2 --
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 53caf9ab..1de434ac 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -33,8 +33,6 @@ type W.kind +=
   | Returning_sut of string
   | Sut_type_not_specified of string
   | Sut_type_not_supported of string
-  | Syntax_error_in_init_sut of string
-  | Syntax_error_in_type of string
   | Syntax_error_in_config_module of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string
@@ -50,9 +48,9 @@ let level kind =
   | Type_not_supported _ ->
       W.Warning
   | Impossible_init_state_generation _ | Incompatible_sut _
-  | Incomplete_configuration_module _ | No_init_function _ | No_models _
-  | No_sut_type _ | Sut_type_not_specified _ | Sut_type_not_supported _
-  | Syntax_error_in_init_sut _ | Syntax_error_in_type _
+  | Incomplete_configuration_module _ | No_configuration_file _
+  | No_init_function _ | No_models _ | No_sut_type _ | Sut_type_not_specified _
+  | Sut_type_not_supported _ | Syntax_error_in_config_module _
   | Type_not_supported_for_sut_parameter _ | Type_parameter_not_instantiated _
     ->
       W.Error
@@ -168,8 +166,6 @@ let pp_kind ppf kind =
   (* Errors *)
   | No_sut_type ty -> pf ppf "Type %s not declared in the module" ty
   | No_init_function f -> pf ppf "Function %s not declared in the module" f
-  | Syntax_error_in_type t -> pf ppf "Syntax error in type %s" t
-  | Syntax_error_in_init_sut s -> pf ppf "Syntax error in OCaml expression %s" s
   | Syntax_error_in_config_module s ->
       pf ppf "Syntax error in OCaml configuration module %s" s
   | Sut_type_not_supported ty ->
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 378645df..708d074a 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -33,8 +33,6 @@ type W.kind +=
   | Returning_sut of string
   | Sut_type_not_specified of string
   | Sut_type_not_supported of string
-  | Syntax_error_in_init_sut of string
-  | Syntax_error_in_type of string
   | Syntax_error_in_config_module of string
   | Type_not_supported of string
   | Type_not_supported_for_sut_parameter of string

From f0c3e15f108d7af15e9cf48f77a264f7ae246bbd Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 26 Mar 2024 16:46:05 +0100
Subject: [PATCH 07/27] Add the logic of scanning the configuration module

This still doesn't implement what to do at each element of the
configuration though.
---
 plugins/qcheck-stm/src/config.ml | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index 8ea28b9d..901fa16a 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -88,7 +88,7 @@ let scan_config cfg_uc config_mod =
   in
   let lb = Lexing.from_channel ic in
   let () = Lexing.set_filename lb config_mod in
-  let* _ast =
+  let* ast =
     try ok @@ Ppxlib.Parse.implementation lb
     with _ ->
       error
@@ -101,7 +101,25 @@ let scan_config cfg_uc config_mod =
             } )
   in
   close_in ic;
-  ok cfg_uc
+  let aux cfg_uc (str : structure_item) =
+    match str.pstr_desc with
+    | Pstr_eval (_, _) -> ok cfg_uc
+    | Pstr_value (_, _) -> ok cfg_uc
+    | Pstr_primitive _ -> ok cfg_uc
+    | Pstr_type (_, _) -> ok cfg_uc
+    | Pstr_typext _ -> ok cfg_uc
+    | Pstr_exception _ -> ok cfg_uc
+    | Pstr_module _ -> ok cfg_uc
+    | Pstr_recmodule _ -> ok cfg_uc
+    | Pstr_modtype _ -> ok cfg_uc
+    | Pstr_open _ -> ok cfg_uc
+    | Pstr_class _ -> ok cfg_uc
+    | Pstr_class_type _ -> ok cfg_uc
+    | Pstr_include _ -> ok cfg_uc
+    | Pstr_attribute _ -> ok cfg_uc
+    | Pstr_extension (_, _) -> ok cfg_uc
+  in
+  fold_left aux cfg_uc ast
 
 let init gospel config_module =
   let open Reserr in

From 0a4293c1c2be2e5c3526746033c3ba3ee23eca2c Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 26 Mar 2024 19:45:31 +0100
Subject: [PATCH 08/27] Process values to look for `init_sut`

As before, checking the expression is in the expected form is postponed
to `Ir_of_gospel`
---
 plugins/qcheck-stm/src/config.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index 901fa16a..2e28f8d0 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -80,6 +80,21 @@ let core_type_is_a_well_formed_sut (core_type : Ppxlib.core_type) =
       let str = Fmt.str "%a" Ppxlib_ast.Pprintast.core_type core_type in
       error (Sut_type_not_supported str, Location.none)
 
+(* Inspect value definition in config module in order to collect information
+   about:
+   - the definition of the [init_sut] function *)
+let value_bindings cfg_uc =
+  let open Reserr in
+  let aux cfg_uc vb =
+    let open Ppxlib in
+    match vb.pvb_pat.ppat_desc with
+    | Ppat_var s when String.equal "init_sut" s.txt ->
+        let init_sut' = Some vb.pvb_expr in
+        ok { cfg_uc with init_sut' }
+    | _ -> ok cfg_uc
+  in
+  fold_left aux cfg_uc
+
 let scan_config cfg_uc config_mod =
   let open Reserr in
   let* ic =
@@ -104,7 +119,7 @@ let scan_config cfg_uc config_mod =
   let aux cfg_uc (str : structure_item) =
     match str.pstr_desc with
     | Pstr_eval (_, _) -> ok cfg_uc
-    | Pstr_value (_, _) -> ok cfg_uc
+    | Pstr_value (_, xs) -> value_bindings cfg_uc xs
     | Pstr_primitive _ -> ok cfg_uc
     | Pstr_type (_, _) -> ok cfg_uc
     | Pstr_typext _ -> ok cfg_uc

From 552717815063376bf013301c84d9743290e49bda Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 16 Apr 2024 16:22:38 +0200
Subject: [PATCH 09/27] Use init_sut_txt and location from config file

---
 plugins/qcheck-stm/src/ir_of_gospel.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml
index 6c649dc8..ec1d93a1 100644
--- a/plugins/qcheck-stm/src/ir_of_gospel.ml
+++ b/plugins/qcheck-stm/src/ir_of_gospel.ml
@@ -305,8 +305,8 @@ let init_state config state sigs =
     | expr ->
         error
           ( Impossible_init_state_generation
-              (Not_a_function_call (Fmt.str "%a" Pprintast.expression expr)),
-            Location.none )
+              (Not_a_function_call config.init_sut_txt),
+            expr.pexp_loc )
   in
   let* fct_str =
     match fct with
@@ -349,9 +349,8 @@ let init_state config state sigs =
     with Invalid_argument _ ->
       error
         ( Impossible_init_state_generation
-            (Mismatch_number_of_arguments
-               (Fmt.str "%a" Pprintast.expression config.init_sut)),
-          Location.none )
+            (Mismatch_number_of_arguments config.init_sut_txt),
+          config.init_sut.pexp_loc )
   in
   let open Gospel.Symbols in
   let rec return_type ty =

From 3e0d6b098aabbbcba2754612989a28add61dfa0c Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 27 Mar 2024 11:22:49 +0100
Subject: [PATCH 10/27] Process type declarations to find the type `sut`

---
 plugins/qcheck-stm/src/config.ml | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index 2e28f8d0..ffde446a 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -73,9 +73,9 @@ let core_type_is_a_well_formed_sut (core_type : Ppxlib.core_type) =
   let open Ppxlib in
   let open Reserr in
   match core_type.ptyp_desc with
-  | Ptyp_constr (lid, cts) ->
+  | Ptyp_constr (_lid, cts) ->
       let* _ = map acceptable_type_parameter cts in
-      ok (lid, cts)
+      ok ()
   | _ ->
       let str = Fmt.str "%a" Ppxlib_ast.Pprintast.core_type core_type in
       error (Sut_type_not_supported str, Location.none)
@@ -95,6 +95,27 @@ let value_bindings cfg_uc =
   in
   fold_left aux cfg_uc
 
+(* Inspect type definition in config module in order to collect information
+   about:
+   - the definition of the [sut] type *)
+let type_declarations cfg_uc =
+  let open Reserr in
+  let aux cfg_uc (td : type_declaration) =
+    let open Ppxlib in
+    if String.equal "sut" td.ptype_name.txt then
+      let* manifest =
+        of_option
+          ~default:
+            ( Sut_type_not_supported (Fmt.str "%a" Pprintast.type_declaration td),
+              td.ptype_loc )
+          td.ptype_manifest
+      in
+      let* () = core_type_is_a_well_formed_sut manifest in
+      ok { cfg_uc with sut_core_type' = Some manifest }
+    else ok cfg_uc
+  in
+  fold_left aux cfg_uc
+
 let scan_config cfg_uc config_mod =
   let open Reserr in
   let* ic =
@@ -121,7 +142,7 @@ let scan_config cfg_uc config_mod =
     | Pstr_eval (_, _) -> ok cfg_uc
     | Pstr_value (_, xs) -> value_bindings cfg_uc xs
     | Pstr_primitive _ -> ok cfg_uc
-    | Pstr_type (_, _) -> ok cfg_uc
+    | Pstr_type (_, xs) -> type_declarations cfg_uc xs
     | Pstr_typext _ -> ok cfg_uc
     | Pstr_exception _ -> ok cfg_uc
     | Pstr_module _ -> ok cfg_uc

From f8bad7f6076464c43cb2fec94207a509cb2a6756 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 27 Mar 2024 14:53:45 +0100
Subject: [PATCH 11/27] Update tests to use the new interface

---
 .../qcheck-stm/test/all_warnings_config.ml    |   5 +
 plugins/qcheck-stm/test/array_config.ml       |   5 +
 .../test/conjunctive_clauses_config.ml        |   5 +
 plugins/qcheck-stm/test/dune                  |   6 +-
 plugins/qcheck-stm/test/dune.inc              |  53 ++-------
 plugins/qcheck-stm/test/dune_gen.args         |  18 +--
 plugins/qcheck-stm/test/dune_gen.ml           |  13 ++-
 .../qcheck-stm/test/ghost_as_model_config.ml  |   5 +
 plugins/qcheck-stm/test/hashtbl_config.ml     |   5 +
 .../test/integer_in_model_config.ml           |   5 +
 plugins/qcheck-stm/test/invariants_config.ml  |   5 +
 plugins/qcheck-stm/test/record_config.ml      |   5 +
 plugins/qcheck-stm/test/ref_config.ml         |   5 +
 .../qcheck-stm/test/sequence_model_config.ml  |   5 +
 plugins/qcheck-stm/test/test_errors.t         | 106 +++++++++++++-----
 15 files changed, 153 insertions(+), 93 deletions(-)
 create mode 100644 plugins/qcheck-stm/test/all_warnings_config.ml
 create mode 100644 plugins/qcheck-stm/test/array_config.ml
 create mode 100644 plugins/qcheck-stm/test/conjunctive_clauses_config.ml
 create mode 100644 plugins/qcheck-stm/test/ghost_as_model_config.ml
 create mode 100644 plugins/qcheck-stm/test/hashtbl_config.ml
 create mode 100644 plugins/qcheck-stm/test/integer_in_model_config.ml
 create mode 100644 plugins/qcheck-stm/test/invariants_config.ml
 create mode 100644 plugins/qcheck-stm/test/record_config.ml
 create mode 100644 plugins/qcheck-stm/test/ref_config.ml
 create mode 100644 plugins/qcheck-stm/test/sequence_model_config.ml

diff --git a/plugins/qcheck-stm/test/all_warnings_config.ml b/plugins/qcheck-stm/test/all_warnings_config.ml
new file mode 100644
index 00000000..2b4b3a6b
--- /dev/null
+++ b/plugins/qcheck-stm/test/all_warnings_config.ml
@@ -0,0 +1,5 @@
+open All_warnings
+
+let init_sut = make 16 'a'
+
+type sut = char t
diff --git a/plugins/qcheck-stm/test/array_config.ml b/plugins/qcheck-stm/test/array_config.ml
new file mode 100644
index 00000000..47c880b1
--- /dev/null
+++ b/plugins/qcheck-stm/test/array_config.ml
@@ -0,0 +1,5 @@
+open Array
+
+let init_sut = make 16 'a'
+
+type sut = char t
diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_config.ml b/plugins/qcheck-stm/test/conjunctive_clauses_config.ml
new file mode 100644
index 00000000..d092e574
--- /dev/null
+++ b/plugins/qcheck-stm/test/conjunctive_clauses_config.ml
@@ -0,0 +1,5 @@
+open Conjunctive_clauses
+
+let init_sut = make 42 'a'
+
+type sut = char t
diff --git a/plugins/qcheck-stm/test/dune b/plugins/qcheck-stm/test/dune
index 6b6dd33c..315851f3 100644
--- a/plugins/qcheck-stm/test/dune
+++ b/plugins/qcheck-stm/test/dune
@@ -19,7 +19,11 @@
    (ignore-stdout
     (with-stderr-to
      %{target}
-     (run ortac qcheck-stm %{dep:all_warnings.mli} "make 16 'a'" "char t"))))))
+     (run
+      ortac
+      qcheck-stm
+      %{dep:all_warnings.mli}
+      %{dep:all_warnings_config.ml}))))))
 
 (rule
  (alias runtest)
diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc
index f4dc4ea0..2bb22c0d 100644
--- a/plugins/qcheck-stm/test/dune.inc
+++ b/plugins/qcheck-stm/test/dune.inc
@@ -18,7 +18,7 @@
      ortac
      qcheck-stm
      %{dep:array.mli}
-     "make 16 'a'" "char t"
+     %{dep:array_config.ml}
      -o
      %{target})))))
 
@@ -71,7 +71,7 @@
      ortac
      qcheck-stm
      %{dep:hashtbl.mli}
-     "create ~random:false 16" "(char, int) t"
+     %{dep:hashtbl_config.ml}
      -o
      %{target})))))
 
@@ -124,7 +124,7 @@
      ortac
      qcheck-stm
      %{dep:record.mli}
-     "make 42" "t"
+     %{dep:record_config.ml}
      -o
      %{target})))))
 
@@ -177,7 +177,7 @@
      ortac
      qcheck-stm
      %{dep:ref.mli}
-     "make 42" "t"
+     %{dep:ref_config.ml}
      -o
      %{target})))))
 
@@ -230,7 +230,7 @@
      ortac
      qcheck-stm
      %{dep:conjunctive_clauses.mli}
-     "make 42 'a'" "char t"
+     %{dep:conjunctive_clauses_config.ml}
      -o
      %{target})))))
 
@@ -283,7 +283,7 @@
      ortac
      qcheck-stm
      %{dep:sequence_model.mli}
-     "create ()" "char t"
+     %{dep:sequence_model_config.ml}
      -o
      %{target})))))
 
@@ -336,7 +336,7 @@
      ortac
      qcheck-stm
      %{dep:invariants.mli}
-     "create 42" "int t"
+     %{dep:invariants_config.ml}
      -o
      %{target})))))
 
@@ -373,26 +373,6 @@
  (name integer_in_model)
  (modules integer_in_model))
 
-(rule
- (target integer_in_model_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
-    integer_in_model_errors
-    (run
-     ortac
-     qcheck-stm
-     %{dep:integer_in_model.mli}
-     "create ()" "t"
-     -o
-     %{target})))))
-
 (test
  (name integer_in_model_stm_tests)
  (package ortac-qcheck-stm)
@@ -426,25 +406,6 @@
  (name ghost_as_model)
  (modules ghost_as_model))
 
-(rule
- (target ghost_as_model_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
-    ghost_as_model_errors
-    (run
-     ortac
-     qcheck-stm
-     %{dep:ghost_as_model.mli}
-     "create ()" "t"
-     -o
-     %{target})))))
 
 (test
  (name ghost_as_model_stm_tests)
diff --git a/plugins/qcheck-stm/test/dune_gen.args b/plugins/qcheck-stm/test/dune_gen.args
index 7d103a08..d075fc50 100644
--- a/plugins/qcheck-stm/test/dune_gen.args
+++ b/plugins/qcheck-stm/test/dune_gen.args
@@ -1,18 +1,18 @@
 array
-"make 16 'a'" "char t"
+array_config
 hashtbl
-"create ~random:false 16" "(char, int) t"
+hashtbl_config
 record
-"make 42" "t"
+record_config
 ref
-"make 42" "t"
+ref_config
 conjunctive_clauses
-"make 42 'a'" "char t"
+conjunctive_clauses_config
 sequence_model
-"create ()" "char t"
+sequence_model_config
 invariants
-"create 42" "int t"
+invariants_config
 integer_in_model
-"create ()" "t"
+integer_in_model_config
 ghost_as_model
-"create ()" "t"
+ghost_as_model_config
diff --git a/plugins/qcheck-stm/test/dune_gen.ml b/plugins/qcheck-stm/test/dune_gen.ml
index 57e5fe29..ee613352 100644
--- a/plugins/qcheck-stm/test/dune_gen.ml
+++ b/plugins/qcheck-stm/test/dune_gen.ml
@@ -1,15 +1,16 @@
 (* Generates the boiler-plater dune configuration for tests
 
-     dune_gen.exe array "\"make 16 'a'\" \"char t\"" ...
-   will generate the dune rules for the array module. *)
+     dune_gen.exe array array_config ...
+   will generate the dune rules for the array module with the array_config
+   configuration. *)
 
 let usage () =
-  Printf.fprintf stderr "Usage: %s [MODULE INIT_SUT] ..." Sys.argv.(0);
+  Printf.fprintf stderr "Usage: %s [MODULE CONFIGURATION] ..." Sys.argv.(0);
   exit 1
 
 let rec print_rules pos =
   if pos < Array.length Sys.argv then (
-    let m = Sys.argv.(pos) and init_sut = Sys.argv.(pos + 1) in
+    let m = Sys.argv.(pos) and config = Sys.argv.(pos + 1) in
     Printf.printf
       {|(library
  (name %s)
@@ -31,7 +32,7 @@ let rec print_rules pos =
      ortac
      qcheck-stm
      %%{dep:%s.mli}
-     %s
+     %%{dep:%s.ml}
      -o
      %%{target})))))
 
@@ -65,7 +66,7 @@ let rec print_rules pos =
   (run %%{dep:%s_stm_tests.exe} -v)))
 
 |}
-      m m m m m init_sut m m m m m m m m m;
+      m m m m m config m m m m m m m m m;
     print_rules (pos + 2))
 
 let () =
diff --git a/plugins/qcheck-stm/test/ghost_as_model_config.ml b/plugins/qcheck-stm/test/ghost_as_model_config.ml
new file mode 100644
index 00000000..be1f0717
--- /dev/null
+++ b/plugins/qcheck-stm/test/ghost_as_model_config.ml
@@ -0,0 +1,5 @@
+open Ghost_as_model
+
+type sut = t
+
+let init_sut = create ()
diff --git a/plugins/qcheck-stm/test/hashtbl_config.ml b/plugins/qcheck-stm/test/hashtbl_config.ml
new file mode 100644
index 00000000..d11dbb62
--- /dev/null
+++ b/plugins/qcheck-stm/test/hashtbl_config.ml
@@ -0,0 +1,5 @@
+open Hashtbl
+
+let init_sut = create ~random:false 16
+
+type sut = (char, int) t
diff --git a/plugins/qcheck-stm/test/integer_in_model_config.ml b/plugins/qcheck-stm/test/integer_in_model_config.ml
new file mode 100644
index 00000000..cb6841cf
--- /dev/null
+++ b/plugins/qcheck-stm/test/integer_in_model_config.ml
@@ -0,0 +1,5 @@
+open Integer_in_model
+
+type sut = t
+
+let init_sut = create ()
diff --git a/plugins/qcheck-stm/test/invariants_config.ml b/plugins/qcheck-stm/test/invariants_config.ml
new file mode 100644
index 00000000..1ecc119b
--- /dev/null
+++ b/plugins/qcheck-stm/test/invariants_config.ml
@@ -0,0 +1,5 @@
+open Invariants
+
+let init_sut = create 42
+
+type sut = int t
diff --git a/plugins/qcheck-stm/test/record_config.ml b/plugins/qcheck-stm/test/record_config.ml
new file mode 100644
index 00000000..514fae75
--- /dev/null
+++ b/plugins/qcheck-stm/test/record_config.ml
@@ -0,0 +1,5 @@
+open Record
+
+let init_sut = make 42
+
+type sut = t
diff --git a/plugins/qcheck-stm/test/ref_config.ml b/plugins/qcheck-stm/test/ref_config.ml
new file mode 100644
index 00000000..b0de43bd
--- /dev/null
+++ b/plugins/qcheck-stm/test/ref_config.ml
@@ -0,0 +1,5 @@
+open Ref
+
+let init_sut = make 42
+
+type sut = t
diff --git a/plugins/qcheck-stm/test/sequence_model_config.ml b/plugins/qcheck-stm/test/sequence_model_config.ml
new file mode 100644
index 00000000..3eafb730
--- /dev/null
+++ b/plugins/qcheck-stm/test/sequence_model_config.ml
@@ -0,0 +1,5 @@
+open Sequence_model
+
+let init_sut = create ()
+
+type sut = char t
diff --git a/plugins/qcheck-stm/test/test_errors.t b/plugins/qcheck-stm/test/test_errors.t
index 311aee9a..dacdc11d 100644
--- a/plugins/qcheck-stm/test/test_errors.t
+++ b/plugins/qcheck-stm/test/test_errors.t
@@ -3,41 +3,55 @@ command-line fail, so we load only the `qcheck-stm` plugin:
 
   $ export ORTAC_ONLY_PLUGIN=qcheck-stm
 
-We can make a syntax error in either the expression for the `init` function, or
-in the type declaration for the sytem under test:
+We can forget to write the configuration file:
 
   $ cat > foo.mli << EOF
   > type 'a t
   > val make : 'a -> 'a t
   > EOF
-  $ ortac qcheck-stm foo.mli "" "int t"
-  Error: Syntax error in OCaml expression .
-  $ ortac qcheck-stm foo.mli "make 42" ""
-  Error: Syntax error in type .
+  $ ortac qcheck-stm foo.mli foo_config.ml
+  Error: Missing configuration file foo_config.ml.
 
 We can give a pair as SUT type:
 
-  $ ortac qcheck-stm foo.mli "make 42" "int * bool"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = int * bool
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Unsupported SUT type (int * bool): SUT type must be a type
          constructor, possibly applied to type arguments.
 
 We can give a functional argument to the SUT type:
 
-  $ ortac qcheck-stm foo.mli "make 42" "(int -> bool) t"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = (int -> bool) t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Unsupported type parameter int -> bool: only constructors and tuples
          are supported in arguments for the SUT type.
 
 We can give a type that does not exist in the module as the system under test:
 
-  $ cat > foo.mli << EOF
-  > type 'a t
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = ty
   > EOF
-  $ ortac qcheck-stm foo.mli "()" "ty"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Type ty not declared in the module.
 
 Or forget its argument:
 
-  $ ortac qcheck-stm foo.mli "()" "t"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 1, characters 0-9:
   1 | type 'a t
       ^^^^^^^^^
@@ -50,19 +64,23 @@ Or forget its argument:
 
 We can forget to instantiate the type parameter of the system under test:
 
-  $ cat > foo.mli << EOF
-  > type 'a t
-  > val make : 'a -> 'a t
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = 'a t
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "'a t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Unsupported type parameter 'a: SUT type should be fully instantiated.
 
-We can forget to specify the type of the system under test:
+We can forget to specify the type of the system under test (which is already
+the case in `foo.mli`):
 
-  $ cat > foo.mli << EOF
-  > type 'a t
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = int t
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 1, characters 0-9:
   1 | type 'a t
       ^^^^^^^^^
@@ -74,7 +92,7 @@ Or specify it without any model:
   > type 'a t
   > (*@ ephemeral *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 2, characters 3-14:
   2 | (*@ ephemeral *)
          ^^^^^^^^^^^
@@ -86,7 +104,7 @@ We can give a non-existing function for `init_state`:
   > type 'a t
   > (*@ mutable model value : 'a *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Function make not declared in the module.
 
 We can forget to specify the function used for the `init_state` function:
@@ -96,7 +114,7 @@ We can forget to specify the function used for the `init_state` function:
   > (*@ mutable model value : 'a list *)
   > val make : 'a -> 'a t
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 3, characters 0-21:
   3 | val make : 'a -> 'a t
       ^^^^^^^^^^^^^^^^^^^^^
@@ -115,7 +133,7 @@ Or specify it in a manner that does not allow to deduce the complete `state`:
   >     requires true
   >     ensures t.max_size = 123 *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 6, characters 3-62:
   6 | ... t = make a
   7 |     requires true
@@ -134,7 +152,7 @@ Or specify it using clauses that cannot be executed:
   >     requires true
   >     ensures t.value = if forall i. i = i then a :: [] else [] *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Unsupported INIT function: the specification of the function called in
          the INIT expression does not provide a translatable specification for
          the following field of the model: value.
@@ -152,7 +170,7 @@ Or we can give a function that does not return the type of the system under test
   > (*@ make i
   >     modifies () *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ ortac qcheck-stm foo.mli foo_config.ml
   File "foo.mli", line 3, characters 0-52:
   3 | val make : int -> unit
   4 | (*@ make i
@@ -166,7 +184,15 @@ We are expected to give a function call as expression for the `init_state` funct
   > type 'a t
   > (*@ mutable model value : 'a *)
   > EOF
-  $ ortac qcheck-stm foo.mli "42" "int t"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = 42
+  > type sut = int t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
+  File "foo_config.ml", line 2, characters 15-17:
+  2 | let init_sut = 42
+                     ^^
   Error: Unsupported INIT expression 42: the INIT expression is expected to be
          a function call (the specification of that function is required to
          initialize the model state).
@@ -177,8 +203,12 @@ It also does not support qualified names:
   > type 'a t
   > (*@ mutable model value : 'a *)
   > EOF
-  $ ortac qcheck-stm foo.mli "Bar.make 42" "int t"
-  Error: Unsupported INIT function Bar.make: qualified names are not yet
+  $ cat > foo_config.ml << EOF
+  > let init_sut = Foo.make 42
+  > type sut = int t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
+  Error: Unsupported INIT function Foo.make: qualified names are not yet
          supported.
 
 It checks the number of arguments in the function call:
@@ -190,9 +220,18 @@ It checks the number of arguments in the function call:
   > (*@ t = make a
   >     ensures t.value = a *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42 73" "int t"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42 73
+  > type sut = int t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
+  File "foo_config.ml", line 2, characters 15-25:
+  2 | let init_sut = make 42 73
+                     ^^^^^^^^^^
   Error: Error in INIT expression make 42 73: mismatch in the number of
          arguments between the INIT expression and the function specification.
+
 We shouldn't be able to define a model by itsef in the `make` function:
   $ cat > foo.mli << EOF
   > type 'a t
@@ -202,7 +241,12 @@ We shouldn't be able to define a model by itsef in the `make` function:
   >     requires true
   >     ensures t.value = t.value *)
   > EOF
-  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  $ cat > foo_config.ml << EOF
+  > open Foo
+  > let init_sut = make 42
+  > type sut = int t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
   Error: Unsupported INIT function: the specification of the function called in
          the INIT expression does not provide a translatable specification for
          the following field of the model: value.

From 9382c7f4bd7f89645ae9ca7baa835516dd4e0e78 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 27 Mar 2024 17:41:32 +0100
Subject: [PATCH 12/27] Collect optional content for the `Gen` module

Inforce the constraints that the module definition should be a
structure.
---
 plugins/qcheck-stm/src/config.ml  | 35 +++++++++++++++++++++++++++----
 plugins/qcheck-stm/src/reserr.ml  | 12 +++++++----
 plugins/qcheck-stm/src/reserr.mli |  1 +
 3 files changed, 40 insertions(+), 8 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index ffde446a..059ed129 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -5,15 +5,22 @@ open Ppxlib
 type config_under_construction = {
   sut_core_type' : Ppxlib.core_type option;
   init_sut' : Ppxlib.expression option;
+  gen_mod' : Ppxlib.structure option;
 }
 
-let config_under_construction = { sut_core_type' = None; init_sut' = None }
+let config_under_construction =
+  {
+    sut_core_type' = None;
+    init_sut' = None;
+    gen_mod' = None;
+  }
 
 type t = {
   context : Context.t;
   sut_core_type : Ppxlib.core_type;
   init_sut : Ppxlib.expression;
   init_sut_txt : string;
+  gen_mod : Ppxlib.structure option; (* Containing custom QCheck generators *)
 }
 
 let mk_config context cfg_uc =
@@ -27,8 +34,9 @@ let mk_config context cfg_uc =
       ~default:(Incomplete_configuration_module `Init_sut, Location.none)
       cfg_uc.init_sut'
   in
-  let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut in
-  ok { context; sut_core_type; init_sut; init_sut_txt }
+  let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut
+  and gen_mod = cfg_uc.gen_mod' in
+  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod }
 
 let get_sut_type_name config =
   let open Ppxlib in
@@ -116,6 +124,25 @@ let type_declarations cfg_uc =
   in
   fold_left aux cfg_uc
 
+(* Inspect module definition in config module in order to collect information
+   about:
+     - the custom [QCheck] generators *)
+let module_binding cfg_uc (mb : Ppxlib.module_binding) =
+  let open Reserr in
+  match mb.pmb_name.txt with
+  | Some name when String.equal "Gen" name ->
+      let* content =
+        match mb.pmb_expr.pmod_desc with
+        | Pmod_structure structure
+        (* there is no need to go further, module constraints of module
+           constraints doesn't make sense *)
+        | Pmod_constraint ({ pmod_desc = Pmod_structure structure; _ }, _) ->
+            ok structure
+        | _ -> error (Not_a_structure name, Location.none)
+      in
+      ok { cfg_uc with gen_mod' = Some content }
+  | _ -> ok cfg_uc
+
 let scan_config cfg_uc config_mod =
   let open Reserr in
   let* ic =
@@ -145,7 +172,7 @@ let scan_config cfg_uc config_mod =
     | Pstr_type (_, xs) -> type_declarations cfg_uc xs
     | Pstr_typext _ -> ok cfg_uc
     | Pstr_exception _ -> ok cfg_uc
-    | Pstr_module _ -> ok cfg_uc
+    | Pstr_module mb -> module_binding cfg_uc mb
     | Pstr_recmodule _ -> ok cfg_uc
     | Pstr_modtype _ -> ok cfg_uc
     | Pstr_open _ -> ok cfg_uc
diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index 1de434ac..d8bd0182 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -29,6 +29,7 @@ type W.kind +=
   | No_spec of string
   | No_sut_argument of string
   | No_sut_type of string
+  | Not_a_structure of string
   | Returned_tuple of string
   | Returning_sut of string
   | Sut_type_not_specified of string
@@ -49,10 +50,10 @@ let level kind =
       W.Warning
   | Impossible_init_state_generation _ | Incompatible_sut _
   | Incomplete_configuration_module _ | No_configuration_file _
-  | No_init_function _ | No_models _ | No_sut_type _ | Sut_type_not_specified _
-  | Sut_type_not_supported _ | Syntax_error_in_config_module _
-  | Type_not_supported_for_sut_parameter _ | Type_parameter_not_instantiated _
-    ->
+  | No_init_function _ | No_models _ | No_sut_type _ | Not_a_structure _
+  | Sut_type_not_specified _ | Sut_type_not_supported _
+  | Syntax_error_in_config_module _ | Type_not_supported_for_sut_parameter _
+  | Type_parameter_not_instantiated _ ->
       W.Error
   | _ -> W.level kind
 
@@ -183,6 +184,9 @@ let pp_kind ppf kind =
       pf ppf "Missing specification for the SUT type %s" ty
   | No_configuration_file file -> pf ppf "Missing configuration file %s" file
   | No_models ty -> pf ppf "Missing model(s) for the SUT type %s" ty
+  | Not_a_structure mod_name ->
+      pf ppf "Unsupported %s module definition:@ %a" mod_name text
+        "only structures are allowed as module definition here"
   | Impossible_init_state_generation (Not_a_function_call fct) ->
       pf ppf "Unsupported INIT expression %s:@ %a" fct text
         "the INIT expression is expected to be a function call (the \
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index 708d074a..de57e59f 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -29,6 +29,7 @@ type W.kind +=
   | No_spec of string
   | No_sut_argument of string
   | No_sut_type of string
+  | Not_a_structure of string
   | Returned_tuple of string
   | Returning_sut of string
   | Sut_type_not_specified of string

From 88049650087802b35f04ef27973cb42ba26cd3aa Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 27 Mar 2024 17:44:16 +0100
Subject: [PATCH 13/27] Integrate generators into the generated code

---
 plugins/qcheck-stm/src/stm_of_ir.ml | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 064beeba..722204c7 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -932,12 +932,29 @@ let agree_prop =
       check_init_state ();
       STMTests.agree_prop cs]
 
+let qcheck config =
+  match config.Cfg.gen_mod with
+  | None -> []
+  | Some structure ->
+      let open Ast_helper in
+      let name = noloc (Some "Gen")
+      and expr =
+        pmod_structure
+          ((lident "Gen" |> Mod.ident |> Incl.mk |> pstr_include) :: structure)
+      in
+      let structure = [ pstr_module (module_binding ~name ~expr) ] in
+      let expr =
+        pmod_structure
+          ((lident "QCheck" |> Mod.ident |> Incl.mk |> pstr_include)
+          :: structure)
+      in
+      [ pstr_module (module_binding ~name:(noloc (Some "QCheck")) ~expr) ]
+
 let stm config ir =
   let open Reserr in
   let* ghost_types = ghost_types config ir.ghost_types in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
   let warn = [%stri [@@@ocaml.warning "-26-27"]] in
-  let incl = [] in
   let sut = sut_type config in
   let cmd = cmd_type ir in
   let* cmd_show = cmd_show config ir in
@@ -962,7 +979,7 @@ let stm config ir =
   let open_mod m = pstr_open Ast_helper.(Opn.mk (Mod.ident (lident m))) in
   let spec_expr =
     pmod_structure
-      ((open_mod "STM" :: incl)
+      ((open_mod "STM" :: qcheck config)
       @ [
           sut;
           cmd;

From 802cba57b467ccf25b9982a1b1ede547ea15c28e Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Wed, 27 Mar 2024 17:53:09 +0100
Subject: [PATCH 14/27] Add tests for inclusion of the custom generators

---
 plugins/qcheck-stm/test/array_config.ml       |   4 +
 .../test/array_stm_tests.expected.ml          |   6 +
 plugins/qcheck-stm/test/custom_config.ml      |   3 +
 plugins/qcheck-stm/test/custom_config.mli     |  11 ++
 .../qcheck-stm/test/custom_config_config.ml   |   5 +
 .../test/custom_config_errors.expected        |   0
 .../test/custom_config_stm_tests.expected.ml  | 106 ++++++++++++++++++
 plugins/qcheck-stm/test/dune.inc              |  92 +++++++++++++++
 plugins/qcheck-stm/test/dune_gen.args         |   2 +
 plugins/qcheck-stm/test/test_errors.t         |  18 +++
 10 files changed, 247 insertions(+)
 create mode 100644 plugins/qcheck-stm/test/custom_config.ml
 create mode 100644 plugins/qcheck-stm/test/custom_config.mli
 create mode 100644 plugins/qcheck-stm/test/custom_config_config.ml
 create mode 100644 plugins/qcheck-stm/test/custom_config_errors.expected
 create mode 100644 plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml

diff --git a/plugins/qcheck-stm/test/array_config.ml b/plugins/qcheck-stm/test/array_config.ml
index 47c880b1..b67f6826 100644
--- a/plugins/qcheck-stm/test/array_config.ml
+++ b/plugins/qcheck-stm/test/array_config.ml
@@ -3,3 +3,7 @@ open Array
 let init_sut = make 16 'a'
 
 type sut = char t
+
+module Gen = struct
+  let int = small_signed_int
+end
diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
index 2be1f672..4a9fe1e5 100644
--- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -6,6 +6,12 @@ module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =
   struct
     open STM
+    module QCheck =
+      struct
+        include QCheck
+        module Gen = struct include Gen
+                            let int = small_signed_int end
+      end
     type sut = char t
     type cmd =
       | Length 
diff --git a/plugins/qcheck-stm/test/custom_config.ml b/plugins/qcheck-stm/test/custom_config.ml
new file mode 100644
index 00000000..0aab01b6
--- /dev/null
+++ b/plugins/qcheck-stm/test/custom_config.ml
@@ -0,0 +1,3 @@
+type 'a t = 'a list ref
+let empty () = ref []
+let push t a = t := a :: !t
diff --git a/plugins/qcheck-stm/test/custom_config.mli b/plugins/qcheck-stm/test/custom_config.mli
new file mode 100644
index 00000000..18883c68
--- /dev/null
+++ b/plugins/qcheck-stm/test/custom_config.mli
@@ -0,0 +1,11 @@
+type 'a t
+(*@ mutable model contents : 'a sequence *)
+
+val empty : unit -> 'a t
+(*@ t = empty ()
+    ensures t.contents = Sequence.empty *)
+
+val push : 'a t -> 'a -> unit
+(*@ push t a
+    modifies t.contents
+    ensures t.contents = Sequence.cons a (old t.contents) *)
diff --git a/plugins/qcheck-stm/test/custom_config_config.ml b/plugins/qcheck-stm/test/custom_config_config.ml
new file mode 100644
index 00000000..9ac539ae
--- /dev/null
+++ b/plugins/qcheck-stm/test/custom_config_config.ml
@@ -0,0 +1,5 @@
+type sut = int t
+let init_sut = empty ()
+module Gen = struct
+  let int = small_signed_int
+end
diff --git a/plugins/qcheck-stm/test/custom_config_errors.expected b/plugins/qcheck-stm/test/custom_config_errors.expected
new file mode 100644
index 00000000..e69de29b
diff --git a/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
new file mode 100644
index 00000000..462661b4
--- /dev/null
+++ b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
@@ -0,0 +1,106 @@
+(* This file is generated by ortac qcheck-stm,
+   edit how you run the tool instead *)
+[@@@ocaml.warning "-26-27"]
+open Custom_config
+module Ortac_runtime = Ortac_runtime_qcheck_stm
+module Spec =
+  struct
+    open STM
+    module QCheck =
+      struct
+        include QCheck
+        module Gen = struct include Gen
+                            let int = small_signed_int end
+      end
+    type sut = int t
+    type cmd =
+      | Push of int 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Push a_1 ->
+          Format.asprintf "%s sut %a" "push" (Util.Pp.pp_int true) a_1
+    type nonrec state = {
+      contents: int Ortac_runtime.Gospelstdlib.sequence }
+    let init_state =
+      let () = () in
+      {
+        contents =
+          (try Ortac_runtime.Gospelstdlib.Sequence.empty
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "custom_config.mli";
+                            pos_lnum = 6;
+                            pos_bol = 257;
+                            pos_cnum = 282
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "custom_config.mli";
+                            pos_lnum = 6;
+                            pos_bol = 257;
+                            pos_cnum = 296
+                          }
+                      })))
+      }
+    let init_sut () = empty ()
+    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
+                  Ortac_runtime.Gospelstdlib.Sequence.cons a_1
+                    state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "custom_config.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 469;
+                                 pos_cnum = 494
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "custom_config.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 469;
+                                 pos_cnum = 526
+                               }
+                           }))))
+          }
+    let precond cmd__008_ state__009_ =
+      match cmd__008_ with | Push a_1 -> true
+    let postcond _ _ _ = true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with | Push a_1 -> Res (unit, (push sut__011_ a_1))
+  end
+module STMTests = (Ortac_runtime.Make)(Spec)
+let check_init_state () = ()
+let ortac_postcond cmd__004_ state__005_ res__006_ =
+  let open Spec in
+    let open STM in
+      let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
+      match (cmd__004_, res__006_) with
+      | (Push a_1, Res ((Unit, _), _)) -> None
+      | _ -> None
+let _ =
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Custom_config STM tests"
+        check_init_state ortac_postcond])
diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc
index 2bb22c0d..2edab4c2 100644
--- a/plugins/qcheck-stm/test/dune.inc
+++ b/plugins/qcheck-stm/test/dune.inc
@@ -373,6 +373,26 @@
  (name integer_in_model)
  (modules integer_in_model))
 
+(rule
+ (target integer_in_model_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
+    integer_in_model_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:integer_in_model.mli}
+     %{dep:integer_in_model_config.ml}
+     -o
+     %{target})))))
+
 (test
  (name integer_in_model_stm_tests)
  (package ortac-qcheck-stm)
@@ -406,6 +426,25 @@
  (name ghost_as_model)
  (modules ghost_as_model))
 
+(rule
+ (target ghost_as_model_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
+    ghost_as_model_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:ghost_as_model.mli}
+     %{dep:ghost_as_model_config.ml}
+     -o
+     %{target})))))
 
 (test
  (name ghost_as_model_stm_tests)
@@ -436,3 +475,56 @@
  (action
   (run %{dep:ghost_as_model_stm_tests.exe} -v)))
 
+(library
+ (name custom_config)
+ (modules custom_config))
+
+(rule
+ (target custom_config_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
+    custom_config_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:custom_config.mli}
+     %{dep:custom_config_config.ml}
+     -o
+     %{target})))))
+
+(test
+ (name custom_config_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules custom_config_stm_tests)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime-qcheck-stm
+  custom_config)
+ (action
+  (echo
+   "\n%{dep:custom_config_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff custom_config_errors.expected custom_config_errors)
+   (diff custom_config_stm_tests.expected.ml custom_config_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:custom_config_stm_tests.exe} -v)))
+
diff --git a/plugins/qcheck-stm/test/dune_gen.args b/plugins/qcheck-stm/test/dune_gen.args
index d075fc50..cb8685d2 100644
--- a/plugins/qcheck-stm/test/dune_gen.args
+++ b/plugins/qcheck-stm/test/dune_gen.args
@@ -16,3 +16,5 @@ integer_in_model
 integer_in_model_config
 ghost_as_model
 ghost_as_model_config
+custom_config
+custom_config_config
diff --git a/plugins/qcheck-stm/test/test_errors.t b/plugins/qcheck-stm/test/test_errors.t
index dacdc11d..928aeb98 100644
--- a/plugins/qcheck-stm/test/test_errors.t
+++ b/plugins/qcheck-stm/test/test_errors.t
@@ -255,3 +255,21 @@ We shouldn't be able to define a model by itsef in the `make` function:
                             ^
   Warning: Skipping clause: impossible to define the initial value of the model
            with a recursive expression.
+
+If we add some custom generators, we should do so in a `Gen` module that is implemented (functor application or reference to another module are not supported):
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > val make : 'a -> 'a t
+  > (*@ t = make a
+  >     ensures t.value = a *)
+  > EOF
+  $ cat > foo_config.ml << EOF
+  > module Gen = QCheck.Gen
+  > open Foo
+  > let init_sut = make 42
+  > type sut = int t
+  > EOF
+  $ ortac qcheck-stm foo.mli foo_config.ml
+  Error: Unsupported Gen module definition: only structures are allowed as
+         module definition here.

From 165501f0a3bbe4cf9f21fa13714d0c7ee28a8a98 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 10:20:19 +0100
Subject: [PATCH 15/27] Collect optional content for `Pp` module

---
 plugins/qcheck-stm/src/config.ml | 33 ++++++++++++++++++++------------
 1 file changed, 21 insertions(+), 12 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index 059ed129..d636c7a5 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -6,6 +6,7 @@ type config_under_construction = {
   sut_core_type' : Ppxlib.core_type option;
   init_sut' : Ppxlib.expression option;
   gen_mod' : Ppxlib.structure option;
+  pp_mod' : Ppxlib.structure option;
 }
 
 let config_under_construction =
@@ -13,6 +14,7 @@ let config_under_construction =
     sut_core_type' = None;
     init_sut' = None;
     gen_mod' = None;
+    pp_mod' = None;
   }
 
 type t = {
@@ -21,6 +23,7 @@ type t = {
   init_sut : Ppxlib.expression;
   init_sut_txt : string;
   gen_mod : Ppxlib.structure option; (* Containing custom QCheck generators *)
+  pp_mod : Ppxlib.structure option; (* Containing custom pretty printers *)
 }
 
 let mk_config context cfg_uc =
@@ -35,8 +38,9 @@ let mk_config context cfg_uc =
       cfg_uc.init_sut'
   in
   let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut
-  and gen_mod = cfg_uc.gen_mod' in
-  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod }
+  and gen_mod = cfg_uc.gen_mod'
+  and pp_mod = cfg_uc.pp_mod' in
+  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod; pp_mod }
 
 let get_sut_type_name config =
   let open Ppxlib in
@@ -126,21 +130,26 @@ let type_declarations cfg_uc =
 
 (* Inspect module definition in config module in order to collect information
    about:
-     - the custom [QCheck] generators *)
+     - the custom [QCheck] generators
+     - the custom [STM] pretty printers *)
 let module_binding cfg_uc (mb : Ppxlib.module_binding) =
   let open Reserr in
+  let get_structure name mb =
+    match mb.pmb_expr.pmod_desc with
+    | Pmod_structure structure
+    (* there is no need to go further, module constraints of module
+       constraints doesn't make sense *)
+    | Pmod_constraint ({ pmod_desc = Pmod_structure structure; _ }, _) ->
+        ok structure
+    | _ -> error (Not_a_structure name, Location.none)
+  in
   match mb.pmb_name.txt with
   | Some name when String.equal "Gen" name ->
-      let* content =
-        match mb.pmb_expr.pmod_desc with
-        | Pmod_structure structure
-        (* there is no need to go further, module constraints of module
-           constraints doesn't make sense *)
-        | Pmod_constraint ({ pmod_desc = Pmod_structure structure; _ }, _) ->
-            ok structure
-        | _ -> error (Not_a_structure name, Location.none)
-      in
+      let* content = get_structure name mb in
       ok { cfg_uc with gen_mod' = Some content }
+  | Some name when String.equal "Pp" name ->
+      let* content = get_structure name mb in
+      ok { cfg_uc with pp_mod' = Some content }
   | _ -> ok cfg_uc
 
 let scan_config cfg_uc config_mod =

From 48924d6d7dcfea2ab94fff1495508d65d9ae1d4d Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 10:55:33 +0100
Subject: [PATCH 16/27] Integrate pretty printers into generated code

Some refactoring as the shape of the generated code is very similar to
the one for generators
---
 plugins/qcheck-stm/src/stm_of_ir.ml | 36 ++++++++++++++++++++---------
 1 file changed, 25 insertions(+), 11 deletions(-)

diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 722204c7..161ca3a8 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -932,23 +932,36 @@ let agree_prop =
       check_init_state ();
       STMTests.agree_prop cs]
 
+let prepend_include_in_module name lident structure =
+  let open Ast_helper in
+  let name = noloc (Some name)
+  and expr =
+    pmod_structure
+    @@ ((Mod.ident lident |> Incl.mk |> pstr_include) :: structure)
+  in
+  [ pstr_module @@ module_binding ~name ~expr ]
+
 let qcheck config =
   match config.Cfg.gen_mod with
   | None -> []
   | Some structure ->
-      let open Ast_helper in
-      let name = noloc (Some "Gen")
-      and expr =
-        pmod_structure
-          ((lident "Gen" |> Mod.ident |> Incl.mk |> pstr_include) :: structure)
+      let structure =
+        prepend_include_in_module "Gen" (lident "Gen") structure
       in
-      let structure = [ pstr_module (module_binding ~name ~expr) ] in
-      let expr =
-        pmod_structure
-          ((lident "QCheck" |> Mod.ident |> Incl.mk |> pstr_include)
-          :: structure)
+      prepend_include_in_module "QCheck" (lident "QCheck") structure
+
+let util config =
+  match config.Cfg.pp_mod with
+  | None -> []
+  | Some structure ->
+      let structure =
+        prepend_include_in_module "Pp"
+          (noloc (Ldot (Lident "Util", "Pp")))
+          structure
       in
-      [ pstr_module (module_binding ~name:(noloc (Some "QCheck")) ~expr) ]
+      (* We don't need the whole `Util` module here *)
+      let name = noloc (Some "Util") and expr = pmod_structure structure in
+      [ pstr_module (module_binding ~name ~expr) ]
 
 let stm config ir =
   let open Reserr in
@@ -980,6 +993,7 @@ let stm config ir =
   let spec_expr =
     pmod_structure
       ((open_mod "STM" :: qcheck config)
+      @ util config
       @ [
           sut;
           cmd;

From 3a1a17e6d331a0f7785e7414604c50d832bc579e Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 10:56:32 +0100
Subject: [PATCH 17/27] Add tests for inclusion of custom pretty printers

---
 plugins/qcheck-stm/test/custom_config_config.ml           | 3 +++
 .../qcheck-stm/test/custom_config_stm_tests.expected.ml   | 8 ++++++++
 2 files changed, 11 insertions(+)

diff --git a/plugins/qcheck-stm/test/custom_config_config.ml b/plugins/qcheck-stm/test/custom_config_config.ml
index 9ac539ae..f625614a 100644
--- a/plugins/qcheck-stm/test/custom_config_config.ml
+++ b/plugins/qcheck-stm/test/custom_config_config.ml
@@ -3,3 +3,6 @@ let init_sut = empty ()
 module Gen = struct
   let int = small_signed_int
 end
+module Pp = struct
+  let _pp_wont_be_used = of_show (fun _ -> "dummy") false
+end
diff --git a/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
index 462661b4..d250e343 100644
--- a/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
@@ -12,6 +12,14 @@ module Spec =
         module Gen = struct include Gen
                             let int = small_signed_int end
       end
+    module Util =
+      struct
+        module Pp =
+          struct
+            include Util.Pp
+            let _pp_wont_be_used = of_show (fun _ -> "dummy") false
+          end
+      end
     type sut = int t
     type cmd =
       | Push of int 

From c5e9c48eac8495adb07e03a4042c198ea1d5d863 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 11:19:45 +0100
Subject: [PATCH 18/27] Collect optional ty extensions and functional
 constructors

---
 plugins/qcheck-stm/src/config.ml    | 14 +++++++++++---
 plugins/qcheck-stm/src/stm_of_ir.ml |  1 +
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml
index d636c7a5..79b74500 100644
--- a/plugins/qcheck-stm/src/config.ml
+++ b/plugins/qcheck-stm/src/config.ml
@@ -7,6 +7,7 @@ type config_under_construction = {
   init_sut' : Ppxlib.expression option;
   gen_mod' : Ppxlib.structure option;
   pp_mod' : Ppxlib.structure option;
+  ty_mod' : Ppxlib.structure option;
 }
 
 let config_under_construction =
@@ -15,6 +16,7 @@ let config_under_construction =
     init_sut' = None;
     gen_mod' = None;
     pp_mod' = None;
+    ty_mod' = None;
   }
 
 type t = {
@@ -24,6 +26,7 @@ type t = {
   init_sut_txt : string;
   gen_mod : Ppxlib.structure option; (* Containing custom QCheck generators *)
   pp_mod : Ppxlib.structure option; (* Containing custom pretty printers *)
+  ty_mod : Ppxlib.structure option; (* Containing custom STM.ty extensions *)
 }
 
 let mk_config context cfg_uc =
@@ -39,8 +42,9 @@ let mk_config context cfg_uc =
   in
   let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut
   and gen_mod = cfg_uc.gen_mod'
-  and pp_mod = cfg_uc.pp_mod' in
-  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod; pp_mod }
+  and pp_mod = cfg_uc.pp_mod'
+  and ty_mod = cfg_uc.ty_mod' in
+  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod; pp_mod; ty_mod }
 
 let get_sut_type_name config =
   let open Ppxlib in
@@ -131,7 +135,8 @@ let type_declarations cfg_uc =
 (* Inspect module definition in config module in order to collect information
    about:
      - the custom [QCheck] generators
-     - the custom [STM] pretty printers *)
+     - the custom [STM] pretty printers
+     - the custom [STM.ty] extensions and function constructors *)
 let module_binding cfg_uc (mb : Ppxlib.module_binding) =
   let open Reserr in
   let get_structure name mb =
@@ -150,6 +155,9 @@ let module_binding cfg_uc (mb : Ppxlib.module_binding) =
   | Some name when String.equal "Pp" name ->
       let* content = get_structure name mb in
       ok { cfg_uc with pp_mod' = Some content }
+  | Some name when String.equal "Ty" name ->
+      let* content = get_structure name mb in
+      ok { cfg_uc with ty_mod' = Some content }
   | _ -> ok cfg_uc
 
 let scan_config cfg_uc config_mod =
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 161ca3a8..6478eaa6 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -994,6 +994,7 @@ let stm config ir =
     pmod_structure
       ((open_mod "STM" :: qcheck config)
       @ util config
+      @ Option.value config.ty_mod ~default:[]
       @ [
           sut;
           cmd;

From 30afd2587cd1e11b58a209583a42567aeac2fb0b Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 14:47:05 +0100
Subject: [PATCH 19/27] Add tests for inclusion of `ty` extensions

---
 plugins/qcheck-stm/test/custom_config.ml      |  11 +-
 plugins/qcheck-stm/test/custom_config.mli     |  17 +-
 .../qcheck-stm/test/custom_config_config.ml   |  16 +-
 .../test/custom_config_errors.expected        |  18 ++
 .../test/custom_config_stm_tests.expected.ml  | 222 ++++++++++++++++--
 5 files changed, 254 insertions(+), 30 deletions(-)

diff --git a/plugins/qcheck-stm/test/custom_config.ml b/plugins/qcheck-stm/test/custom_config.ml
index 0aab01b6..2ebc066f 100644
--- a/plugins/qcheck-stm/test/custom_config.ml
+++ b/plugins/qcheck-stm/test/custom_config.ml
@@ -1,3 +1,10 @@
-type 'a t = 'a list ref
+type 'a elt = Elt of 'a
+
+let elt a = Elt a
+
+type 'a t = 'a elt list ref
+
+let proj = function Elt a -> a
 let empty () = ref []
-let push t a = t := a :: !t
+let push t e = t := e :: !t
+let top t = match !t with [] -> invalid_arg "top" | x :: _ -> x
diff --git a/plugins/qcheck-stm/test/custom_config.mli b/plugins/qcheck-stm/test/custom_config.mli
index 18883c68..9a5942e7 100644
--- a/plugins/qcheck-stm/test/custom_config.mli
+++ b/plugins/qcheck-stm/test/custom_config.mli
@@ -1,11 +1,22 @@
 type 'a t
 (*@ mutable model contents : 'a sequence *)
 
+type 'a elt = private Elt of 'a
+
+val elt : 'a -> 'a elt
+val proj : 'a elt -> 'a
+(*@ pure *)
+
 val empty : unit -> 'a t
 (*@ t = empty ()
     ensures t.contents = Sequence.empty *)
 
-val push : 'a t -> 'a -> unit
-(*@ push t a
+val push : 'a t -> 'a elt -> unit
+(*@ push t e
     modifies t.contents
-    ensures t.contents = Sequence.cons a (old t.contents) *)
+    ensures t.contents = Sequence.cons (proj e) (old t.contents) *)
+
+val top : 'a t -> 'a elt
+(*@ a = top t
+    checks t.contents <> Sequence.empty
+    ensures proj a = Sequence.hd t.contents *)
diff --git a/plugins/qcheck-stm/test/custom_config_config.ml b/plugins/qcheck-stm/test/custom_config_config.ml
index f625614a..1ee37ef0 100644
--- a/plugins/qcheck-stm/test/custom_config_config.ml
+++ b/plugins/qcheck-stm/test/custom_config_config.ml
@@ -1,8 +1,22 @@
 type sut = int t
+
 let init_sut = empty ()
+
 module Gen = struct
   let int = small_signed_int
+  let elt gen = elt <$> gen
 end
+
 module Pp = struct
-  let _pp_wont_be_used = of_show (fun _ -> "dummy") false
+  let pp_elt pp par fmt e =
+    let open Format in
+    fprintf fmt "(Elt %a)" (pp par) (proj e)
+end
+
+module Ty = struct
+  type _ ty += Elt : 'a ty -> 'a elt ty
+
+  let elt spec =
+    let ty, show = spec in
+    (Elt ty, fun x -> Printf.sprintf "Elt %s" (show (proj x)))
 end
diff --git a/plugins/qcheck-stm/test/custom_config_errors.expected b/plugins/qcheck-stm/test/custom_config_errors.expected
index e69de29b..4f363f45 100644
--- a/plugins/qcheck-stm/test/custom_config_errors.expected
+++ b/plugins/qcheck-stm/test/custom_config_errors.expected
@@ -0,0 +1,18 @@
+File "custom_config.mli", line 6, characters 10-22:
+6 | val elt : 'a -> 'a elt
+              ^^^^^^^^^^^^
+Warning: Skipping elt: functions with no SUT argument cannot be tested.
+File "custom_config.mli", line 6, characters 0-22:
+6 | val elt : 'a -> 'a elt
+    ^^^^^^^^^^^^^^^^^^^^^^
+Warning: Skipping elt: functions without specifications cannot be tested.
+File "custom_config.mli", line 7, characters 11-23:
+7 | val proj : 'a elt -> 'a
+               ^^^^^^^^^^^^
+Warning: Skipping proj: functions with no SUT argument cannot be tested.
+File "custom_config.mli", line 19, characters 0-125:
+19 | val top : 'a t -> 'a elt
+20 | (*@ a = top t
+21 |     checks t.contents <> Sequence.empty
+22 |     ensures proj a = Sequence.hd t.contents *)
+Warning: Incomplete computation of the returned value in the specification of top. Failure message won't be able to display the expected returned value.
diff --git a/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
index d250e343..e3febc26 100644
--- a/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
+++ b/plugins/qcheck-stm/test/custom_config_stm_tests.expected.ml
@@ -9,24 +9,37 @@ module Spec =
     module QCheck =
       struct
         include QCheck
-        module Gen = struct include Gen
-                            let int = small_signed_int end
+        module Gen =
+          struct
+            include Gen
+            let int = small_signed_int
+            let elt gen = elt <$> gen
+          end
       end
     module Util =
       struct
         module Pp =
           struct
             include Util.Pp
-            let _pp_wont_be_used = of_show (fun _ -> "dummy") false
+            let pp_elt pp par fmt e =
+              let open Format in fprintf fmt "(Elt %a)" (pp par) (proj e)
           end
       end
+    type _ ty +=  
+      | Elt: 'a ty -> 'a elt ty 
+    let elt spec =
+      let (ty, show) = spec in
+      ((Elt ty), (fun x -> Printf.sprintf "Elt %s" (show (proj x))))
     type sut = int t
     type cmd =
-      | Push of int 
+      | Push of int elt 
+      | Top 
     let show_cmd cmd__001_ =
       match cmd__001_ with
-      | Push a_1 ->
-          Format.asprintf "%s sut %a" "push" (Util.Pp.pp_int true) a_1
+      | Push e ->
+          Format.asprintf "%s sut %a" "push"
+            (Util.Pp.pp_elt Util.Pp.pp_int true) e
+      | Top -> Format.asprintf "protect (fun () -> %s sut)" "top"
     type nonrec state = {
       contents: int Ortac_runtime.Gospelstdlib.sequence }
     let init_state =
@@ -43,16 +56,16 @@ module Spec =
                         Ortac_runtime.start =
                           {
                             pos_fname = "custom_config.mli";
-                            pos_lnum = 6;
-                            pos_bol = 257;
-                            pos_cnum = 282
+                            pos_lnum = 12;
+                            pos_bol = 421;
+                            pos_cnum = 446
                           };
                         Ortac_runtime.stop =
                           {
                             pos_fname = "custom_config.mli";
-                            pos_lnum = 6;
-                            pos_bol = 257;
-                            pos_cnum = 296
+                            pos_lnum = 12;
+                            pos_bol = 421;
+                            pos_cnum = 460
                           }
                       })))
       }
@@ -61,14 +74,15 @@ module Spec =
     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 open Gen in
+             oneof [(pure (fun e -> Push e)) <*> (elt int); pure Top])
     let next_state cmd__002_ state__003_ =
       match cmd__002_ with
-      | Push a_1 ->
+      | Push e ->
           {
             contents =
               ((try
-                  Ortac_runtime.Gospelstdlib.Sequence.cons a_1
+                  Ortac_runtime.Gospelstdlib.Sequence.cons (proj e)
                     state__003_.contents
                 with
                 | e ->
@@ -79,24 +93,29 @@ module Spec =
                              Ortac_runtime.start =
                                {
                                  pos_fname = "custom_config.mli";
-                                 pos_lnum = 11;
-                                 pos_bol = 469;
-                                 pos_cnum = 494
+                                 pos_lnum = 17;
+                                 pos_bol = 639;
+                                 pos_cnum = 664
                                };
                              Ortac_runtime.stop =
                                {
                                  pos_fname = "custom_config.mli";
-                                 pos_lnum = 11;
-                                 pos_bol = 469;
-                                 pos_cnum = 526
+                                 pos_lnum = 17;
+                                 pos_bol = 639;
+                                 pos_cnum = 703
                                }
                            }))))
           }
+      | Top -> state__003_
     let precond cmd__008_ state__009_ =
-      match cmd__008_ with | Push a_1 -> true
+      match cmd__008_ with | Push e -> true | Top -> true
     let postcond _ _ _ = true
     let run cmd__010_ sut__011_ =
-      match cmd__010_ with | Push a_1 -> Res (unit, (push sut__011_ a_1))
+      match cmd__010_ with
+      | Push e -> Res (unit, (push sut__011_ e))
+      | Top ->
+          Res
+            ((result (elt int) exn), (protect (fun () -> top sut__011_) ()))
   end
 module STMTests = (Ortac_runtime.Make)(Spec)
 let check_init_state () = ()
@@ -105,7 +124,162 @@ let ortac_postcond cmd__004_ state__005_ res__006_ =
     let open STM in
       let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
       match (cmd__004_, res__006_) with
-      | (Push a_1, Res ((Unit, _), _)) -> None
+      | (Push e, Res ((Unit, _), _)) -> None
+      | (Top, Res ((Result (Elt (Int), Exn), _), a_1)) ->
+          (match if
+                   try
+                     not
+                       (state__005_.contents =
+                          Ortac_runtime.Gospelstdlib.Sequence.empty)
+                   with
+                   | e ->
+                       raise
+                         (Ortac_runtime.Partial_function
+                            (e,
+                              {
+                                Ortac_runtime.start =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 21;
+                                    pos_bol = 875;
+                                    pos_cnum = 886
+                                  };
+                                Ortac_runtime.stop =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 21;
+                                    pos_bol = 875;
+                                    pos_cnum = 914
+                                  }
+                              }))
+                 then None
+                 else
+                   Some
+                     (Ortac_runtime.report "Custom_config" "empty ()"
+                        (Either.left "Invalid_argument") "top"
+                        [("t.contents <> Sequence.empty",
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "custom_config.mli";
+                                 pos_lnum = 21;
+                                 pos_bol = 875;
+                                 pos_cnum = 886
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "custom_config.mli";
+                                 pos_lnum = 21;
+                                 pos_bol = 875;
+                                 pos_cnum = 914
+                               }
+                           })])
+           with
+           | None ->
+               (match a_1 with
+                | Ok a_1 ->
+                    if
+                      (try
+                         (proj a_1) =
+                           (Ortac_runtime.Gospelstdlib.Sequence.hd
+                              (Lazy.force new_state__007_).contents)
+                       with
+                       | e ->
+                           raise
+                             (Ortac_runtime.Partial_function
+                                (e,
+                                  {
+                                    Ortac_runtime.start =
+                                      {
+                                        pos_fname = "custom_config.mli";
+                                        pos_lnum = 22;
+                                        pos_bol = 915;
+                                        pos_cnum = 927
+                                      };
+                                    Ortac_runtime.stop =
+                                      {
+                                        pos_fname = "custom_config.mli";
+                                        pos_lnum = 22;
+                                        pos_bol = 915;
+                                        pos_cnum = 958
+                                      }
+                                  })))
+                    then None
+                    else
+                      Some
+                        (Ortac_runtime.report "Custom_config" "empty ()"
+                           (Either.right (Res (Ortac_runtime.dummy, ())))
+                           "top"
+                           [("proj a = Sequence.hd t.contents",
+                              {
+                                Ortac_runtime.start =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 22;
+                                    pos_bol = 915;
+                                    pos_cnum = 927
+                                  };
+                                Ortac_runtime.stop =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 22;
+                                    pos_bol = 915;
+                                    pos_cnum = 958
+                                  }
+                              })])
+                | _ -> None)
+           | _ ->
+               (match a_1 with
+                | Error (Invalid_argument _) -> None
+                | _ ->
+                    if
+                      (try
+                         not
+                           (state__005_.contents =
+                              Ortac_runtime.Gospelstdlib.Sequence.empty)
+                       with
+                       | e ->
+                           raise
+                             (Ortac_runtime.Partial_function
+                                (e,
+                                  {
+                                    Ortac_runtime.start =
+                                      {
+                                        pos_fname = "custom_config.mli";
+                                        pos_lnum = 21;
+                                        pos_bol = 875;
+                                        pos_cnum = 886
+                                      };
+                                    Ortac_runtime.stop =
+                                      {
+                                        pos_fname = "custom_config.mli";
+                                        pos_lnum = 21;
+                                        pos_bol = 875;
+                                        pos_cnum = 914
+                                      }
+                                  })))
+                    then None
+                    else
+                      Some
+                        (Ortac_runtime.report "Custom_config" "empty ()"
+                           (Either.left "Invalid_argument") "top"
+                           [("t.contents <> Sequence.empty",
+                              {
+                                Ortac_runtime.start =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 21;
+                                    pos_bol = 875;
+                                    pos_cnum = 886
+                                  };
+                                Ortac_runtime.stop =
+                                  {
+                                    pos_fname = "custom_config.mli";
+                                    pos_lnum = 21;
+                                    pos_bol = 875;
+                                    pos_cnum = 914
+                                  }
+                              })])))
       | _ -> None
 let _ =
   QCheck_base_runner.run_tests_main

From 6ac533a27049581382ee914cb32411e8005f1f4d Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 4 Jun 2024 11:28:09 +0200
Subject: [PATCH 20/27] Reorder `pp_kind` cases in reserr

---
 plugins/qcheck-stm/src/reserr.ml | 140 +++++++++++++++----------------
 1 file changed, 70 insertions(+), 70 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index d8bd0182..3818b82b 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -100,30 +100,50 @@ let pp_kind ppf kind =
   (* Warnings *)
   | Constant_value id ->
       pf ppf "Skipping %s:@ %a" id text "constants cannot be tested"
-  | Returning_sut id ->
-      pf ppf "Skipping %s:@ %a" id text
-        "functions returning a SUT value cannot be tested"
-  | No_sut_argument id ->
-      pf ppf "Skipping %s:@ %a" id text
-        "functions with no SUT argument cannot be tested"
-  | Multiple_sut_arguments id ->
-      pf ppf "Skipping %s:@ %a" id text
-        "functions with multiple SUT arguments cannot be tested"
+  | Ensures_not_found_for_next_state (f, m) ->
+      pf ppf "Skipping %s:@ model@ %s %a@;%a%s%a" f m text
+        "is declared as modified by the function but no suitable ensures \
+         clause was found."
+        text "Specifications should contain at least one \"ensures x." m text
+        " = expr\" where x is the SUT and expr can refer to the SUT only under \
+         an old operator and can't refer to the returned value"
+  | Functional_argument f ->
+      pf ppf "Skipping %s:@ %a" f text
+        "functions are not supported yet as arguments"
+  | Ghost_values (id, k) ->
+      pf ppf "Skipping %s:@ %a%a%a" id text "functions with a ghost " text
+        (match k with `Arg -> "argument" | `Ret -> "returned value")
+        text " are not supported"
+  | Ignored_modifies ->
+      pf ppf "Skipping unsupported modifies clause:@ %a" text
+        "expected \"modifies x\" or \"modifies x.model\" where x is the SUT"
   | Incompatible_type (v, t) ->
       pf ppf "Skipping %s:@ %a%s" v text
         "the type of its SUT-type argument is incompatible with the configured \
          SUT type: "
         t
+  | Multiple_sut_arguments id ->
+      pf ppf "Skipping %s:@ %a" id text
+        "functions with multiple SUT arguments cannot be tested"
   | No_spec fct ->
       pf ppf "Skipping %s:@ %a" fct text
         "functions without specifications cannot be tested"
+  | No_sut_argument id ->
+      pf ppf "Skipping %s:@ %a" id text
+        "functions with no SUT argument cannot be tested"
+  | Returned_tuple f ->
+      pf ppf "Skipping %s:@ %a" f text
+        "functions returning tuples are not supported yet"
+  | Returning_sut id ->
+      pf ppf "Skipping %s:@ %a" id text
+        "functions returning a SUT value cannot be tested"
   | Impossible_term_substitution why ->
       let msg =
         match why with
         | `NotModel ->
             "occurrences of the SUT in clauses are only supported to access \
              its model fields"
-        (* The  [`Never] case is used when generating [init_state] *)
+        (* The [`Never] case is used when generating [init_state] *)
         | `Never ->
             "impossible to define the initial value of the model with a \
              recursive expression"
@@ -140,62 +160,15 @@ let pp_kind ppf kind =
              next_state function"
       in
       pf ppf "Skipping clause:@ %a" text msg
-  | Ignored_modifies ->
-      pf ppf "Skipping unsupported modifies clause:@ %a" text
-        "expected \"modifies x\" or \"modifies x.model\" where x is the SUT"
-  | Ensures_not_found_for_next_state (f, m) ->
-      pf ppf "Skipping %s:@ model@ %s %a@;%a%s%a" f m text
-        "is declared as modified by the function but no suitable ensures \
-         clause was found."
-        text "Specifications should contain at least one \"ensures x." m text
-        " = expr\" where x is the SUT and expr can refer to the SUT only under \
-         an old operator and can't refer to the returned value"
-  | Functional_argument f ->
-      pf ppf "Skipping %s:@ %a" f text
-        "functions are not supported yet as arguments"
-  | Returned_tuple f ->
-      pf ppf "Skipping %s:@ %a" f text
-        "functions returning tuples are not supported yet"
-  | Ghost_values (id, k) ->
-      pf ppf "Skipping %s:@ %a%a%a" id text "functions with a ghost " text
-        (match k with `Arg -> "argument" | `Ret -> "returned value")
-        text " are not supported"
   (* This following message is broad and used in seemingly different contexts
      but in fact we support all the types that the Gospel type-checker supports,
      so that error message should never get reported to the end user *)
   | Type_not_supported ty -> pf ppf "Type %s not supported" ty
   (* Errors *)
-  | No_sut_type ty -> pf ppf "Type %s not declared in the module" ty
-  | No_init_function f -> pf ppf "Function %s not declared in the module" f
-  | Syntax_error_in_config_module s ->
-      pf ppf "Syntax error in OCaml configuration module %s" s
-  | Sut_type_not_supported ty ->
-      pf ppf "Unsupported SUT type %s:@ %a" ty text
-        "SUT type must be a type constructor, possibly applied to type \
-         arguments"
-  | Type_parameter_not_instantiated ty ->
-      pf ppf "Unsupported type parameter %s:@ %a" ty text
-        "SUT type should be fully instantiated"
-  | Type_not_supported_for_sut_parameter ty ->
-      pf ppf "Unsupported type parameter %s:@ %a" ty text
-        "only constructors and tuples are supported in arguments for the SUT \
-         type"
-  | Sut_type_not_specified ty ->
-      pf ppf "Missing specification for the SUT type %s" ty
-  | No_configuration_file file -> pf ppf "Missing configuration file %s" file
-  | No_models ty -> pf ppf "Missing model(s) for the SUT type %s" ty
-  | Not_a_structure mod_name ->
-      pf ppf "Unsupported %s module definition:@ %a" mod_name text
-        "only structures are allowed as module definition here"
-  | Impossible_init_state_generation (Not_a_function_call fct) ->
-      pf ppf "Unsupported INIT expression %s:@ %a" fct text
-        "the INIT expression is expected to be a function call (the \
-         specification of that function is required to initialize the model \
-         state)"
-  | Impossible_init_state_generation (No_specification fct) ->
-      pf ppf "Unsupported INIT function %s:@ %a" fct text
-        "the function called in the INIT expression must be specified to \
-         initialize the model state"
+  | Impossible_init_state_generation (Mismatch_number_of_arguments fct) ->
+      pf ppf "Error in INIT expression %s:@ %a" fct text
+        "mismatch in the number of arguments between the INIT expression and \
+         the function specification"
   | Impossible_init_state_generation
       (No_appropriate_specifications (fct, models)) ->
       pf ppf "Unsupported INIT function %s:@ %a:@ %a" fct text
@@ -203,12 +176,21 @@ let pp_kind ppf kind =
          not specify the following fields of the model"
         (Fmt.list ~sep:(Fmt.any ",@ ") Fmt.string)
         models
+  | Impossible_init_state_generation (No_specification fct) ->
+      pf ppf "Unsupported INIT function %s:@ %a" fct text
+        "the function called in the INIT expression must be specified to \
+         initialize the model state"
   | Impossible_init_state_generation (No_translatable_specification model) ->
       pf ppf "Unsupported INIT function:@ %a:@ %s" text
         "the specification of the function called in the INIT expression does \
          not provide a translatable specification for the following field of \
          the model"
         model
+  | Impossible_init_state_generation (Not_a_function_call fct) ->
+      pf ppf "Unsupported INIT expression %s:@ %a" fct text
+        "the INIT expression is expected to be a function call (the \
+         specification of that function is required to initialize the model \
+         state)"
   | Impossible_init_state_generation (Not_returning_sut fct) ->
       pf ppf "Unsupported INIT expression %s:@ %a" fct text
         "the function called in the INIT expression must return a value of SUT \
@@ -216,10 +198,11 @@ let pp_kind ppf kind =
   | Impossible_init_state_generation (Qualified_name fct) ->
       pf ppf "Unsupported INIT function %s:@ %a" fct text
         "qualified names are not yet supported"
-  | Impossible_init_state_generation (Mismatch_number_of_arguments fct) ->
-      pf ppf "Error in INIT expression %s:@ %a" fct text
-        "mismatch in the number of arguments between the INIT expression and \
-         the function specification"
+  | Incompatible_sut t ->
+      pf ppf "Incompatible declaration of SUT type:@ %a%s" text
+        "the declaration of the SUT type is incompatible with the configured \
+         one: "
+        t
   | Incomplete_configuration_module missing ->
       let what =
         match missing with
@@ -227,17 +210,34 @@ let pp_kind ppf kind =
         | `Sut -> "the sut type declaration"
       in
       pf ppf "Incomplete configuration module: it is missing %s" what
-  | Incompatible_sut t ->
-      pf ppf "Incompatible declaration of SUT type:@ %a%s" text
-        "the declaration of the SUT type is incompatible with the configured \
-         one: "
-        t
   | Incomplete_ret_val_computation fct ->
       pf ppf
         "Incomplete computation of the returned value in the specification of \
          %s. Failure message won't be able to display the expected returned \
          value"
         fct
+  | No_configuration_file file -> pf ppf "Missing configuration file %s" file
+  | No_init_function f -> pf ppf "Function %s not declared in the module" f
+  | No_models ty -> pf ppf "Missing model(s) for the SUT type %s" ty
+  | No_sut_type ty -> pf ppf "Type %s not declared in the module" ty
+  | Not_a_structure mod_name ->
+      pf ppf "Unsupported %s module definition:@ %a" mod_name text
+        "only structures are allowed as module definition here"
+  | Sut_type_not_specified ty ->
+      pf ppf "Missing specification for the SUT type %s" ty
+  | Sut_type_not_supported ty ->
+      pf ppf "Unsupported SUT type %s:@ %a" ty text
+        "SUT type must be a type constructor, possibly applied to type \
+         arguments"
+  | Syntax_error_in_config_module s ->
+      pf ppf "Syntax error in OCaml configuration module %s" s
+  | Type_not_supported_for_sut_parameter ty ->
+      pf ppf "Unsupported type parameter %s:@ %a" ty text
+        "only constructors and tuples are supported in arguments for the SUT \
+         type"
+  | Type_parameter_not_instantiated ty ->
+      pf ppf "Unsupported type parameter %s:@ %a" ty text
+        "SUT type should be fully instantiated"
   | _ -> W.pp_kind ppf kind
 
 let pp_errors = W.pp_param pp_kind level |> Fmt.list

From 6537f47ded3a84f6be89aaada183755ca8e54f83 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 16:46:53 +0100
Subject: [PATCH 21/27] Update Ortac/QCheck-STM README

---
 plugins/qcheck-stm/README.md | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/plugins/qcheck-stm/README.md b/plugins/qcheck-stm/README.md
index 7928dd23..a91d2835 100644
--- a/plugins/qcheck-stm/README.md
+++ b/plugins/qcheck-stm/README.md
@@ -60,10 +60,18 @@ indicate:
 - how to generate an initial value of that type, for instance
   `make 16 'a'`.
 
-Using those example values, you can run
+You can do so with the following `lib_conf.ml` file:
+
+```ocaml
+open Lib
+type sut = char t
+let init_sut = make 16 'a'
+```
+
+You can then run:
 
 ```shell
-$ ortac qcheck-stm lib.mli "make 16 'a'" "char t"
+$ ortac qcheck-stm lib.mli lib_conf.ml
 ```
 
 to generate the corresponding QCheck-STM program. The [QCheck-STM
@@ -75,7 +83,7 @@ one that is generated by the plugin.
 You can then save this module into a file:
 
 ```shell
-$ ortac qcheck-stm lib.mli "make 16 'a'" "char t" > main.ml
+$ ortac qcheck-stm lib.mli lib_conf.ml -o main.ml
 ```
 
 and compile this into an executable using:

From 4e0cdbfedae62e9aff35f533b9715576aac6d923 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 15:13:24 +0100
Subject: [PATCH 22/27] Update Ortac/Dune plugin to new qcheck-stm interface

---
 plugins/dune-rules/src/dune_rules.ml  | 29 ++++--------------
 plugins/dune-rules/src/qcheck_stm.ml  | 43 +++++++++------------------
 plugins/dune-rules/src/qcheck_stm.mli |  4 +--
 3 files changed, 21 insertions(+), 55 deletions(-)

diff --git a/plugins/dune-rules/src/dune_rules.ml b/plugins/dune-rules/src/dune_rules.ml
index dc278113..b8a32f70 100644
--- a/plugins/dune-rules/src/dune_rules.ml
+++ b/plugins/dune-rules/src/dune_rules.ml
@@ -17,22 +17,16 @@ end = struct
         & info [] ~doc:"Interface file containing Gospel specifications"
             ~docv:"INTERFACE")
 
-    let init =
+    let config_file =
       Arg.(
         required
         & pos 1 (some string) None
-        & info [] ~doc:"Init function to feed to ortac qcheck-stm" ~docv:"INIT")
-
-    let sut =
-      Arg.(
-        required
-        & pos 2 (some string) None
-        & info [] ~doc:"Sut type to feed to ortac qcheck-stm" ~docv:"SUT")
+        & info [] ~doc:"Configuration file for Ortac/QCheckSTM" ~docv:"CONFIG")
 
     let ocaml_output =
       Arg.(
         required
-        & pos 3 (some string) None
+        & pos 2 (some string) None
         & info [] ~doc:"Filename for the generated tests" ~docv:"OCAML_OUTPUT")
 
     let package_name =
@@ -48,19 +42,10 @@ end = struct
         & info [ "w"; "with-stdout-to" ]
             ~doc:"Filename for the generated dune rules" ~docv:"DUNE_OUTPUT")
 
-    let main interface_file init_function sut_type ocaml_output include_
-        package_name dune_output =
+    let main interface_file config_file ocaml_output package_name dune_output =
       let open Qcheck_stm in
       let config =
-        {
-          interface_file;
-          init_function;
-          sut_type;
-          ocaml_output;
-          include_;
-          package_name;
-          dune_output;
-        }
+        { interface_file; config_file; ocaml_output; package_name; dune_output }
       in
       let ppf = Registration.get_out_formatter dune_output in
       Qcheck_stm.gen_dune_rules ppf config
@@ -69,10 +54,8 @@ end = struct
       Term.(
         const main
         $ interface_file
-        $ init
-        $ sut
+        $ config_file
         $ ocaml_output
-        $ Registration.include_
         $ package_name
         $ with_stdout_to)
 
diff --git a/plugins/dune-rules/src/qcheck_stm.ml b/plugins/dune-rules/src/qcheck_stm.ml
index 0acd2601..74ba2300 100644
--- a/plugins/dune-rules/src/qcheck_stm.ml
+++ b/plugins/dune-rules/src/qcheck_stm.ml
@@ -1,9 +1,7 @@
 type config = {
   interface_file : string;
-  init_function : string;
-  sut_type : string;
+  config_file : string;
   ocaml_output : string;
-  include_ : string option;
   package_name : string option;
   dune_output : string option;
 }
@@ -21,7 +19,6 @@ let msg ppf config =
      ; change some options rather that running ortac on the command line again@\n"
     config.interface_file
 
-let quote ppf s = pf ppf "%S" s
 let stanza k ppf config = pf ppf "@[<v 1>(%a)@]" k config
 let stanza_rule k ppf config = pf ppf "%a@." (stanza k) config
 
@@ -49,20 +46,22 @@ let ortac ppf _ = pf ppf "ortac"
 let dune ppf _ = pf ppf "dune"
 let qcheck_stm ppf _ = pf ppf "qcheck-stm"
 let interface ppf config = pf ppf "%s" config.interface_file
-let interface_mli ppf config = pf ppf "%%{dep:%s.mli}" config.interface_file
-let init_sut ppf config = pf ppf "%a" quote config.init_function
-let sut ppf config = pf ppf "%a" quote config.sut_type
+let config_file ppf config = pf ppf "%s" config.config_file
 let ocaml_output ppf config = pf ppf "%s" config.ocaml_output
 let runtest ppf _ = pf ppf "(alias runtest)"
 let promote ppf _ = pf ppf "(mode promote)"
-let name ppf config = pf ppf "(name %s)" config.ocaml_output
+
+let name ppf config =
+  pf ppf "(name %s)" (Filename.chop_extension config.ocaml_output)
+
+let dep aux ppf config = pf ppf "%%{dep:%a}" aux config
 
 let libraries =
   let k ppf config =
     pf ppf
       "libraries@ %s@ qcheck-stm.stm@ qcheck-stm.sequential@ \
        qcheck-multicoretests-util@ ortac-runtime-qcheck-stm"
-      config.interface_file
+      (Filename.chop_extension config.interface_file)
   in
   stanza k
 
@@ -77,27 +76,20 @@ let deps plug ppf _ =
   pf ppf "(deps@; %a)" package p
 
 let optional ppf s = function None -> () | Some x -> pf ppf s x
-let include_ ppf config = optional ppf "--include=%s" config.include_
 let quiet ppf _ = pf ppf "--quiet"
 let package_opt ppf config = optional ppf "--package=%s" config.package_name
 let package ppf config = optional ppf "(package %s)" config.package_name
-let targets_ml ppf config = pf ppf "(targets %s.ml)" config.ocaml_output
+let targets_ml ppf config = pf ppf "(targets %s)" config.ocaml_output
 let targets_dune ppf config = optional ppf "(targets %s)" config.dune_output
 
 let with_stdout_to ppf config =
   optional ppf "--with-stdout-to=%s" config.dune_output
 
-type optional_stanza =
-  | Include_
-  | Package_opt
-  | Package
-  | Targets_dune
-  | With_stdout_to
+type optional_stanza = Package_opt | Package | Targets_dune | With_stdout_to
 
 let get config =
   let aux x = function None -> [] | Some _ -> [ x ] in
   function
-  | Include_ -> aux include_ config.include_
   | Package_opt -> aux package_opt config.package_name
   | Package -> aux package config.package_name
   | Targets_dune -> aux targets_dune config.dune_output
@@ -105,12 +97,9 @@ let get config =
 
 let gen_gen_rule ppf config =
   let get = get config in
-  let opt_args =
-    List.flatten [ get Include_; get Package_opt; get With_stdout_to ]
-  in
+  let opt_args = List.flatten [ get Package_opt; get With_stdout_to ] in
   let args =
-    [ ortac; dune; qcheck_stm; interface; init_sut; sut; ocaml_output ]
-    @ opt_args
+    [ ortac; dune; qcheck_stm; interface; config_file; ocaml_output ] @ opt_args
   in
   let run ppf = run ppf args in
   let run = stanza run in
@@ -123,9 +112,7 @@ let gen_gen_rule ppf config =
 let gen_ortac_rule ppf config =
   let get = get config in
   let args =
-    [ ortac; qcheck_stm; interface_mli; init_sut; sut ]
-    @ get Include_
-    @ [ quiet ]
+    [ ortac; qcheck_stm; dep interface; dep config_file ] @ [ quiet ]
   in
   let run ppf = run ppf args in
   let run = stanza run in
@@ -139,9 +126,7 @@ let gen_ortac_rule ppf config =
 let gen_test_rule ppf config =
   let get = get config in
   let modules ppf config =
-    match config.include_ with
-    | None -> pf ppf "(modules %s)" config.ocaml_output
-    | Some i -> pf ppf "(modules %s %s)" config.ocaml_output i
+    pf ppf "(modules %s)" (Filename.chop_extension config.ocaml_output)
   in
   let run ppf =
     run ppf
diff --git a/plugins/dune-rules/src/qcheck_stm.mli b/plugins/dune-rules/src/qcheck_stm.mli
index e9e3e189..10469894 100644
--- a/plugins/dune-rules/src/qcheck_stm.mli
+++ b/plugins/dune-rules/src/qcheck_stm.mli
@@ -1,9 +1,7 @@
 type config = {
   interface_file : string;
-  init_function : string;
-  sut_type : string;
+  config_file : string;
   ocaml_output : string;
-  include_ : string option;
   package_name : string option;
   dune_output : string option;
 }

From c73610e17889738b635a9782a5c8f68b32220ebc Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 15:21:58 +0100
Subject: [PATCH 23/27] Update Ortac/Dune cram tests

---
 plugins/dune-rules/test/test.t | 34 +++++++++++++---------------------
 1 file changed, 13 insertions(+), 21 deletions(-)

diff --git a/plugins/dune-rules/test/test.t b/plugins/dune-rules/test/test.t
index e51aed50..04c19610 100644
--- a/plugins/dune-rules/test/test.t
+++ b/plugins/dune-rules/test/test.t
@@ -7,7 +7,7 @@ Without the optional output argument (for the dune rules, output for the generat
 has to be set), the rules are printed on stdout. This is useful to check what will be
 generated.
 
-  $ ortac dune qcheck-stm intf_spec "init_sut ()" "int sut" test --include=included --package=my_package
+  $ ortac dune qcheck-stm intf_spec.mli config_mod.ml test.ml --package=my_package
   (rule
    (alias runtest)
    (mode promote)
@@ -22,11 +22,9 @@ generated.
       ortac
       dune
       qcheck-stm
-      intf_spec
-      "init_sut ()"
-      "int sut"
-      test
-      --include=included
+      intf_spec.mli
+      config_mod.ml
+      test.ml
       --package=my_package))))
   
   (rule
@@ -46,14 +44,12 @@ generated.
        ortac
        qcheck-stm
        %{dep:intf_spec.mli}
-       "init_sut ()"
-       "int sut"
-       --include=included
+       %{dep:config_mod.ml}
        --quiet)))))
   
   (test
    (name test)
-   (modules test included)
+   (modules test)
    (libraries
     intf_spec
     qcheck-stm.stm
@@ -69,10 +65,10 @@ generated.
 When the optional output argument is set, rules will be written in the file and will reflect
 this fact.
 
-  $ ortac dune qcheck-stm intf_spec "init_sut ()" "int sut" test --include=included --package=my_package --with-stdout-to=dune.inc
+  $ ortac dune qcheck-stm intf_spec.mli config_mod.ml test.ml --package=my_package --with-stdout-to=dune.inc
   $ cat dune.inc
   ; This file is generated by ortac dune qcheck-stm
-  ; It contains the rules for generating and running QCheck-STM tests for intf_spec
+  ; It contains the rules for generating and running QCheck-STM tests for intf_spec.mli
   ; It also contains the rule to generate itself, so you can edit this rule to
   ; change some options rather that running ortac on the command line again
   
@@ -91,11 +87,9 @@ this fact.
       ortac
       dune
       qcheck-stm
-      intf_spec
-      "init_sut ()"
-      "int sut"
-      test
-      --include=included
+      intf_spec.mli
+      config_mod.ml
+      test.ml
       --package=my_package
       --with-stdout-to=dune.inc))))
   
@@ -116,14 +110,12 @@ this fact.
        ortac
        qcheck-stm
        %{dep:intf_spec.mli}
-       "init_sut ()"
-       "int sut"
-       --include=included
+       %{dep:config_mod.ml}
        --quiet)))))
   
   (test
    (name test)
-   (modules test included)
+   (modules test)
    (libraries
     intf_spec
     qcheck-stm.stm

From bf58af855db73306bf390557d843c7f075d8ced8 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 16:42:42 +0100
Subject: [PATCH 24/27] Update Ortac/Dune README

---
 plugins/dune-rules/README.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/plugins/dune-rules/README.md b/plugins/dune-rules/README.md
index f0901e19..9078e666 100644
--- a/plugins/dune-rules/README.md
+++ b/plugins/dune-rules/README.md
@@ -20,18 +20,18 @@ plugins (the qcheck-stm plugin for now). You have to give it the option you want
 pass to the other plugins and some more information for dune.
 
 Let's say you want use the [Ortac/QCheck-STM] plugin on a module interface
-`lib.mli` to generate QCheck-STM tests for this module using `make 42 'a'` as
-initial value of type `char t`, including the `Lib_incl` module, in the context
-of the `pack` package.
+`lib.mli` to generate QCheck-STM tests with the `lib_conf.ml` configuration, in
+the context of the `pack` package.
 
 Then you can run:
 
 ```shell
-$ ortac dune qcheck-stm lib "make 42 'a'" "char t" lib_tests --include=lib_incl --package=pack --with-stdout-to=dune.inc
+$ ortac dune qcheck-stm lib.mli lib_conf.ml lib_tests.ml --package=pack --with-stdout-to=dune.inc
 ```
 
-to generate the dune rules to generate and run the tests. Next time you run
-`dune runtest`, your code should be tested using QCheck-STM.
+to generate the dune rules to generate and run the tests. You can then include
+`dune.inc` in the `dune` file and the next time you run `dune runtest`, your
+code should be tested using QCheck-STM.
 
 [Ortac/QCheck-STM]: ../qcheck-stm/README.md
 

From 92b70d758f04d97c0baa8067177b08350a8edf13 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 16:30:59 +0100
Subject: [PATCH 25/27] Update examples to new interface

---
 examples/README.md                 | 13 ++++++-------
 examples/dune.lwt_dllist.inc       | 16 ++++++----------
 examples/dune.varray.inc           | 16 ++++++----------
 examples/dune.varray_circular.inc  | 16 ++++++----------
 examples/lwt_dllist_config.ml      | 13 +++++++++++++
 examples/lwt_dllist_incl.ml        |  8 --------
 examples/lwt_dllist_tests.ml       |  6 +++++-
 examples/varray_circular_config.ml | 26 ++++++++++++++++++++++++++
 examples/varray_circular_incl.ml   | 27 ---------------------------
 examples/varray_circular_tests.ml  | 24 +++++++++++++++++++++++-
 examples/varray_config.ml          | 26 ++++++++++++++++++++++++++
 examples/varray_incl.ml            | 27 ---------------------------
 examples/varray_tests.ml           | 24 +++++++++++++++++++++++-
 13 files changed, 140 insertions(+), 102 deletions(-)
 create mode 100644 examples/lwt_dllist_config.ml
 delete mode 100644 examples/lwt_dllist_incl.ml
 create mode 100644 examples/varray_circular_config.ml
 delete mode 100644 examples/varray_circular_incl.ml
 create mode 100644 examples/varray_config.ml
 delete mode 100644 examples/varray_incl.ml

diff --git a/examples/README.md b/examples/README.md
index 24239c70..27dd98a9 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -28,9 +28,8 @@ need to be visible.
 The STM `postcond` function pattern match on the returned value encapsulated in
 a `STM.ty`. As functions `add_l` and `add_r` both return the node that has been
 added, we need to extend the `STM.ty` type with an encoding for
-`Lwt_dllist.node`. We add this extension in the external module
-`Lwt_dllist_incl` and pass it to the `--include` option of the `ortac
-qcheck-stm` command.
+`Lwt_dllist.node`. We add this extension in the configuration module for
+Ortac/QCheckSTM.
 
 The generated code can be found in `lwt_dllist_tests.ml`. You can run the test
 either with `dune runtest examples/` or by directly running the compiled
@@ -40,7 +39,7 @@ Dune rules have been generated using the `dune-rules` plugin, providing the
 `dune` subcommand:
 
 ```sh
-$ ortac dune qcheck-stm lwt_dllist_spec "create ()" "int t" lwt_dllist_tests --include=lwt_dllist_incl --package=ortac-examples --with-stdout-to=dune.lwt_dllist.inc
+$ ortac dune qcheck-stm lwt_dllist_spec.mli lwt_dllist_config.ml lwt_dllist_tests.ml --package=ortac-examples --with-stdout-to=dune.lwt_dllist.inc
 ```
 
 ## `varray` library
@@ -62,8 +61,8 @@ dune-generated `mli` files hidden in the `_build` folder.
 Here again, as for the previous example, we need to include some code. That is
 the extension of the `STM.ty` type. But also a `QCheck` generator for the `'a
 elt` type, as some functions of the library take arguments of this type. You
-can find these extensions in the `varray_incl.ml` and `varray_circular_incl.ml`
-files.
+can find these extensions in the `varray_config.ml` and
+`varray_circular_config.ml` files.
 
 The generated code can be found in the respective `varray*tests.ml` files. They
 have been promoted in the source tree in order to be easily accessible for
@@ -74,6 +73,6 @@ following command for `varray_spec.mli` and an adapted version for
 `varray_circular_spec.mli`:
 
 ```sh
-$ ortac dune qcheck-stm varray_spec "make 42 'a'" "char t" varray_tests --include=varray_incl --package=ortac-examples --with-stdout-to=dune.varray.inc
+$ ortac dune qcheck-stm varray_spec.mli varray_config.ml varray_tests.ml --package=ortac-examples --with-stdout-to=dune.varray.inc
 ```
 
diff --git a/examples/dune.lwt_dllist.inc b/examples/dune.lwt_dllist.inc
index 881c3650..9f461598 100644
--- a/examples/dune.lwt_dllist.inc
+++ b/examples/dune.lwt_dllist.inc
@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for lwt_dllist_spec
+; It contains the rules for generating and running QCheck-STM tests for lwt_dllist_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    lwt_dllist_spec
-    "create ()"
-    "int t"
-    lwt_dllist_tests
-    --include=lwt_dllist_incl
+    lwt_dllist_spec.mli
+    lwt_dllist_config.ml
+    lwt_dllist_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.lwt_dllist.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:lwt_dllist_spec.mli}
-     "create ()"
-     "int t"
-     --include=lwt_dllist_incl
+     %{dep:lwt_dllist_config.ml}
      --quiet)))))
 
 (test
  (name lwt_dllist_tests)
- (modules lwt_dllist_tests lwt_dllist_incl)
+ (modules lwt_dllist_tests)
  (libraries
   lwt_dllist_spec
   qcheck-stm.stm
diff --git a/examples/dune.varray.inc b/examples/dune.varray.inc
index 163756c9..ae10cbfe 100644
--- a/examples/dune.varray.inc
+++ b/examples/dune.varray.inc
@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for varray_spec
+; It contains the rules for generating and running QCheck-STM tests for varray_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    varray_spec
-    "make 42 'a'"
-    "char t"
-    varray_tests
-    --include=varray_incl
+    varray_spec.mli
+    varray_config.ml
+    varray_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.varray.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:varray_spec.mli}
-     "make 42 'a'"
-     "char t"
-     --include=varray_incl
+     %{dep:varray_config.ml}
      --quiet)))))
 
 (test
  (name varray_tests)
- (modules varray_tests varray_incl)
+ (modules varray_tests)
  (libraries
   varray_spec
   qcheck-stm.stm
diff --git a/examples/dune.varray_circular.inc b/examples/dune.varray_circular.inc
index 7b73c2f4..16a07cda 100644
--- a/examples/dune.varray_circular.inc
+++ b/examples/dune.varray_circular.inc
@@ -1,5 +1,5 @@
 ; This file is generated by ortac dune qcheck-stm
-; It contains the rules for generating and running QCheck-STM tests for varray_circular_spec
+; It contains the rules for generating and running QCheck-STM tests for varray_circular_spec.mli
 ; It also contains the rule to generate itself, so you can edit this rule to
 ; change some options rather that running ortac on the command line again
 
@@ -18,11 +18,9 @@
     ortac
     dune
     qcheck-stm
-    varray_circular_spec
-    "make 42 'a'"
-    "char t"
-    varray_circular_tests
-    --include=varray_circular_incl
+    varray_circular_spec.mli
+    varray_circular_config.ml
+    varray_circular_tests.ml
     --package=ortac-examples
     --with-stdout-to=dune.varray_circular.inc))))
 
@@ -43,14 +41,12 @@
      ortac
      qcheck-stm
      %{dep:varray_circular_spec.mli}
-     "make 42 'a'"
-     "char t"
-     --include=varray_circular_incl
+     %{dep:varray_circular_config.ml}
      --quiet)))))
 
 (test
  (name varray_circular_tests)
- (modules varray_circular_tests varray_circular_incl)
+ (modules varray_circular_tests)
  (libraries
   varray_circular_spec
   qcheck-stm.stm
diff --git a/examples/lwt_dllist_config.ml b/examples/lwt_dllist_config.ml
new file mode 100644
index 00000000..a0ca5dd5
--- /dev/null
+++ b/examples/lwt_dllist_config.ml
@@ -0,0 +1,13 @@
+open Lwt_dllist_spec
+
+type sut = int t
+
+let init_sut = create ()
+
+module Ty = struct
+  type _ ty += Node : 'a ty -> 'a node ty
+
+  let node spec =
+    let ty, show = spec in
+    (Node ty, fun n -> Printf.sprintf "Node %s" (show (get n)))
+end
diff --git a/examples/lwt_dllist_incl.ml b/examples/lwt_dllist_incl.ml
deleted file mode 100644
index 0afe0995..00000000
--- a/examples/lwt_dllist_incl.ml
+++ /dev/null
@@ -1,8 +0,0 @@
-open Lwt_dllist_spec
-open STM
-
-type _ ty += Node : 'a ty -> 'a node ty
-
-let node spec =
-  let ty, show = spec in
-  (Node ty, fun n -> Printf.sprintf "Node %s" (show (get n)))
diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml
index 099ae07b..29b04ef5 100644
--- a/examples/lwt_dllist_tests.ml
+++ b/examples/lwt_dllist_tests.ml
@@ -6,7 +6,11 @@ module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =
   struct
     open STM
-    include Lwt_dllist_incl
+    type _ ty +=  
+      | Node: 'a ty -> 'a node ty 
+    let node spec =
+      let (ty, show) = spec in
+      ((Node ty), (fun n -> Printf.sprintf "Node %s" (show (get n))))
     type sut = int t
     type cmd =
       | Is_empty 
diff --git a/examples/varray_circular_config.ml b/examples/varray_circular_config.ml
new file mode 100644
index 00000000..726fe416
--- /dev/null
+++ b/examples/varray_circular_config.ml
@@ -0,0 +1,26 @@
+open Varray
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Pp = struct
+  include Util.Pp
+
+  let pp_elt pp = pp
+end
+
+module Gen = struct
+  include QCheck.Gen
+
+  let int = small_signed_int
+  let elt gen = gen
+end
+
+module Ty = struct
+  type _ ty += Elt : 'a ty -> 'a elt ty
+
+  let elt spec =
+    let ty, show = spec in
+    (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x))
+end
diff --git a/examples/varray_circular_incl.ml b/examples/varray_circular_incl.ml
deleted file mode 100644
index cfe35125..00000000
--- a/examples/varray_circular_incl.ml
+++ /dev/null
@@ -1,27 +0,0 @@
-module Util = struct
-  module Pp = struct
-    include Util.Pp
-
-    let pp_elt pp = pp
-  end
-end
-
-module QCheck = struct
-  include QCheck
-
-  module Gen = struct
-    include QCheck.Gen
-
-    let int = small_signed_int
-    let elt gen = gen
-  end
-end
-
-open STM
-open Varray_circular_spec
-
-type _ ty += Elt : 'a ty -> 'a elt ty
-
-let elt spec =
-  let ty, show = spec in
-  (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x))
diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml
index c7937aff..80d98460 100644
--- a/examples/varray_circular_tests.ml
+++ b/examples/varray_circular_tests.ml
@@ -62,7 +62,29 @@ let proj e =
 module Spec =
   struct
     open STM
-    include Varray_circular_incl
+    module QCheck =
+      struct
+        include QCheck
+        module Gen =
+          struct
+            include Gen
+            include QCheck.Gen
+            let int = small_signed_int
+            let elt gen = gen
+          end
+      end
+    module Util =
+      struct
+        module Pp =
+          struct include Util.Pp
+                 include Util.Pp
+                 let pp_elt pp = pp end
+      end
+    type _ ty +=  
+      | Elt: 'a ty -> 'a elt ty 
+    let elt spec =
+      let (ty, show) = spec in
+      ((Elt ty), (fun x -> Printf.sprintf "Elt %s" (show x)))
     type sut = char t
     type cmd =
       | Push_back of char elt 
diff --git a/examples/varray_config.ml b/examples/varray_config.ml
new file mode 100644
index 00000000..726fe416
--- /dev/null
+++ b/examples/varray_config.ml
@@ -0,0 +1,26 @@
+open Varray
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Pp = struct
+  include Util.Pp
+
+  let pp_elt pp = pp
+end
+
+module Gen = struct
+  include QCheck.Gen
+
+  let int = small_signed_int
+  let elt gen = gen
+end
+
+module Ty = struct
+  type _ ty += Elt : 'a ty -> 'a elt ty
+
+  let elt spec =
+    let ty, show = spec in
+    (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x))
+end
diff --git a/examples/varray_incl.ml b/examples/varray_incl.ml
deleted file mode 100644
index 1fe4712e..00000000
--- a/examples/varray_incl.ml
+++ /dev/null
@@ -1,27 +0,0 @@
-module Util = struct
-  module Pp = struct
-    include Util.Pp
-
-    let pp_elt pp = pp
-  end
-end
-
-module QCheck = struct
-  include QCheck
-
-  module Gen = struct
-    include QCheck.Gen
-
-    let int = small_signed_int
-    let elt gen = gen
-  end
-end
-
-open STM
-open Varray_spec
-
-type _ ty += Elt : 'a ty -> 'a elt ty
-
-let elt spec =
-  let ty, show = spec in
-  (Elt ty, fun x -> Printf.sprintf "Elt %s" (show x))
diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml
index 5afd33ac..538ad0e0 100644
--- a/examples/varray_tests.ml
+++ b/examples/varray_tests.ml
@@ -62,7 +62,29 @@ let proj e =
 module Spec =
   struct
     open STM
-    include Varray_incl
+    module QCheck =
+      struct
+        include QCheck
+        module Gen =
+          struct
+            include Gen
+            include QCheck.Gen
+            let int = small_signed_int
+            let elt gen = gen
+          end
+      end
+    module Util =
+      struct
+        module Pp =
+          struct include Util.Pp
+                 include Util.Pp
+                 let pp_elt pp = pp end
+      end
+    type _ ty +=  
+      | Elt: 'a ty -> 'a elt ty 
+    let elt spec =
+      let (ty, show) = spec in
+      ((Elt ty), (fun x -> Printf.sprintf "Elt %s" (show x)))
     type sut = char t
     type cmd =
       | Push_back of char elt 

From 2dcee7a1747f09ebb8f9ef483adcd620d8467df7 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 28 Mar 2024 17:49:01 +0100
Subject: [PATCH 26/27] Update Ortac/QCheck-STM documentation

---
 plugins/qcheck-stm/doc/example_config.ml      |  5 ++
 .../qcheck-stm/doc/example_config_qcheck.ml   |  9 +++
 plugins/qcheck-stm/doc/index.mld              | 69 ++++++++++++++-----
 3 files changed, 67 insertions(+), 16 deletions(-)
 create mode 100644 plugins/qcheck-stm/doc/example_config.ml
 create mode 100644 plugins/qcheck-stm/doc/example_config_qcheck.ml

diff --git a/plugins/qcheck-stm/doc/example_config.ml b/plugins/qcheck-stm/doc/example_config.ml
new file mode 100644
index 00000000..19063db7
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_config.ml
@@ -0,0 +1,5 @@
+open Example
+
+type sut = char t
+
+let init_sut = make 42 'a'
diff --git a/plugins/qcheck-stm/doc/example_config_qcheck.ml b/plugins/qcheck-stm/doc/example_config_qcheck.ml
new file mode 100644
index 00000000..a625cb4f
--- /dev/null
+++ b/plugins/qcheck-stm/doc/example_config_qcheck.ml
@@ -0,0 +1,9 @@
+open Example
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Gen = struct
+  let int = small_signed_int
+end
diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld
index 0b6e20fd..bf42a871 100644
--- a/plugins/qcheck-stm/doc/index.mld
+++ b/plugins/qcheck-stm/doc/index.mld
@@ -18,7 +18,7 @@ pieces of information:
     {- How to generate the said model? The [init_state] function.}
     {- How does the model change when calling a function? The [next_state] function.}}
 
-Answering these five questions is done part in the command-line arguments and
+Answering these five questions is done part in a configuration module and
 part in the Gospel specifications that you will have to write in a specific
 style.
 
@@ -141,15 +141,56 @@ In order to generate postcondition-checking, Ortac/QCheck-STM uses the
 [ensures] clauses that were not used for the [next_state] function but it also
 uses the [checks] clauses and the [raises] ones.
 
-Now you can generate the QCheck-STM file by running the following command where
-you indicate the file you want to test, the function call to build a value of
-the type indicated in the third argument. You can write the generated code into
-a file, using the [-o] option.
+Now you need a configuration file. Configuration files for Ortac/QCheck-STM are
+OCaml modules containing {e at least} a type declaration for `sut` (usually the
+type `t` of the module under test with all the type parameters instantiated)
+and a value declaration for `init_sut` (a call to a function from the module
+under test returning a value of type `sut`)
+
+{@ocaml file=example_config.ml[
+open Example
+
+type sut = char t
+
+let init_sut = make 42 'a'
+]}
+
+Then, you can generate the QCheck-STM file by running the following command where
+you indicate the file you want to test and the configuration file. You can
+write the generated code into a file, using the [-o] option.
 
 {@sh set-ORTAC_ONLY_PLUGIN=qcheck-stm[
-$ ortac qcheck-stm example.mli "make 42 'a'" "char t" -o stm_example.ml
+$ ortac qcheck-stm example.mli example_config.ml -o stm_example.ml
+]}
+
+The other information you can put in the configuration file are:
+
+{ul {li custom [QCheck] generators in a [Gen] module}
+    {li custom [STM] printers in a [Pp] module}
+    {li custom [STM.ty] extensions and its functional constructors in a [Ty]
+    module}}
+
+Let's say for example that you want to run the generated tests using a custom
+generator for the type [int] that only generates small positive integers. You
+can still rely on the generated command generator, you just have to override the
+[int] generator:
+
+{@ocaml file=example_config_qcheck.ml[
+open Example
+
+type sut = char t
+
+let init_sut = make 42 'a'
+
+module Gen = struct
+  let int = small_signed_int
+end
 ]}
 
+When you have a user-defined type in the module under test, you have to declare
+an [STM] printer and an extension of the [STM.ty] type. This follows the same
+principle to include them in the configuration module.
+
 The generated OCaml file has a bunch of dependencies:
 
 {ul {li [qcheck-core] }
@@ -221,7 +262,7 @@ Ortac/QCheck-STM will look at the [modifies] clause and then look for an
 new value. Here, it won't find any and warn you with the following message:
 
 {@sh[
-$ ortac qcheck-stm example_next_state.mli "make 42 'a'" "char t" -o foo.ml
+$ ortac qcheck-stm example_next_state.mli example_config.ml -o foo.ml
 File "example_next_state.mli", line 15, characters 13-23:
 15 |     modifies t.contents
                   ^^^^^^^^^^
@@ -262,11 +303,7 @@ val type_not_supported : new_type -> 'a t -> new_type
 ]}
 
 {@sh[
-$ ortac qcheck-stm example_unknown_type.mli "make 42 'a'" "char t" -o foo.ml
-File "example_unknown_type.mli", line 15, characters 0-87:
-15 | val type_not_supported : new_type -> 'a t -> new_type
-16 | (*@ y = type_not_supported x t *)
-Warning: Incomplete computation of the returned value in the specification of type_not_supported. Failure message won't be able to display the expected returned value.
+$ ortac qcheck-stm example_unknown_type.mli example_config.ml -o foo.ml --quiet
 $ grep -A 1 "type cmd" foo.ml
     type cmd =
       | Type_not_supported of new_type
@@ -294,7 +331,7 @@ val ghost_arg : char -> 'a t -> bool
 the command will generate the following warning:
 
 {@sh[
-$ ortac qcheck-stm example_ghost.mli "make 42 'a'" "char t" -o foo.ml
+$ ortac qcheck-stm example_ghost.mli example_config.ml -o foo.ml
 File "example_ghost.mli", line 14, characters 20-21:
 14 | (*@ b = ghost_arg [ i : integer] c t *)
                          ^
@@ -320,7 +357,7 @@ val incompatible_type : char -> string t -> bool
 the plugin will generate a warning for this function and skip it.
 
 {@sh[
-$ ortac qcheck-stm example_incompatible_type.mli "make 42 'a'" "char t" -o foo.ml
+$ ortac qcheck-stm example_incompatible_type.mli example_config.ml -o foo.ml
 File "example_incompatible_type.mli", line 13, characters 32-40:
 13 | val incompatible_type : char -> string t -> bool
                                      ^^^^^^^^
@@ -351,7 +388,7 @@ val unsupported_quantification : 'a t -> bool
 the command will generate the following warning:
 
 {@sh[
-$ ortac qcheck-stm example_ill_formed_quantification.mli "make 42 'a'" "char t" -o foo.ml
+$ ortac qcheck-stm example_ill_formed_quantification.mli example_config.ml -o foo.ml
 File "example_ill_formed_quantification.mli", line 13, characters 0-142:
 13 | val unsupported_quantification : 'a t -> bool
 14 | (*@ b = unsupported_quantification t
@@ -409,7 +446,7 @@ val for_all : ('a -> bool) -> 'a t -> bool
 Ortac/QCheck-STM will generate the following warnings:
 
 {@sh[
-$ ortac qcheck-stm example_limitations.mli "make 42 'a'" "char t" -o foo.ml
+$ ortac qcheck-stm example_limitations.mli example_config.ml -o foo.ml
 File "example_limitations.mli", line 13, characters 8-26:
 13 | val f : int -> int -> bool
              ^^^^^^^^^^^^^^^^^^

From e190f824209b3c2be3af64594e1bc592fceabcf8 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Thu, 23 May 2024 15:50:00 +0200
Subject: [PATCH 27/27] Update Changelog

---
 CHANGES.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index b580a53c..a5598c68 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Move to a module-based configuration
+  [\#214](https://github.com/ocaml-gospel/ortac/pull/214)
 - Add support for custom ghost types as model
   [\#228](https://github.com/ocaml-gospel/ortac/pull/228)