Copyright © Quviq AB, 2013-2015
Version: 1.36.1
This module provides simulation of QuickCheck state machine models.
The state machine is
specified by a client module similar to eqc_statem
with extra callback
return_value which specifies the expected return value of a given call.
Given such a client, this module can generate and simulate command sequences, checking that
all postconditions are satisfied. It can be used to validate a test model and to
obtain a quick prototype using Test Driven Development. It will also automatically
check the return value against the actual returned value when running tests on
an actual implementation.
The simulator specifications are a special form of eqc_statem
specifications
using additional meta data tagged return.
Modules which use eqc_statem_sim should include
-include_lib("eqc/include/eqc_statem") to import the
functions that eqc_statem_sim provides. The main difference is that
one has to provide MetaData to the eqc_statem call tuple.
One can use eqc_statem_sim both in grouped
or ungrouped style, see eqc_group_commands
for details.
Generated test cases are lists of symbolic commands (command()
), each
of which binds a symbolic variable to the result of a symbolic function call.
{set,{var,1},{call,gen_server,start_link,[myserver,[1],[]]},MetaData}
is a command to set variable 1 to the result of calling gen_server:start_link(myserver,[1],[]). The MetaData contains additional information for different state machine formalisms. In the simulation formalism, the MetaData contains the expected return value of the call.
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.
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()
) :: 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(),Callouts::language()
) :: 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.
symbolic_state()
,R::var()
,C::call()
,Callouts::language()
) :: 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.
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_sim 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_component_correct() -> ?FORALL(Cmds,commands(client), begin {H,S,Result} = run_commands(client,Cmds), Result==ok end).The main purpose of this module is to also be able to simulate the commands instead of really evaluating them. This is done by replacing run_commands by simulate_commands in the property:
prop_component_correct() -> ?FORALL(Cmds,commands(client), begin {H,S,Result} = simulate_commands(client,Cmds), Result==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.
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. |
get_return_value/1 | Return the return value given the MetaData from a call tuple. |
simulate_commands/2 | Runs a simulation of a list of commands specified by the abstract state machine in client module Mod. |
simulate_commands/3 |
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}.
get_return_value(MetaData::metadata()) -> term()
Return the return value given the MetaData from a call tuple. Defaults to no_return in case return value is not provided by callback module.
simulate_commands(Mod::atom(), Cmds::[command()]) -> {history(), dynamic_state(), reason()}
Runs a simulation of a list of commands specified by the abstract state machine
in client module Mod. Before each commands return_value is evaluated,
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.
simulate_commands(Mod, Cmds, E) -> any()
Generated by EDoc, Sep 11 2015, 13:38:12.