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/qcheck-stm.sequential/STM_sequential/MakeExt/index.html

Module STM_sequential.MakeExtSource

Parameters

module Spec : STM.SpecExt

Signature

Sourceval 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.

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.

Sourceval 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.

Sourceval 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.

Sourceval 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.