Skip to content

Commit

Permalink
Update Ortac/QCheck-STM README
Browse files Browse the repository at this point in the history
  • Loading branch information
n-osborne committed Apr 16, 2024
1 parent 088e67c commit 36b2ef4
Showing 1 changed file with 11 additions and 3 deletions.
14 changes: 11 additions & 3 deletions plugins/qcheck-stm/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand Down

0 comments on commit 36b2ef4

Please sign in to comment.