Hi everyone!
We - at Tarides - are very pleased to announce the release of the Ortac-0.6.0 packages for specification-driven testing!
Ortac/QCheck-STM is a test generator based on the QCheck-STM model-based testing framework and the Gospel specification language for OCaml.
In addition to generating QCheck-STM tests based on the Gospel specifications, Ortac/QCheck-STM computes and display a bug report in case of test failure.
This report contains the piece of Gospel specification that has been violated, a runnable scenario to reproduce the bug and the expected returned value (if there is enough information in the specification to compute it).
This release improves the reporting in two ways.
First, the way we need to formulate the description of the expected returned value has been made more flexible (and fixed). The main limitation was about functions returning a boolean. Because of the coercion mechanism, Gospel often transforms equalities involving a boolean into a double implication. For example: b = Sequence.mem t.contents a is transformed into b = true <-> Sequence.mem t.contents a. (For the curious, this is because Sequence.mem returns a prop, not a bool, and we don’t have equality on prop). Ortac/QCheck-STM now explores more patterns, including the double implication one, to try to find a suitable description of the returned value to use in the bug report.
Secondly, and more importantly, the Gospel specification language supports partial functions (Sequence.hd is not defined on the empty sequence for example). When we translate calls to such function to OCaml, we raise an exception when the call is out of the function’s domain. Now, that exception was captured by QCheck at runtime, making the test a failure as expected. But the Ortac runtime was then stopped before being able to build and send the bug report to QCheck for display to the user. That was sad, so I’ve fixed it. We can now make use of Gospel partial functions when writing specifications and enjoy the bug report computed by Ortac/QCheck-STM!
You can install Ortac/QCheck-STM via opam (we also advise installing and using Ortac/Dune):
$ opam install ortac-qcheck-stm ortac-dune
You’ll find more information in Ortac/QCheck-STM documentation and in The Ortac/Dune readme.
If you have any questions, please don’t hesitate to ping me 
Next release should be about making Ortac/QCheck-STM generate tests of a library in a parallel context (this is, after all, one of the raison d’être of the fantastic QCheck-STM test framework!).
Happy testing!