package ortac-runtime-qcheck-stm

You can search for identifiers within the package.

in-package search v0.2.0

ortac-runtime-qcheck-stm
- Ortac_runtime_qcheck_stm
  - Make
    
    Internal
  - Model
    
    Make
    
    M
  - SUT
    
    Make
    
    M

Legend:
Library
Module
Module type
Parameter
Class
Class type

val cmds_ok : Spec.state -> Spec.cmd list -> bool

val arb_cmds : Spec.state -> Spec.cmd list QCheck.arbitrary

val consistency_test : count:int -> name:string -> QCheck.Test.t

val interp_agree : Spec.state -> Spec.sut -> Spec.cmd list -> bool

val check_disagree : 
  Spec.state ->
  Spec.sut ->
  Spec.cmd list ->
  (Spec.cmd * STM.res) list option

val check_obs : 
  (Spec.cmd * STM.res) list ->
  (Spec.cmd * STM.res) list ->
  (Spec.cmd * STM.res) list ->
  Spec.state ->
  bool

val gen_cmds_size : 
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  Spec.state ->
  int QCheck.Gen.t ->
  Spec.cmd list QCheck.Gen.t

val arb_cmds_triple : 
  int ->
  int ->
  (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary

val all_interleavings_ok : 
  Spec.cmd list ->
  Spec.cmd list ->
  Spec.cmd list ->
  Spec.state ->
  bool

val shrink_triple : 
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.Shrink.t

val arb_triple : 
  int ->
  int ->
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.state -> Spec.cmd QCheck.arbitrary) ->
  (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary