package qcheck-stm

  1. Overview
  2. Docs
State-machine testing library for sequential and parallel model-based tests

Install 

dune-project
 Dependency

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

Authors

  1. J
    Jan Midtgaard
  2. O
    Olivier Nicole
  3. N
    Nicolas Osborne
  4. S
    Samuel Hym

Maintainers

  1. J
    Jan Midtgaard <mail@janmidtgaard.dk>

Sources

0.10.tar.gz
md5=ed5980f1cfbfa1e2d2ec5a87954dddf8
sha512=90c451903adb7cbd83aa0f2ad7738d662edc23affb669ed762564cdb2e140ca931afeaabc199fbb6028163fc41c17049961bef7fd2664c677cb1df552d10736d

doc/src/qcheck-stm.sequential/STM_sequential.ml.html

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)