| Overview |  |
Copyright © Quviq AB, 2004-2015
Version: 1.34.3
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.
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).
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. 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.
symbolic_state(),C::call()) :: bool()
Returns true if the symbolic call C can be performed in the state S. 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(), C::call()) :: 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. This function may be partial, i.e. if it crashes it is interpreted as no adaptation is possible. After adapt is finished, the precondition is checked again to see whether the changes were sufficient.
symbolic_state()) :: gen(call()
Generates an appropriate symbolic function call to appear next in a test case, if the symbolic state is S. Test sequences are generated by using command(S) repeatedly. However, generated calls are only included in test sequences if their precondition is also true.
dynamic_state(),C::call(),R::term()) :: bool()
Checks the postcondition of symbolic call C, 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. Thus when a postcondition is checked, we know the function called, the values it was passed, the value it returned, and the state in which it was called.
Of course, postconditions are checked during test execution, not test generation.
dynamic_state(),C::call(),R::term()) :: list(any())
Collects the features of a symbolic call C, 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 result is a list of features, which can later be retrieved from
the test execution history by using call_features/1.
Features are collected during test execution, not test generation.
symbolic_state(),R::var(),C::call()) :: 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 C, performed in symbolic state S, with result R. Because it is applied to symbolic states and symbolic calls, the result of the call must also be symbolic-- in fact, R is the symbolic variable which will be set to the result of the call. R can then be included in the next state if necessary. For example, if the state were a list of pids, and C spawned a new process, then the variable R 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, C is a symbolic call in which the arguments are the actual values passed (not symbolic argument expressions), and R is the actual value returned--in other words, all the symbolic inputs are replaced by their values. A correctly written next_state 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 next_state 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.
dynamic_state()) :: bool()
This is an optional call-back 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.
dynamic_state(),C::call()) :: 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.
Typically each function appearing in generated tests is specified by
a generator in the command/1 callback, a clause in the
precondition/2 callback, a clause in the
next_state callback, and so on. Thus the specification of
one function is divided into fragments that appear in different
places in the model. This can become unwieldy for complex state
machines, and so eqc_statem also supports "grouped"
specifications, in which all the aspects of a function are specified
together. The grouped syntax is documented under eqc_group_commands.
prop_statem_correct() ->
?FORALL(Cmds,commands(client),
begin {H,S,Res} = run_commands(client,Cmds),
check_commands(client,Cmds,{H,S,Res}).
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 blocking/2 callback:
blocking(S::If blocking/2 is not defined in the state machine specification, then it is assumed always to return false. 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 blocking/2 call-back is not defined, but QuickCheck can find more bugs given the additional information that blocking/2 represents.dynamic_state(),C::call()) :: bool()
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 {H,S,Result} = run_parallel_commands(client,ParCmds),
check_commands(client,ParCmds,{H,S,Result})
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, atom(), atom(), [expr()]} | {call, atom(), atom(), [expr()], proplist()}
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() = [{dynamic_state(), term()}]
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.
parallel_test_case() = {[command()], [[command()]]}
A sequential prefix, and a list of concurrent child tasks.
proplist() = [{atom(), expr()}]
A property list, where each property is a tuple containing a tag and an expression.
reason() = ok | initialization | {precondition, boolean()} | {postcondition, any()} | {invariant, any()} | {exception, exit()}
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 one of the functions initial_state/0, next_state/3, or
precondition/2 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 | Equivalent to erlang:apply(M, F, As). |
| 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 | Equivalent to erlang:now(). |
| 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).
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(), Cmd::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().
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::atom(), 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::atom(), 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, May 11 2015, 12:46:12.