@@ -141,6 +141,8 @@ In order to generate postcondition-checking, Ortac/QCheck-STM uses the
141
141
[ensures] clauses that were not used for the [next_state] function but it also
142
142
uses the [checks] clauses and the [raises] ones.
143
143
144
+ {1 How to generate the test file }
145
+
144
146
Now you can generate the QCheck-STM file by running the following command where
145
147
you indicate the file you want to test, the function call to build a value of
146
148
the type indicated in the third argument. You can write the generated code into
@@ -177,6 +179,20 @@ like the following:
177
179
(run %{test} --verbose)))
178
180
]}
179
181
182
+ There are other optional argument that are worth detailing here.
183
+
184
+ The first one is the [-i] optional argument, taking the name of the module to
185
+ include in the generated code. This is a flexible way to provide pretty
186
+ pinters, QCheck generators and extenstions to the [STM.ty] type.
187
+
188
+ The second one is the [-p] optional argument, taking a string. The string
189
+ should be the name of a function, and the function will be protecting the call
190
+ to the generated tests. The function should be implemented in the included
191
+ module (the one passed to the [-i] optional argument). The funciton is of type
192
+ [(unit -> unit) -> unit]. That means that it takes the suspended call the the
193
+ generated tests as argument, so don't forget to launch them when implementing
194
+ the function. One use case of this optional argument is to set up a [Lwt]
195
+ scheduler berfore running the tests.
180
196
{1 Warning system}
181
197
182
198
Now that you know what Gospel specifications for the [qcheck-stm] plugin should
0 commit comments