Copyright © Quviq AB, 2004-2015
Version: 1.36.1
This module provides functions for testing operations with side-effects, which are specified via an abstract state machine. The state machine is in turn specified by a client module (which implements the callbacks for eqc_statem). Given such a client, this module can generate and run command sequences, checking that all postconditions are satisfied, and shrinking failing sequences by discarding commands which do not contribute to the failure. Thus it can be used to find minimal command sequences which elicit an unexpected behaviour.
It can also generate parallel test cases from the same client module, which are used to test for race conditions.
Modules which use this one should -include_lib("eqc/include/eqc_statem") to import the functions that eqc_statem provides.
Since release 1.35 of QuickCheck, the documentation of this module has been updated to the grouped style of writing callbacks. In case you are confronted with a legacy state machine model that you need to understand, please read the old documentation.
command()
), each
of which binds a symbolic variable to the result of a symbolic function call (except,
possibly, for a first command which initializes the state, see below).
For example,
{set,{var,1},{call,erlang,whereis,[a]}}is a command to set variable 1 to the result of calling erlang:whereis(a). The command generator is specified by COMMAND_command/1. QuickCheck recognizes a set of suffices, such as _command to enable compact model notations. For the above symbolic call, one would write the generator:
whereis_command(_S) -> {call, erlang, whereis, [elements([a, b, c, d])]}.Alternatively, one only specifies the argument generator, which in practice works best, and write a wrapper for the function under test, for example:
register_args(S) -> [elements([a, b, c, d]), pid(S)]. register(Name, Pid) -> catch erlang:register(Name, Pid).When a test case is run, then symbolic variables (
var()
) are replaced
by the values they were set to, and symbolic calls (call()
) are
performed. In addition, the post-condition of each command is checked. Running
a list of commands generates a result which indicates whether
any post-condition failed, or any command raised an exception, or whether all
commands and checks completed successfully.
It is very important to keep in mind the difference between symbolic calls and variables, which are used during test case generation, and the values they represent, which are computed during test execution. We refer to the latter as dynamic values. The reason we use symbolic representations (rather than just working with their dynamic values) is to enable us to display, save, analyze, and above all simplify test cases before they are run.
[{var,1},{var,2},{var,3}]if the first three commands all spawned processes. The model for spawning process needs to update the state, for which the _next suffix is used: to compute the nest model state.
spawn_args(_S) -> []. spawn() -> erlang:spawn(timer, sleep, [5000]). spawn_next(S, Res, []) -> S#state{pids = S#state.pids ++ [Res]}.During test execution the corresponding dynamic state is computed--in this case a list of three pids returned by the first three commands in the test case. Dynamic states always have the same structure as the corresponding symbolic states--the difference is just that symbolic variables and calls are replaced by their values.
Symbolic states are used to generate symbolic commands, or to decide whether a given symbolic command can be included in a test case. Dynamic states are used to check postconditions.
It is not usually necessary to track all relevant state information in the test case state--there is no need to include more information in the state than is necessary to generate and execute the command sequences we are interested in.
symbolic_state()
.
Returns the state in which each test case starts (unless a different initial state is supplied explicitly). This symbolic state is evaluated to construct the initial dynamic state before each test case is executed.
The following call-back suffixes are provided for eqc_statem.
symbolic_state()
) :: bool()
Returns true if the command COMMAND may be generated in state S. The precondition is also used when shrinking to make sure that invalid commands do not pop-up in a test case while shrinking.
default: truesymbolic_state()
, Args::[term()]) :: bool()
Returns true if the symbolic call {call,_,COMMAND,Args} can be performed in the state S. The precondition is also used when shrinking to make sure that invalid commands do not pop-up in a test case while shrinking.
default: true
Preconditions are used to decide whether or not to include candidate commands in test cases, which is why only the symbolic state information is available when preconditions are checked.
symbolic_state()
, Args::[term()], MetaData::[proplists:property()]) :: bool()
Returns true if the symbolic call {call,_,COMMAND,Args} can be performed in the state S and with the given MetaData. The precondition is also used when shrinking to make sure that invalid commands do not pop-up in a test case while shrinking.
default: true
Note: You may only use either COMMAND_pre/2 or COMMAND_pre/3, not both! The use of MetaData is advanced and we recommend the usage of it to experts only.symbolic_state()
, Args::[term()]) :: false | gen(call()
)
This is an optional call-back used during shrinking; when a precondition does not hold, adapt is called to try to repair/patch a call before it is discarded. Typically metadata in the call tuple can be adjusted. After adapt is finished, the precondition is checked again to see whether the changes were sufficient.
default: falsesymbolic_state()
) :: gen([term()])
Generates appropriate arguments for the function under test. The result are arguments Args that are used in the symbolic call
{call,?MODULE,COMMAND,Args}in the test case generator, given that COMMAND_pre(S) returns true for the symbolic state S at generation time.
symbolic_state()
) :: gen(call()
)
Generates an appropriate call for the function under test. The result is a symbolic call used in the test case generator, given that COMMAND_pre(S) returns true for the symbolic state S at generation time.
This is the function that is called during test case execution.
symbolic_state()
, V::var()
, Args::[term()]) :: symbolic_state()
This is the state transition function of the abstract state machine, and it is used during both test generation and test execution. The type above refers to calls during test generation.
In this case, it computes the symbolic state after symbolic call {call,_,COMMAND,Args}, performed in symbolic state S, with result V. Because it is applied to symbolic states and symbolic calls, the result of the call must also be symbolic-- in fact, V is the symbolic variable which will be set to the result of the call.
For example, if the state were a list of pids, and COMMAND applied to Args spawned a new process, then the variable V could be added to the state to refer to the pid of the process just spawned. Symbolic function calls can also be included in the next state, to construct parts whose values will only be known during test execution.
The same function is used to compute the next dynamic state during test execution. In this case S is the previous dynamic state, and Args are the actual values passed (not symbolic argument expressions), and V is the actual value returned--in other words, all the symbolic inputs are replaced by their values. A correctly written COMMAND_next function does not inspect symbolic inputs--it just includes them as symbolic parts of the result. Thus the same code can construct a dynamic state of the same shape, given actual values instead of symbolic ones. The only difficulty is that COMMAND_next may itself introduce symbolic function calls into its result, which would then be a kind of mixture of a symbolic and dynamic state. To ensure that the state remains dynamic during test execution, any such symbolic calls are performed, and replaced by their values, before test execution continues.
default: S, i.e., leave state unchanged
COMMAND_next(S::symbolic_state()
, V::var()
, Args::[term()], MetaData::[proplists:property()]) :: symbolic_state()
As _next/3, but also taking MetaData into account.
Note: You may only use either COMMAND_next/3 or COMMAND_next/4, not both!dynamic_state()
, Args::[term()], R::term()) :: bool()
Checks the postcondition of symbolic call {call,_,COMMAND,Args}, executed in dynamic state S, with result R.
default: trueOf course, postconditions are checked during test execution, not test generation.
dynamic_state()
, Args::[term()], R::term(), MetaData::[proplists:property()]) :: bool()
Checks the postcondition of symbolic call {call,_,COMMAND,Args}, executed in dynamic state S, with result R, having metadata MetaData.
default: true
Note: You may only use either COMMAND_post/3 or COMMAND_post/4, not both!
An important special case is checking that the result of COMMAND matches the expected return value. If COMMAND_return is specified this is done by:COMMAND_post(S, Args, Res) -> eq(Res, COMMAND_return(S, Args)).
symbolic_state()
, Args::[term()]) :: term()
This is an optional callback that computes the expected return value from the model state. This return value can be used in simulation mode, or when clustering a state machine with a component. It is often good practice to check the return value in the postcondition by explicitely calling this return callback to check whether the actual returned value is equivalent with the return value computed by this function using the model state.
The return function can be an over specification, not leaving enough implementation freedom. In those cases it is preferred to use a general postcondition, which might check that the returned value is in a certain range or of a certain form.
COMMAND_return(S::symbolic_state()
, Args::[term()], MetaData::[proplists:property()]) :: term()
As _return/2, but also taking MetaData into account.
Note: You may only use either COMMAND_return/2 or COMMAND_return/3, not both!dynamic_state()
, Args::[term()], R::term()) :: list(any())
Collects a list of features of the symbolic call {call,_,COMMAND,Args}, executed in dynamic
state S, with result R.
The arguments of the symbolic call are the
actual values passed, not any symbolic expressions from which they were computed.
The features can be recovered later using call_features/1
.
Features are collected during test execution, not test generation.
dynamic_state()
, Args::[term()]) :: bool()
This is an optional call-back which can be used to check a precondition during test execution. Its argument is a dynamic state, and a call with the actual argument values (even for calls which are generated with symbolic arguments). If it returns false, then the command is not executed during the test. Dynamic preconditions may be easier to write than the normal preconditions, because they need not work with symbolic values. However, they have significant disadvantages:
parallel_commands/1
is not possible.
For these reasons, it is almost always better to enrich the model state so that a static precondition can be defined, than to use a dynamic one. In rare cases, and especially when the dynamic precondition will usually be true, then using this call-back can be the best approach.
default: true
COMMAND_dynamicpre(S::dynamic_state()
, Args::[term()], MetaData::[proplists:property()]) :: bool()
As _dynamicpre/2, but also taking MetaData into account.
Note: You may only use either COMMAND_dynamicpre/2 or COMMAND_dynamicpre/3, not both!dynamic_state()
, Cmd :: atom()) :: bool()
This is an optional callback which specifies the distribution with which commands are generated. Commands are normally generated with a the oneof generator unless a weight function is provided. In this case the weight computed from the symbolic state S is used as frequency in the frequency generator (used instead of oneof).
dynamic_state()
) :: bool()
This is an optional callback which can be used to check an invariant during test execution. It is called at the beginning of each command sequence with the initial state as argument, and then after each command is executed with the resulting state as argument. Its argument is always a dynamic state; it is not used during test case generation. If invariant returns anything other than true, the test fails. Its intended use is to compare the model state S with the actual state of the system under test.
If invariant is not defined by the user, then it is assumed to be true.
precondition_common(S::symbolic_state()
, Call::[call()]) :: bool()
Used to specify a general precondition. This precondition is applied after command generation, but before the specific (COMMAND_pre/2 or COMMAND_pre/3) is applied. Thus in COMMAND_pre/2 (or COMMAND_pre/3) one may assume that the general precondition holds.
command_precondition_common(S::dynamic_state()
, COMMAND :: atom()) :: bool()
command_precondition_common(S, Cmd) -> S /= uninitialized orelse Cmd == init.This precondition ensures that unless the state is not uninitialized the command must be init.
postcondition_common(S::symbolic_state()
, Call::[call()], Res::term()) :: bool()
eqc_component
is to check that all return values follow what we expect:
postcondition_common(S, Call, Res) -> eq(Res, return_value(S, Call)).
call_features_common(S::symbolic_state()
, Call::[call()], Res::term()) :: bool()
prop_statem_correct() -> ?FORALL(Cmds,commands(client), begin {H,S,Res} = run_commands(client,Cmds), pretty_commands(client, Cmds, {H, S, Res}, Res == ok). end).
However, in any particular case we may wish to add a little to this basic form, for example to collect statistics, to clean up after test execution, or to print more information in the event of failure. It is to allow this flexibility that the properties to test are placed in the client module, rather than in this one.
parallel_commands/1
instead of commands/1
. Instead of just one list of commands,
a parallel test case consists of a sequential prefix, followed by a
list of concurrent tasks. The prefix and each task are lists
of commands, just like a sequential test case. A parallel test case
is run using run_parallel_commands/2
, by first executing the
prefix in the normal way, then executing the concurrent tasks in
newly spawned processes. The test passes if every command behaves
atomically--that is, if the results we actually see could
have been produced by some serialization of the concurrent
tasks.
Blocking operations can be specified using the optional callback:
COMMAND_blocking(S::dynamic_state()
, Args::[term()]) :: bool()
If blocking returns true, then QuickCheck assumes that the given call blocks in that state, allowing concurrent non-blocking calls to proceed first. Hopefully one of these will change the state so as to allow the blocking call to proceed. If not, QuickCheck expects the blocking call to time out eventually, allowing the test case to finish. Blocking operations can be included in test cases even if the COMMAND_blocking/2 callback is not defined, but QuickCheck can find more bugs given the additional information that blocking represents.
default: false
The properties for parallel testing are very similar to those for
sequential testing: we just replace the commands/1
and
run_commands/2
functions by their parallel versions. Often,
though, the race conditions we are testing for only occur sometimes,
and so we need to repeat each test several times using
?ALWAYS to be reasonably sure of provoking it. It is only
really necessary to do this during shrinking (since otherwise
shrinking is likely to stop before the test case is properly
simplified). Using this idea, a property that tests each case once
while initially searching for a failure, then ten times at each
shrinking step, could be written as
prop_atomic() -> ?FORALL(Repetitions,?SHRINK(1,[10]), ?FORALL(ParCmds,parallel_commands(client), ?ALWAYS(Repetitions, begin {Seq, Par, Res} = run_parallel_commands(?MODULE, Cmds), pretty_commands(?MODULE, Cmds, {Seq, Par, Res}, Res == ok) end))).Note also that the results from
run_parallel_commands/2
are
a little different from those of run_commands
.
One difference to be aware of is that postconditions and invariants are not checked during a parallel test, they are checked afterwards using the results collected from the concurrent tasks. This means that the postcondition and invariant callbacks cannot inspect the current state of the software under test, when they are used in parallel testing.
linearizable(ParCmds) can be used to insert calls to now() into the generated test case, giving more information to be used when deciding whether tests passed or failed.call() = {call, module(), atom(), [expr()]} | {call, module(), atom(), [expr()], metadata()}
A symbolic function call: {call,M,F,Args} represents a call of function F in module M, with arguments Args. {call,M,F,Args,Meta} represents a call with metadata (which may be symbolic). Metadata does not affect the way the call is executed, but is passed (as part of the call) to all the eqc_statem call-backs that take a call as an argument.
command() = {set, var(), call()} | {init, symbolic_state()}
A symbolic command, which when run either
performs a call and binds the result to a variable, or initialises
the state of the test case. (The latter appears only when commands/2
in used to generate a command sequence starting in a state other than
initial_state()).
command_history() = [{command(), term()}]
A list of commands and their results. The arguments in each call are the evaluated arguments, not the symbolic ones.
dynamic_state() = any()
The type used by the client module to represent
the state of a test case during test execution. It is the same as
symbolic_state()
, except that symbolic variables and calls
are replaced by their values.
exit() = {'EXIT', term()}
The type of a caught exception.
expr() = term()
A symbolic expression, which is evaluated by
replacing any symbolic variables (var()
) or function calls
(call()
) in the term by their values.
history() = [#eqc_statem_history{state = any(), args = eqc_statem:call(), features = [any()], result = any()}]
The history of a test execution, with one element for each command that was executed without an exception, containing the state before the command and the value it returned.
metadata() = [{atom(), expr()}]
A property list, where each property is a tuple containing a tag and an expression.
parallel_test_case() = {[command()], [[command()]]}
A sequential prefix, and a list of concurrent child tasks.
reason() = ok | initialization | {precondition, boolean()} | {postcondition, any()} | {invariant, any()} | {exception, exit()} | precondition_failed | {bad_dynamic_precondition, term()} | {bad_next_state, term()} | {bad_precondition, term()}
The reason execution of a command sequence terminated.
All commands completed normally, and all postconditions were true.
There was an exception when computing the initial state--that is, converting the
result of initial_state() to a dynamic_state()
.
A precondition failed to return true during test execution.
Since preconditions are checked when tests are generated, this should not normally
happen. It is possible
when using eqc:check/2
to rerun a saved test, after modifying the code,
or if any of initial_state/0, a _next or
_precondition callback behaves differently at generation time and test execution
time. For example, a pattern match on a symbolic variable ({var,N}) will
behave differently during test case generation and execution--so any such pattern
matching is a warning sign.
A postcondition failed to return true.
An invariant failed to return true.
One of the commands in the sequence raised an exception. In this case the
history()
contains all previous commands, and the final state is
the state just before the faulty command was executed.
symbolic_state() = any()
The type used by the client module to represent the state of a test case during test case generation.
var() = {var, integer()}
A symbolic variable, which is replace during test execution by the value bound
by the corresponding command()
.
apply/3 | Added by the QuickCheck framework to recognize the origin of the apply in test sequences. |
call_features/1 | Returns a list of command features exercised in this test. |
call_features/2 | Returns a list of features exercised by calls to F (or F/A, if the arity is also specified). |
check_commands/3 | Check the result of run_commands. |
check_commands/4 | Like check_commands/3 , but also takes the environment
passed to run_commands/3 as an additional parameter. |
command_names/1 | Returns a list of the command names used in Cmds. |
commands/1 | Generates a list of commands, using the abstract state machine defined in module Mod. |
commands/2 | Behaves like commands/1 , but generates a list of
commands starting in state S. |
eq/2 | Compare X and Y for equality, returns true if equal, and {X, '/=', Y} otherwise. |
get_metadata/2 | Retreive a field from the MetaData component. |
linearizable/1 | Adds calls of eqc_statem:now() before and after each command in the parallel part of the test case, which enables us to observe the order in which calls are made. |
more_commands/2 | Increases the expected length of command sequences generated within Gen by a factor N. |
now/0 | Used in combination with linearizable/1 . |
parallel_commands/1 | Generate a parallel test case from the callbacks in the client module Mod. |
parallel_commands/2 | Behaves like parallel_commands/1 , but generates a test
case starting in the state S. |
postconditions/3 | Given the values returned by a list of commands, checks that all pre- and postconditions are satisfied. |
pretty_commands/4 | Pretty-prints the execution history of a failing test, showing the calls made, the actual arguments and results, and (optionally) the model states. |
pretty_commands/5 | Like pretty_commands/4 , but also takes the environment
passed to run_commands/3 as an additional parameter. |
run_commands/2 | Runs a list of commands specified by the abstract state machine in client module Mod. |
run_commands/3 | Behaves like run_commands/2 , but also takes an environment
containing values for additional variables that may be referred
to in test cases. |
run_parallel_commands/2 | Runs a parallel test case, and returns the history of the prefix, each of the parallel tasks, and the overall result. |
run_parallel_commands/3 | Like run_commands/2 , but also takes an
environment binding variables, like run_commands/3 . |
show_states/1 | Causes a call of pretty_commands/4 or pretty_commands/5 in the property to display the test case states
as well as arguments and results. |
state_after/2 | Returns the symbolic state after a list of commands is run. |
zip/2 | Zips two lists together, but accepts lists of different lengths, stopping when the shorter list stops. |
apply(M, F, As) -> any()
Equivalent to erlang:apply(M, F, As).
Added by the QuickCheck framework to recognize the origin of the apply in test sequences.
call_features(H::history()) -> [any()]
Returns a list of command features exercised in this test.
Returns a list of features exercised by calls to F (or F/A, if the arity is also specified).
check_commands(Mod::atom(), Cmds::[command()], HSRes::{history(), dynamic_state(), reason()}) -> property()
Check the result of run_commands. The recommended way to write an eqc_statem property is in the form
X = run_commands(Mod,Cmds), ...any clean-up code... check_commands(Mod,Cmds,X)This:
eqc:conjunction/1
.
check_commands(Mod::atom(), Cmds::[command()], HSRes::{history(), dynamic_state(), reason()}, Env::[{atom(), term()}]) -> property()
Like check_commands/3
, but also takes the environment
passed to run_commands/3
as an additional parameter.
command_names(Cmds::[command()]) -> [{atom(), atom(), integer()}]
Returns a list of the command names used in Cmds. This function can be used in properties to measure the frequency with which each command actually occurs in the generated test cases, as follows:
?FORALL(Cmds,commands(...), begin {H,S,Res} = run_commands(...,Cmds), aggregate(command_names(Cmds), Res==ok) end)
Generates a list of commands, using the abstract state machine defined in module Mod. The commands in the sequence are generated by Mod:command/1, starting in the state Mod:initial_state(), and tracking state changes using Mod:next_state/3. Commands are only included in the sequence if their precondition (given by Mod:precondition/2) is satisfied. Sequences are shrunk by discarding commands in such a way that preconditions always hold, and all variables are set before they are used.
commands(Mod::atom(), S::symbolic_state()) -> gen([command()])
Behaves like commands/1
, but generates a list of
commands starting in state S. To ensure the correct state when the
commands are run, the first command is {init,S}.
eq(X, Y) -> true | {X, '/=', Y}
Compare X and Y for equality, returns true if equal, and {X, '/=', Y} otherwise. Typically used in postcondition; since it will result in a more informative counterexample.
get_metadata(Key::term(), Call::call()) -> false | {ok, term()}
Retreive a field from the MetaData component. This function pre-suppose that the meta data is organized in the form of a proplist with {Key, Value}-pairs.
linearizable(TestCase::parallel_test_case()) -> parallel_test_case()
Adds calls of eqc_statem:now() before and after each command in the parallel part of the test case, which enables us to observe the order in which calls are made. This gives us more information with which to determine whether a test passed or failed, which may improve the detection of races. On the other hand, calling now() involves a global synchronization, and so may make race conditions less likely to appear.
Increases the expected length of command sequences generated within Gen by a factor N.
now() -> any()
Equivalent to erlang:now().
Used in combination with linearizable/1
.
parallel_commands(Mod::atom()) -> gen(parallel_test_case())
Generate a parallel test case from the callbacks in the client module Mod. These test cases are used to test for race conditions that make the commands in the tests behave non-atomically.
parallel_commands(Mod::atom(), S::symbolic_state()) -> gen(parallel_test_case())
Behaves like parallel_commands/1
, but generates a test
case starting in the state S.
postconditions(Mod::atom(), Cmds::[command()], Vals::[term()]) -> bool()
Given the values returned by a list of
commands, checks that all pre- and postconditions are satisfied. Mod
is a module defining a state machine, Cmds a list of commands
generated from it, and Vals the list of values returned by running
those commands. This function is useful when the list of commands
cannot be run just by calling run_commands/2
, for example
because the commands represent calls to functions in a different
programming language.
pretty_commands(Mod::atom(), Cmds::[command()], HSRes::{history(), dynamic_state(), reason()}, P::property()) -> property()
Pretty-prints the execution history of a failing test, showing
the calls made, the actual arguments and results, and (optionally)
the model states. Like ?WHENFAIL, pretty_commands
takes the rest of the property as its last argument, and constructs
a new property that also pretty-prints. The argument Cmds
should be the list of commands passed to run_commands/2
,
and HSRes should be its result. Alternatively
(notwithstanding the type signature above) a parallel test case
generated by parallel_commands/1
, and the result of
run_parallel_commands/2
, can be passed instead.
The pretty-printing can be customized using
eqc_gen:with_parameter/3
to specify
eqc:quickcheck/1
is called from the Erlang shell.
Alternatively, the simplest way to show the states when a property fails is to call
eqc:quickcheck(eqc_statem:show_states(...property...)).from the shell.
pretty_commands(Mod::atom(), Cmds::[command()], HSRes::{history(), dynamic_state(), reason()}, Env::[{atom(), term()}], P::property()) -> property()
Like pretty_commands/4
, but also takes the environment
passed to run_commands/3
as an additional parameter.
run_commands(Mod::module(), Cmds::[command()]) -> {history(), dynamic_state(), reason()}
Runs a list of commands specified by the abstract state machine
in client module Mod. Before each command is run, its precondition is
checked by Mod:precondition/2, and after each command is executed, its
postcondition is checked by Mod:postcondition/3. The result contains the
history()
of execution, the state after the last command that was
executed successfully, and the reason()
execution stopped.
run_commands(Mod::module(), Cmds::[command()], Env::[{atom(), term()}]) -> {history(), dynamic_state(), reason()}
Behaves like run_commands/2
, but also takes an environment
containing values for additional variables that may be referred
to in test cases. For example, if Env is [{x,32}],
then {var,x} may appear in the commands, and will evaluate
to 32. The variables names must be atoms (unlike generated variable
names, which are numbers).
run_parallel_commands(Mod::atom(), ParCmds::parallel_test_case()) -> {command_history(), [command_history()], reason()}
Runs a parallel test case, and returns the history of the prefix, each of the parallel tasks, and the overall result.
run_parallel_commands(Mod::atom(), ParCmds::parallel_test_case(), Env::[{atom(), term()}]) -> {command_history(), [command_history()], reason()}
Like run_commands/2
, but also takes an
environment binding variables, like run_commands/3
.
show_states(Prop::property()) -> property()
Causes a call of pretty_commands/4
or pretty_commands/5
in the property to display the test case states
as well as arguments and results.
state_after(Mod::atom(), Cmds::[command()]) -> symbolic_state()
Returns the symbolic state after a list of commands is run. The commands are not executed.
zip(Xs::[A], Ys::[B]) -> [{A, B}]
Zips two lists together,
but accepts lists of different lengths, stopping when the shorter
list stops. This is useful to zip together a list of commands with
the history returned by run_commands/2
, to display each
command together with its result in the output from QuickCheck.
Generated by EDoc, Sep 11 2015, 13:38:12.