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
|
(** Module for building sequential STM tests *)
module Make : functor (Spec : STM.Spec) ->
sig
val cmds_ok : Spec.state -> Spec.cmd list -> bool
(** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
Accepts the initial state and the command sequence as parameters.
[cmds_ok] catches and ignores exceptions arising from {!next_state}. *)
val arb_cmds : Spec.state -> Spec.cmd list QCheck.arbitrary
(** A generator of {!Spec.cmd} sequences. Accepts the initial state as a parameter.
[arb_cmds] catches and ignores generation-time exceptions arising from
{!Spec.next_state}. *)
val agree_prop : Spec.cmd list -> bool
(** The agreement property: the command sequence [cs] yields the same observations
when interpreted from the model's initial state and the [sut]'s initial state.
Cleans up after itself by calling {!Spec.cleanup}. *)
val agree_test : count:int -> name:string -> QCheck.Test.t
(** An actual agreement test (for convenience). Accepts two labeled parameters:
[count] is the test count and [name] is the printed test name. *)
val neg_agree_test : count:int -> name:string -> QCheck.Test.t
(** A negative agreement test (for convenience). Accepts two labeled parameters:
[count] is the test count and [name] is the printed test name. *)
end
module MakeExt : functor (Spec : STM.SpecExt) ->
module type of Make (Spec)
|
