stateful-check executions happen in three stages: command generation, command execution, and trace verification.
First, commands are generated. In this stage, stateful-check uses your specification to generate a sequence of actions to perform, followed by a configurable number of parallel sequences to run (which defaults to zero). These commands are generated in-line with your specification such that the :requires and :preconditions for each command are valid. See below for more information about these attributes.
Once a sequence of commands has been generated it is executed on a real system. This essentially consists of running each action in turn (i.e. the :command key), and storing its result. Note that no verification of the results is done until the execution has completed. If an exception is thrown then execution stops at that point.
Finally, the results are verified. To do this, stateful-check will invoke each of the :postcondition functions in order to verify that they all return true. In the parallel case this is more difficult, but stateful-check will check to make sure that the observed results match at least one of the expected execution orders (assuming each command is atomic).
This clear separation of stages during execution means that no functions should interact with the System Under Test (SUT) except for the :command function of each command, and the :setup and :cleanup functions of the specification. It may still be necessary to generate commands where the results of previous commands are re-used as arguments to later commands. To facilitate this stateful-check uses “symbolic values” which are replaced with real values during the execution phase.
A command is a single action which the stateful-test runner may perform on the system. It specifies the command’s expected semantics, which are then checked by random trials.
Commands have one required function:
| Key | Arguments |
:command | see optional :args function |
The :command key specifies what to do when executing this command on the SUT. The arguments to this function are determined by the :args function (specified below). This is the only function in a command specification that can interact with the SUT.
Commands have a number of optional functions:
| Key | Arguments | Default value |
:requires | [state] | (constantly true) |
The :requires key specifies a predicate that must be true in order for this command to be generated. If this function returns a falsey value then this command is not valid to generate with the provided state.
| Key | Arguments | Default value |
:args | [state] | (constantly nil) |
The :args key specifies a function from the abstract state of the system to a generator. Values generated by the generator are then used as the arguments to this function (so the generated value must be seq-able). The value returned by this function is converted into a generator with the following rules:
- objects matching
gen/generator?are left unmodified - vectors are turned into a
gen/tupleof their contents, after each if converted into a generator - maps are turned into a
gen/hash-mapwith the keys held constant, and the values are converted into generators - all other values are wrapped in
gen/return(that is: generated themselves)
During command execution, any “symbolic values” in the arguments for a command are replaced by the real value that they represent.
| Key | Arguments | Default value |
:precondition | [state args] | (constantly true) |
The :precondition is very similar to the :requires key, except that it runs after the command’s arguments have been generated, and thus can test a relationship between the state and the generated arguments. If this function returns falsey then this command is not valid to generate with the provided state and args.
| Key | Arguments | Default value |
:next-state | [state args result] | (fn [state _ _] state) |
The :next-state function denotes the effect of this command on the state. This command is called during command generation, but also during trace verification.
During command generation the result provided to this function is an abstract object used as a “symbolic value” representing the return value of the :command function. These objects do not permit introspection of the return value, but they may be added to the state and used during argument generation for other commands. See the end of this document for some more information about symbolic values.
During trace verification the result provided to this function is the value that was returned during command execution. It is important that the behaviour of the :next-state function is the same whether or not it is given a symbolic value or its real equivalent. If the :next-state function has different behaviours then it may create an inconsistent state object. To guard against this, you should not interact with the result object in any way, except those which are mentioned at the end of this document in the symbolic values section.
| Key | Arguments | Default value |
:postcondition | [prev-state next-state args result] | (constantly true) |
The :postcondition function is how test assertions are performed. This function is provided with the state before (prev-state) and after (next-state) this command’s :next-state function is called. There are two ways for a postcondition to signal success/failure:
- they can use
clojure.test/is, where a failed assertion means the command did not perform as expected on the SUT; or - if there are no
clojure.test/isassertions, then they can return a falsey value to indicate the command did not perform as expected on the SUT.
If a failure is indicated on a given command, the execution containing it is recorded as a failure. If an assertion has failed, then the expected/actual values will be printed to aid in debugging.
Everything provided to the :postcondition function is a “real” value. All symbolic values will be replaced before the :postcondition function is called.
Be aware that :postcondition functions run after the execution has completed, and thus any objects which have been mutated or otherwise changed may cause your test to fail. If you are planning to use a postcondition, ensure that your :command function returns an immutable value!
System specifications are a representation of a number of commands which can be performed on an actual system. They specify setup/cleanup operations, initial state, and any extra rules around command generation.
When running stateful-check it always expects a system specification to be provided at the top level.
(is (specification-correct? system-specification))Specifications have one required key:
| Key | Shape |
:commands | map of names to commands |
The :commands key specifies all of the commands that can be used in this specification. Each command needs a “name”, which will be used in the command output to identify which command is being run.
The values of the map may either be a command map (see above section on their structure), or they may be a var which holds a reference to a command map. If the value is a var then it will be dereferenced whenever the command is generated (this permits the var to be redefined without needing to also redefine the spec).
{:new #'new-command
:pop #'pop-command
:push #'push-command}
Specifications also have a number of optional functions:
| Key | Arguments | Default value |
:generate-command | [state] | (gen/elements (:keys system-specification)) |
The :generate-command function is used to determine which command to add to the command list next. The generator returned by :generate-command is used to generate the name of the next command (which then goes through ordinary command generation).
In general, if your commands are set up appropriately then you will not need to declare a :generate-command function. It can be helpful for changing the distribution of generated commands, or for increasing the efficiency of generation in some cases.
| Key | Arguments | Default value |
:setup | none | nil |
:cleanup | [setup] or none | nil |
The :setup function is run prior to the real execution phase. It should perform any one-time setup tasks which are necessary to prepare the SUT.
The :cleanup function is run immediately after the real execution phase. It is always run (irrespective of the pass/fail state of the test) and should clean up any necessary resources. If you have declared a :setup function, then :cleanup will be called with its return value as an argument. If you have not declared a :setup function then :cleanup will be called with no arguments.
| Key | Arguments | Default value |
:initial-state | none or [setup] | (constantly nil) |
The :initial-state function is used to seed the state value, which is then used extensively throughout command generation and execution.
If a :setup function has been provided then the :initial-state function will be passed a symbolic value representing the result of the setup. During execution the symbolic value will be replaced with the value that :setup returned for that execution.
Symbolic values are used during the abstract model phase in order to represent the results of real executions of commands. When they are used as the arguments to a command they are replaced by their concrete values.
The only operation permitted on symbolic values is to lookup a key within them. During the real execution phase the corresponding key will be looked up in the concrete value (so (:key symbolic-value) will, during real execution, be replaced with (:key concrete-value)).