Parameter MakeExt.Spec

include STM.SpecExt
type cmd
type state
type sut
val arb_cmd : state -> cmd QCheck.arbitrary
val init_state : state
val show_cmd : cmd -> string
val next_state : cmd -> state -> state
val init_sut : unit -> sut
val cleanup : sut -> unit
val precond : cmd -> state -> bool
val run : cmd -> sut -> STM.res
val postcond : cmd -> state -> STM.res -> bool
val wrap_cmd_seq : (unit -> 'a) -> 'a
val arb_cmd_seq : state -> cmd QCheck.arbitrary
val arb_cmd_dom0 : state -> cmd QCheck.arbitrary
val arb_cmd_dom1 : state -> cmd QCheck.arbitrary