Module eqc_statem_sim

This module provides simulation of QuickCheck state machine models.

Copyright © Quviq AB, 2013-2015

Version: 1.36.1

Description

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.

Symbolic Commands

Generated test cases are lists of symbolic commands (command()), each of which binds a symbolic variable to the result of a symbolic function call.

For example,
{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.

Callback Functions

The client module specifies an abstract state machine by defining the following functions:

Grouping Callbacks

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.

What Property Should We Test?

This module does not define any properties to test, it only provides functions to make defining such properties easy. A client module will normally contain a property resembling this one, which generates a command sequence using the client state machine, and then tests it:
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.

Function Index

commands/1Generates a list of commands, using the abstract state machine defined in module Mod.
commands/2Behaves like commands/1, but generates a list of commands starting in state S.
get_return_value/1Return the return value given the MetaData from a call tuple.
simulate_commands/2Runs a simulation of a list of commands specified by the abstract state machine in client module Mod.
simulate_commands/3

Function Details

commands/1

commands(Mod::atom()) -> gen([command()])

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/2

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/1

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/2

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/3

simulate_commands(Mod, Cmds, E) -> any()


Generated by EDoc, Sep 11 2015, 13:38:12.