net.jeffhui.check.statem — net.jeffhui/check.statem 1.0.0-SNAPSHOT

Facilities for testing stateful systems using state machines.

Allows defining specially annotated state machines that can be used as the basis for generating test verification programs to validate stateful specifications.

Test verification programs are defined as a sequence of transitions that conform to a state machine.

API OVERVIEW

The goal for state machine testing is to define the following:

• A 'model' state machine (using defstatem). The model state machine defines the expected state machine behavior.
• A interpreter function (adapter between defstatem and an implementation). This function reads model state transitions and performs the appropriate behavior in an implementation.

The most important functions you need to understand are:

• defstatem for defining state machines.
• cmd-seq for generating symbolic test programs from a state machine.
• run-cmds for executing a symbolic test program against code that needs to be verified. This is to compare the state machine behavior to a real implementation.

There are some useful helper functions that aid in building & debugging state machines:

• check! run some sanity checks against the state machine definition.
• run-cmds-debug is a verbose printout version of run-cmds.
• select-by-frequency allows you to skew how cmd-seq generates commands.
• print-failed-runs! prints commands if a particular run-cmds call fails.

always clj macro

(always body)

(always n body)

Repeats a body that returns any [[clojure.test.check.results/Result]] conforming value up to n times. Returns the first failing result encountered.

This is useful to verify that asynchronous / concurrent behavior doesn't cause any flakey behavior.

Parameters

key	required?	expected type	description
body	required	expression	The form to execute that returns a Result value (eg - run-cmds)
n	optional	positive integer	The number of times to repeatedly run a property to see if it failed.

Notes:

Papers from the Erlang QuickCheck implementation mention n=10 is a 'practically good enough' value. Lower values of n risk not finding flaky behavior, but higher values of n will require more executions (and take more time to complete).

Example:

(always (run-cmds statem cmds interpreter))

always-fn clj

(always-fn f)

(always-fn n f)

Function form of always macro. See the macro for more details.

Parameters

key	required?	expected type	description
f	required	(fn [] ...)	The function to execute that returns a Result value (eg - run-cmds)
n	optional	positive integer	The number of times to repeatedly run a property to see if it failed.

catch-interpreter clj

(catch-interpreter interpreter)

Wraps an interpreter function that provides try-catch error behavior that run-cmds expects.

Using this decorator is equivalent to passing {:catch? true} to run-cmds-debug.

catch-print-interpreter clj

(catch-print-interpreter interpreter)

Like catch-interpreter, but prints to stdout

Using this decorator is equivalent to passing {:catch? true} to run-cmds.

check! clj

(check! statem)

Performs validations against state machine. Useful for sanity-checking state machine definitions before attempting to use them.

This will never run verify methods of state machine commands. But this does generate command sequences.

cmd-seq clj

(cmd-seq statem)

(cmd-seq statem
         {:keys [select-generator size initial-state]
          :or {select-generator select-by-any}
          :as options})

A generator that produces a random sequence of commands that conform to a given state machine. Shrinking removes commands from the sequence while still conforming to the state machine.

Parameters

key	required?	expected type	description
statem	required	StateMachine	The state machine that the sequence of commands must conform to.
select-generator	optional	(fn [state statem m] ...)	A function that accepts a map of {:command-kw command-impl} where only commands valid for the state machine is in m. state is the current stored state of the state machine and statem is the given state machine. The function is expected to return a generator that picks one of the command-impls. (Default select-by-any).
size	optional	non-negative integer	The number of commands to generate for any particular program. The default relies on test.check's natural sizing behavior.
initial-state	optional	anything StateMachine accepts as model state	The initial state when the state machine starts. Should be the same as the one given to run-cmds.

Example

(defn queue-interpreter [cmd run-cmd-ctx] ...)

(for-all [cmds (cmd-seq queue-statem)]
  (:pass? (run-cmds queue-statem cmds queue-interpreter)))

For a more thorough example, check out run-cmds.

Generated Values

An opaque value to pass to run-cmds. The structure may change in the SNAPSHOT versions.

Technically, returns a sequence of commands are in single-assignment statement form:

[
  [:set [:var 1] ...]
  [:set [:var 2] ...]
  [:set [:var 3] ...]
  ...
]

Where [:var N] is a return value from running a given statement. This is abstract representation akin to this in Clojure:

(do
  (def var1 ...)
  (def var2 ...)
  (def var3 ...)
  ...)

The data structure returned is a format that is intended:

• To be somewhat human readable (since test.check prints this)
• To have enough information in each statement for an interpreter function to operate
• To be pure data to allow them to be stored as regression test cases
• To be fast at generating. State machine generation can be slow for large state machines.

SNAPSHOT limitations:

The last reason is why the format should be considered opaque. It may be useful for inspecting, but it should be considered 'no warranty' behavior for depending on this result, say in a library.

Command clj protocol

Command interface. NOTE: It's recommended to use defstatem and/or defcommand instead of implementing this protocol directly. Advanced-usage only.

Command (aka - State Transition) represents an 'action' or transition that can be taken by a state machine. These transitions requires several bits of metadata:

1. When is calling this command valid?
2. What data does this command require besides the current state?
3. How does the state machine's state change invoking this command?
4. How do we validate this command's behavior to another implementation?

The following functions map to the following questions:

• assume and only-when answers #1, with the first being an optimization of the latter.
• args answers #2
• advance answers #3
• verify answers #4

If you're implementing these functions from defstatem is that the first two arguments (_ and model-state) are assumed for brevity.

advance clj

(advance _ model-state return-sym args)

Returns next model state from the given model state and its arguments. Should be free of side effects.

args clj

(args _ model-state)

Returns a vector generator to use as input arguments for the command and subsequent protocol functions below. The first argument of the vector must be the command's keyword (eg - (gen/return :add)).

Should be free of side effects.

assume clj

(assume _ model-state)

Return true to indicate that this command can be executed based on the current model state. Should be free of side effects.

kind clj

(kind _)

Returns a constant value of representing the type of transition this. Currently can be :observed or :conjectured.

• :observed commands are traditional transitions that are invocable / observable actions taken
• :conjectured commands are transitions that are implied when another transition occurrs. Conjectured commands are useful when modeling asynchronous background operations.

only-when clj

(only-when _ model-state args)

Return true to indicate that this command can be executed based on the current model and generated arg data. Should be free of side effects.

verify clj

(verify _ model-state previous-model-state args return-value)

Asserts if the command is valid after state application. Should be free of side effects.

DebuggableCommand clj protocol

An extension to Command protocol that allows a command to provide debug information.

verify-debug clj

(verify-debug _ model-state previous-model-state args return-value)

Called when verify of Command returns false. Allows returning a data structure for debugging.

Useful to return model-state information related to verify.

Return :net.jeffhui.check.statem/no-debug to indicate no debugging information. (Default for defstatem/defcommand macros).

Note: remember that debugging information already includes return-value. So it's typically not useful to return it as well.

defcommand clj macro

(defcommand table-name
            cmd-name
            [model-state this :as shared-bindings]
            &
            methods)

Provides an simplified way to define commands for the statem.

You probably want to use defstatem instead of this macro directly. defcommand allows you to structure your state machine more like multimethods.

Simply is sugar for (alter-var-root state-machine assoc-in ... (reify Command ...)) to save typing and some boilerplate in the following ways:

• all methods imply model-state and this via the 3rd argument
• args's body will wrap (gen/tuple (gen/return command-name-kw) ...)
• all methods have default implementations if not specified:
  • kind returns :observed
  • assume returns true
  • only-when returns true
  • advance returns model-state it was given
  • args returns nil. AKA: (gen/tuple (gen/return command-name-kw))
  • verify returns true

Example

(defstatem set-statem)

(defcommand set-statem :add [mstate]
  (args [] [gen/integer])
  (advance [_ [_ value]] (conj (set mstate) value)))

(defcommand set-statem :has [mstate]
  (args [] [gen/integer])
  (verify [_ [_ value]] (contains? (mstate) value)))

defstatem clj macro

(defstatem table-name & commands)

Declares a state machine for building test verification programs.

This macro provides syntactic sugar to creating a map that represents a state machine with Commands.

If you have a large state machine, you can break the state machine definition into several forms by using defcommand directly. Although, it may be more indicative of a bigger problem if your state machine has a lot of commands (since test.check may not be able to generate a large part of the state machine's program space on any given run.)

Example:

(defstatem queue-statem
  "A basic queue state machine"
  [mstate this]  ; -> state machine's model state is available in all commands

  ;; define commands for the state machine
  (:enqueue (args [] gen/any-printable)
            (advance [return-sym [cmd-name item]] ((fnil conj []) mstate item))
            (verify [prev-mstate [cmd-name item] ret] ret))

  (:dequeue (assume [] (pos? (count mstate)))
            (advance [_ _] (subvec mstate 1))
            (verify [_ _ return-value] (= return-value (first mstate)))))

Implied parameters

Implied parameters are like defrecord fields - parameters that exist in every method body. For conciseness, this is defined once instead of having to repeat it for every command. Otherwise state machine definitions would look like:

;; NOTE: invalid code, do not use
(defstatem queue-statem
  (:enqueue (assume [this model-state])
            (args [this model-state])
            (only-when [this model-state cmd-data])
            (advance [this model-state ret-sym cmd-data])
            (verify [this model-state prev-mstate cmd-data return-value])))

Here's the following implied parameters:

• model-state is the model state that is used for all commands.
• this represents the command itself. Can be optionally elided.

Command Methods

(assume [] ...)

Return true if this command can be used for a given the model state. If you depend on generated data, use only-when instead. Although using this method aids in faster program generation.

Default implementation returns true. Implementation must be free of side effects.

(args [] ...)

Return a vector of generators of data needed to execute this command. Subsequent functions will receive the generated data as cmd-data. The generated data is prefixed with the keyword of the command name.

Default implementation returns nil. Implementation must be free of side effects.

Example

(args [] [gen/int]) ;; => [:command-name 1]

(only-when [cmd-data] ...)

Return true if this command can be used for a given model state or generated command data.

Default implementation calls through to assume. Implementation must be free of side effects.

Parameters

argument	description
model-state	The model state that is used for all commands. See 'Implied parameters' section above.
cmd-data	refers to the generated command data from args.

(advance [ret-sym cmd-data] ...)

Return the next model state from executing this command. ret-sym represents the symbolic value of the return value of from calling subject-under-test (but not yet realized).

Default implementation returns mstate. Implemetation must be free of side effects.

Parameters

argument	description
model-state	The model state that is used for all commands. See 'Implied parameters' section above.
ret-sym	A symbolic representation of the subject under test's return value. This may be useful to reference usage of a return value for testing / interpreter usage.
cmd-data	The generated command data from args.

(verify [prev-mstate cmd-data return-value] ...)

Verifies the state machine against the subject under test. Returns true if the subject under test returned the correct value (aka - passed an assertion).

Default implementation returns true. Implementation must be free of side effects.

Parameters

argument	description
model-state	The model state that is used for all commands. See 'Implied parameters' section above.
prev-mstate	The model state prior to advance.
cmd-data	The generated command data frmo args.
return-value	The actual value the subject under test returned when running.

Notes

State machine definitions are entirely abstract - meaning there is no external side effects that a production implementation may have. To perform that comparison, use a function like run-cmds with some integration code. This allows state machine definitions to be shared or reused against other production implementations.

Other details of this macro:

• args's body will wrap (gen/tuple (gen/return command-name-kw) ...)
• all methods have default implementations if not specified
  • assume returns true
  • args returns nil. AKA: (gen/tuple (gen/return command-name-kw))
  • only-when returns true
  • advance returns model-state it was given
  • verify returns true

Large State Machines

If you have a large state machine, it may be better to break it up into multiple smaller ones to test. Smaller state machines allow test.check to generate more of the possible program space within a typical test generation (100 commands is test.checks' default size maximum).

Alternatively, you can choose to generate commands with a skewed probability of generating specific events. It's probably not as good of a solution to breaking up the state machine, but can provide a more focused exploration of specific kinds of program generations.

ExecutionResult clj

HistoryEntry clj

interpreter-with-cleanup clj

(interpreter-with-cleanup interpreter-fn cleanup-fn)

Adds metadata to an interpreter function to allow cleanup code to run after a test run finishes.

This allows an interpreter to clean up any resources created during the test run by accessing the var-table of the run - such as closing open files.

list-commands clj

(list-commands statem)

Returns a sequence of keywords indicating available command names for the state machine.

Example

(list-commands queue-statem)
;; => [:new :enqueue :dequeue]

list-commands-by clj

(list-commands-by statem k)

Returns a sequence of keywords indicates available command names for the given state machine that match a given kind.

Example

  (list-commands-by queue-statem :observable)
  ;; => [:new :enqueue :dequeue]
  (list-commands-by queue-statem :conjectured)
  ;; => []

lookup-command clj

(lookup-command statem command-name)

(lookup-command statem command-name default-value)

Returns a command that that matches a given interface. Throws if the command does not exist unless a default value is given.

Example

(lookup-command queue-statem :new)
;; => <instance conforming to Command>

print-failed-runs! clj

(print-failed-runs! execution-result)

(print-failed-runs! {:keys [mstate? max-size] :or {mstate? false max-size 10}}
                    execution-result)

A helper function thar prints execution results if a run has failed. Useful to scan and see all failing tests. For convinence, only prints small, failing executions by default.

Returns the execution result given.

If you're looking to do something else on failure, see the when-failed! macro.

Parameters

• max-size (optional, integer) If set, only prints history sizes less than or equal to this max size. Defaults to 10. Setting this to nil will print any sized failure.
• mstate? (optional, boolean) If true, prints the model state for each executed command. Defaults to false.
• execution-result (required, ExecutionResult) The execution result produced by run-cmds.

Examples

(print-failed-runs! (run-cmd statem cmds interpreter))
(print-failed-runs! {:mstate? true} (run-cmd statem cmds interpreter))

run-cmds clj

(run-cmds statem cmds interpreter)

(run-cmds statem
          cmds
          interpreter
          {:keys [initial-state catch?] :or {catch? true}})

Executes the symbolic representation of a sequence of commands using an interpreter.

Returns

An ExecutionResult record. Always returns a map with a key :pass? to indicate if the test program succeeded or failed. Alternatively, you can use clojure.test.check.results/pass? to resolve to true. This means simply returning this value to for-all will work as expected (by checking :pass?).

ExecutionResult contains the execution history that can be useful for debugging. See when-failed! macro for example usage.

Parameters

key	required?	expected type	description
statem	required	StateMachine	The state machine needed to verify behavior against.
cmds	required	seq of symbolic commands	The sequence of commands to execute against the subject under test. This should be generated from cmd-seq.
intepreter	required	(fn [cmd ctx] ...)	The interface to interacting with the subject under test. See 'Interpreter'section below.
initial-state	optional	anything valid for StateMachine's model state	The initial state machine state. Should be the same as the one given to cmd-seq.
catch?	optional	boolean	Should this runner attempt to catch exceptions? Catching exceptions allows the runner to minimize the failure, but may lose the original stacktrace. (Default true)

Interpreter

  :: (fn interpreter [cmd run-cmds-ctx])
    where
      cmd          :: [cmd-type & generated-cmd-args]
      run-cmds-ctx :: {:keys [var-table]}
      var-table    :: {VariableSymbol value}

Interpreter receives every command to execute and is expected to run against the subject under test. The return value of interpreter is the return-value used in the state machine's verify method.

This function bridges the model state machine with a concrete implementation. Having this interpreter function also keeps the model state machines free from directly comparing to a specific imlementation.

var-table is a map of symbolic variables to concrete values. A symboli value is in the form [:var N] in the command generation value:

[[:set [:var 1] [:upload "foo"]]
;;     ^^^^^^^^ this
 [:set [:var 2] [:result [:var 1]]]]
;;     ^^^^^^^^ and this

This allows the state machine and interpreter to hold/refer to stateful references to from previous statements.

For the state machine side, look at [[advance]] to see ret-sym, which is the symbolic reference to the return value of the command after execution.

Example

;; elided: TestQueue implementation
(defn queue-runner [cmd {:keys [varsym var-table]}]
  (case (first cmd)
    :new     (TestQueue. [] (second cmd))
    :enqueue (.enqueue ^IQueue (var-table (second cmd)) (nth cmd 2))
    :deque   (.dequeue ^IQueue (var-table (second cmd)))))

(defstatem queue-statem
  [mstate]
  (:new (assume [] (nil? mstate))
        (args [] [gen/pos-int])
        (advance [v [_ n]] {:items    []
                            :capacity n
                            :ref      v}))
  (:enqueue (assume [] (and (not (nil? mstate))
                            (< (count (mstate :items)) (mstate :capacity))))
            (args [] [(gen/return (:ref mstate)) gen/int])
            (advance [v [_ _ n]] (update mstate :items conj n)))
  (:deque (assume [] (and (not (nil? mstate))
                          (pos? (count (mstate :items)))))
          (advance [_ _] (update mstate :items subvec 1))
          (args [] [(gen/return (:ref mstate))])
          (verify [_ _ r] (= r (first (:items mstate))))))

(for-all [cmds (cmd-seq queue-statem)]
          (run-cmds queue-statem cmds queue-interpreter))

run-cmds-debug clj

(run-cmds-debug statem cmds interpreter)

(run-cmds-debug
  statem
  cmds
  interpreter
  {:keys [initial-state mstate? return-value? catch? debug-method]
   :or {return-value? true catch? true mstate? true debug-method :print}})

Identical to run-cmds, but prints out data related to each command executed.

Because of the debugging instrumentation, this executes commands more slowly than run-cmds. This function is typically more useful if you're diagnosing why one particular sequence of commands is hanging.

Parameters

• statem (required, StateMachine) The state machine needed to verify behavior against.

• cmds (required, seq of symbolic commands) The sequence of commands to execute against the subject under test.

• interpreter (required, fn[2-args]) The interface to interacting with the subject under test. See 'Interpreter' section below.

• inital-state (optional, anything valid for StateMachine's model state) The initial state machine state. Should be the same as the one given to cmd-seq.

• mstate? (optional, bool) If true, print out the model state after each command. Defaults to true.

• return-value? (optional, bool) If true, print out the return value for verify after each command. Defaults to true.

• catch? (optional, bool) Should this runner attempt to catch exceptions? Catching exceptions allows the runner to minimize the failure, but may lose the original stacktrace. Defaults to true.

• debug-method (optional, keyword) How should debug information be emitted? Default is :print which prints to stdout. Supported methods:

  - `:print` Prints data to stdout. Default value.
  - `:print-short` Prints data to stdout in compact form. Ignores `:mstate?` option.
  - `:inspect` Emits data to clojure.inspector/inspect.
  - `:inspect-tree` Emits data to clojure.inspector/inspect-tree
  - `:inspect-table` Emits data to clojure.inspector/inspect-tabl
  

  Note that inspect debug methods create windows per run-cmds-debug invocation, so using those methods inside a property may cause many windows to be created.

select-by-any clj

A helper that simply returns a generator that picks commands randomly.

Note

Based on how cmd-seq works, this frequency is affected by the constraints which the command can be valid as defined by the state machine.

Example

(cmd-seq statem {:select-generator select-by-any})

select-by-frequency clj

(select-by-frequency cmd-kw->count)

A helper that simply returns a generator that picks commands based on a probability map of the command keyword name to its likelihood.

The likelihood is determined by taking the value divided by the sum of all likelihoods.

Note

Based on how cmd-seq works, this frequency is affected by the constraints which the command can be valid as defined by the state machine.

Example

(cmd-seq statem {:select-generator (select-by-frequency {:new    1000
                                                         :add    100
                                                         :remove 10})})

sometimes clj macro

(sometimes body)

(sometimes n body)

Repeats a body that returns any [[clojure.test.check.results/Result]] conforming value up to n times. Returns failure if only every try also fails.

This is useful to verify that asynchronous / concurrent behavior that you want to shrink to a reliably reproducable failure.

Parameters

key	required?	expected type	description
body	required	expression	The form to execute that returns a Result value (eg - run-cmds)
n	optional	positive integer	The number of times to repeatedly run a property to see if it always fails.

Example

(sometimes (run-cmds statem cmds interpreter))

sometimes-fn clj

(sometimes-fn f)

(sometimes-fn n f)

Function form of sometimes macro. See the macro for more details.

StateMachine clj

str-history-entry clj

(str-history-entry v)

Returns a print-friendly output of a history entry

valid-cmd-seq? clj

(valid-cmd-seq? statem cmds)

(valid-cmd-seq? statem cmds {:keys [initial-state]})

Returns true if a sequence of commands conforms to a state machine's requirements.

Example

;; for all of correct definitions of `queue-statem`, this should always pass
(for-all [cmds (cmd-seq queue-statem)]
        (valid-cmd-seq? queue-statem cmd))

when-failed! clj macro

(when-failed! execution-result bindings & body)

Executes a given body when a execution fails. Useful for printing debugging information.

You may prefer print-failed-runs! if you want something quick to print out on failure.

Shorthand, for:

(let [result ~execution-result]
  (when-not (clojure.test.check.results/pass? result)
    (let [~bindings [(:history result) (:cmds result)]]
      ~@body)))

This useful for debugging failures.

Example

(for-all [cmd (cmd-seq queue-statem)]
  (when-failed! (run-cmds queue-statem cmds interpreter)
    [history cmds]
    (println "FAILED")
    (doseq [entry history]
      (println " " (str-history-entry entry)))))