Module `STM.SpecDefaults`

Default implementations for state machine specifications that can be given useful defaults.

The intention is that extended spec modules would include the defaults:

  module MySpec = struct
    include SpecDefaults

    (* ... *)
  end

This way the spec module can usually just continue working after new specifications have been added to SpecExt with defaults in SpecDefaults.

val cleanup : 'sut -> unit

cleanup sut just returns ().

val precond : 'cmd -> 'state -> bool

precond cmd state just returns true.

val wrap_cmd_seq : (unit -> 'a) -> 'a

wrap_cmd_seq thunk is equivalent to thunk ().