Source file `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
open STM

module MakeExt (Spec: SpecExt) = struct

  open QCheck
  open Internal.Make(Spec)
    [@alert "-internal"]

  (* re-export some functions *)
  let cmds_ok        = cmds_ok
  let arb_cmds       = arb_cmds

  let print_seq_trace trace =
    List.fold_left
      (fun acc (c,r) -> Printf.sprintf "%s\n   %s : %s" acc (Spec.show_cmd c) (show_res r))
      "" trace

  let agree_prop cs =
    assume (cmds_ok Spec.init_state cs);
    let sut = Spec.init_sut () in (* reset system's state *)
    let res = try Ok (Spec.wrap_cmd_seq @@ fun () -> check_disagree 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 ->
      Test.fail_reportf "  Results incompatible with model\n%s"
      @@ print_seq_trace trace

  let agree_test ~count ~name =
    Test.make ~name ~count (arb_cmds Spec.init_state) agree_prop

  let neg_agree_test ~count ~name =
    Test.make_neg ~name ~count (arb_cmds Spec.init_state) agree_prop

  end

module Make (Spec : Spec) =
  MakeExt (struct
    include SpecDefaults
    include Spec
  end)