Make (ortac-runtime-qcheck-stm.Ortac_runtime_qcheck_stm

Parameters

module Spec : STM.Spec

Signature

module Internal : sig ... end

val pp_program : 
  int ->
  Stdlib.Format.formatter ->
  (Report.trace list * Report.t) ->
  unit

val check_disagree : 
  (Spec.cmd -> Spec.state -> STM.res -> 'a option) ->
  (Spec.cmd -> Spec.state -> bool -> STM.res -> string) ->
  Spec.state ->
  Spec.sut ->
  Spec.cmd list ->
  (Report.trace list * 'a) option

val agree_prop : 
  int ->
  (unit -> unit) ->
  (Spec.cmd -> Spec.state -> bool -> STM.res -> string) ->
  (Spec.cmd -> Spec.state -> STM.res -> Report.t option) ->
  Spec.cmd list ->
  bool

val agree_test : 
  count:int ->
  name:string ->
  int ->
  (unit -> unit) ->
  (Spec.cmd -> Spec.state -> bool -> STM.res -> string) ->
  (Spec.cmd -> Spec.state -> STM.res -> Report.t option) ->
  QCheck.Test.t