package qcheck-stm
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=ce75e64a125c5593d8e3c91752406067
sha512=cbac110fcf490a4c71229937936eb705699489d666c55938df6ce2e31d224494a92d8dc36946e24a506f1962c23d9ac10bf1c0c2685b237e111241ee0a9049b8
doc/qcheck-stm.sequential/STM_sequential/Make/index.html
Module STM_sequential.Make
Source
Parameters
Signature
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
.
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
.
An actual agreement test (for convenience). Accepts two labeled parameters: count
is the test count and name
is the printed test name.
A negative agreement test (for convenience). Accepts two labeled parameters: count
is the test count and name
is the printed test name.