package ortac-runtime-qcheck-stm

  1. Overview
  2. Docs
Runtime support library for Ortac/QCheck-STM-generated code

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (5)

Authors

  1. N
    Nicolas Osborne <nicolas.osborne@tarides.com>
  2. N
    Nikolaus Huber <mail@n-huber.eu>

Maintainers

  1. N
    Nicolas Osborne <nicolas.osborne@tarides.com>

Sources

.tar.gz
md5=1bbffc8b2ecf943c2d66bdf9c72b994a
sha512=f23537bc18149e5cf5f5035139fac0541b55f7087127b1ca963f16d8852096d7fbdd5378b9fbb7703a3ce175b4a90ad8a7dfafc4292b5f1196fa11fbef43a178

doc/src/ortac-runtime-qcheck-stm.sequential/ortac_runtime_qcheck_stm_sequential.ml.html

Source file ortac_runtime_qcheck_stm_sequential.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
open Ortac_runtime_qcheck_stm_util
open STM
include Ortac_runtime
module Report = Report
module Model = Stores.Model
module SUT = Stores.SUT

module Make (Spec : Spec) = struct
  open Report
  open QCheck
  module Internal = Internal.Make (Spec) [@alert "-internal"]

  let pp_program max_suts ppf (trace, report) =
    let open Fmt in
    let inits =
      List.init max_suts (fun i ->
          Format.asprintf "let sut%d = %s" i report.init_sut)
    in
    pf ppf
      "@[%s@\n\
       open %s@\n\
       let protect f = try Ok (f ()) with e -> Error e@\n\
       %a@\n\
       %a@]"
      "[@@@ocaml.warning \"-8\"]" report.mod_name
      Format.(
        pp_print_list ~pp_sep:(fun pf _ -> fprintf pf "@\n") pp_print_string)
      inits
      (pp_traces true report.exp_res)
      trace

  let rec check_disagree postcond ortac_show_cmd s sut cs =
    match cs with
    | [] -> None
    | c :: cs -> (
        let res = Spec.run c sut in
        let s' = Spec.next_state c s in
        let call = lazy (ortac_show_cmd c s' (cs = []) res) in
        (* This functor will be called after a modified postcond has been
           defined, returning a list of 3-plets containing the command, the
           term and the location *)
        match postcond c s res with
        | None -> (
            match check_disagree postcond ortac_show_cmd s' sut cs with
            | None -> None
            | Some (rest, report) -> Some ({ call; res } :: rest, report))
        | Some report -> Some ([ { call; res } ], report))

  let agree_prop max_suts check_init_state ortac_show_cmd postcond cs =
    check_init_state ();
    assume (Internal.cmds_ok Spec.init_state cs);
    let sut = Spec.init_sut () in
    (* reset system's state *)
    let res =
      try Ok (check_disagree postcond ortac_show_cmd Spec.init_state sut cs)
      with exn -> Error exn
    in
    let () = Spec.cleanup sut in
    let res = match res with Ok res -> res | Error exn -> raise exn in
    match res with
    | None -> true
    | Some (trace, report) -> message (pp_program max_suts) trace report

  let agree_test ~count ~name max_suts wrapped_init_state ortac_show_cmd
      postcond =
    let test_prop =
      agree_prop max_suts wrapped_init_state ortac_show_cmd postcond
    in
    let env_var_fail () =
      let msg = "ORTAC_QCHECK_STM_TIMEOUT must be set to a positive integer" in
      Printf.eprintf "%s" msg;
      exit 1
    in
    let wrapped_prop =
      match Sys.getenv_opt "ORTAC_QCHECK_STM_TIMEOUT" with
      | None -> test_prop
      | Some time ->
          let timeout = try int_of_string time with _ -> env_var_fail () in
          if timeout <= 0 then env_var_fail ();
          Util.fork_prop_with_timeout timeout test_prop
    in
    Test.make ~name ~count (Internal.arb_cmds Spec.init_state) wrapped_prop
end