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.