Module eqc_component

This module provides functions for testing operations with side-effects, which are specified via an abstract state machine with external interactions.

Copyright © Quviq AB, 2012-2023

Version: 1.46.3

Description

This module provides functions for testing operations with side-effects, which are specified via an abstract state machine with external interactions.

A component state machine is specified by a client module similar to eqc_statem with extra callbacks callouts and return_value that specifies how the state machine interacts with other components. Given such a component, this module can generate and run command sequences, checking that all postconditions are satisfied and that all external functions are called (via eqc_mocking). Alternatively one can cluster components together to build large specifications from parts using eqc_cluster. It will shrink failing sequences by discarding commands that do not contribute to the failure. Thus, it can be used to find minimal command sequences which elicit an unexpected behaviour.

Component specifications are a special form of eqc_statem specifications. Modules using eqc_component should include -include_lib("eqc/include/eqc_component") to import the functions that eqc_component provides. Do not include eqc_statem; functions needed from that module are automatically imported.

Symbolic Commands

Generated test cases are lists of symbolic commands (eqc_statem: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 component formalism, the MetaData contains a callout description that describes what additional functions are expected to be called when calling the function {call,gen_server,start_link,[myserver,[1],[]]}. The MetaData can also contain the expected return value, if it is defined by the callouts. The callout description can then be used by eqc_mocking to mock the environment outside the SUT; or it can be used by eqc_cluster to correctly combine several components.

As an example, the language provided to this particular call to start a generic server could be
?CALLOUT(myserver,init,[[1]],{ok,1}).

In that case, we do test the gen_server module as SUT and make sure it calls the right callbacks. We specify that the callback to be called is init in the module myserver and that the argument to call it with is the list [1]. We expect the environment to return {ok,1} when this function is called. While the SUT and the (mocked) environment are Erlang we only have a single return value; however, if C is used there are out-parameters that can be part of the "return value". (See eqc_mocking for more details.)

When a test case is run, then symbolic variables (eqc_statem:var()) are replaced by the values they were set to, and symbolic calls (eqc_statem: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

Each command (or API function of the software under test) is specified by a number of functions, which can be grouped together, that represent generation, precondition, postcondition, state update, etc. These functions are named by appending a suffix to the name of the command itself. Apart from the COMMAND_args callback, each of these callbacks is optional, and if not provided a default is used. In addition to callbacks for a specific command, there are also a number of general callbacks, such as The client module specifies an abstract state machine by defining the following functions:

The following call-back suffixes are provided for eqc_component.

Additional callbacks

In addition to the per-command call-backs described above, the following optional call-backs may be included.

Constructing callouts

Callout specifications are built using a macro-based domain specific language and can appear in the _callouts callback. A callout specification is a comma-separated sequence of callout commands, representing the behaviour of the system under test.

To construct callout specifications outside the callouts callbacks, say in a helper function, the callouts need to be wrapped in the ?CALLOUTS() macro. This macro takes an arbitrary number of callout commands as arguments.

The valid callout commands are the following:

In addition to the commands listed above, the normal Erlang control structures, like case and if, are valid callout commands. For case, the scrutinee must be an Erlang expression (and not a callout command), but the clause bodies can be callout command sequences.

Testing blocking operations

Component models support testing systems where some operations are blocking. A typical example is a server with a synchronous client API, but which uses an asynchronous API to talk to the underlying layer (for instance a piece of hardware). In this situation, if you are testing the server in isolation, mocking the hardware layer, you need to execute operations corresponding to calls from the hardware while client operations are still in progress. This is possible using the ?BLOCK and ?UNBLOCK callout primitives: A typical use looks as follows:
   request_callouts(_S, [Req]) ->
     ?APPLY(add_request, [?SELF, Req]),
     ?MATCH(Res, ?BLOCK),
     ?APPLY(rem_request, [?SELF]),
     ?RET(Res).

   reply_args(S) -> [elements(pending_requests(S)), result()].

   reply_callouts(_S, [Pid, Res]) ->
     ?UNBLOCK(Pid, Res).
 

By default blocking operations are executed in a fresh process, but it's possible to use the process callback to change this. Postconditions of blocked operations are checked when they complete, but callouts are checked as they happen.

For more information about testing blocking operations see
Ulf Norell, Hans Svensson, and Thomas Arts, 2013. Testing blocking operations with QuickCheck's component library. In Proceedings of the twelfth ACM SIGPLAN workshop on Erlang (Erlang '13).

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() ->
   ?SETUP(fun() -> eqc_mocking:start_mocking(api_spec()), fun() -> ok end end,
   ?FORALL(Cmds,commands(client),
     begin {H,S,Result} = run_commands(Cmds),
           pretty_commands(?MODULE,Cmds,{H,S,Result},
                           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 setup mocking before test execution. It is to allow this flexibility that the properties to test are placed in the client module, rather than in this one.

Example

To illustrate how a callout specification could look like we take as an example a mode change operation of a communication component. If the system is busy it is not possible to change mode, otherwise the SUT should change mode and make a call to the underlying driver. Note that we are using a local command to do the state update. This is a typical usage of local commands and ?APPLY, the set_driver_state command can also be used in other callout specifications.

change_mode_callouts(S, [NewMode]) ->
   case S#state.driver_state of
     busy ->
       %% We can't change mode while sending!
       ?RET({error, busy});
     _    ->
       %% Change mode. Might fail.
       ?MATCH(Res, ?CALLOUT(driver, change_mode, [NewMode], elements([ok, error]))),
       ?WHEN(Res == ok, ?APPLY(set_driver_state, [NewMode])),
       ?RET(Res)
   end.

 set_driver_state_next(S, _Value, [NewState]) ->
   S#state{ driver_state = NewState }.
 

Data Types

api_arg_c()

api_arg_c() = #api_arg_c{type = atom() | string(), stored_type = atom() | string(), name = atom() | string() | {atom(), string()}, dir = in | out, buffer = false | true | {true, non_neg_integer()} | {true, non_neg_integer(), string()}, phantom = boolean(), matched = boolean(), default_val = no | string(), code = no | string()}

api_fun_c()

api_fun_c() = #api_fun_c{name = atom(), classify = any(), ret = atom() | api_arg_c(), args = [api_arg_c()], silent = false | {true, any()}}

api_fun_erl()

api_fun_erl() = #api_fun{name = atom(), classify = any(), arity = non_neg_integer(), fallback = boolean(), matched = [non_neg_integer()] | fun((any(), any()) -> boolean()) | all}

api_module()

api_module() = #api_module{name = atom(), fallback = atom(), functions = [api_fun_erl()] | [api_fun_c()]}

api_spec()

api_spec() = #api_spec{language = erlang | c, mocking = atom(), config = any(), modules = [api_module()]}

call()

call() = eqc_statem:call()

A symbolic call. Defined in eqc_statem, eqc_statem:call().

callout_spec()

abstract datatype: callout_spec()

The type of callouts. Terms of this type is constructed by using the macros described above.

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/1Get return value as set by the callouts.
pretty_commands/4Pretty-prints the execution history of a failing test, showing the calls made, the actual arguments and results, and (optionally) the model states.
pretty_commands/5Like pretty_commands/4, but also takes the environment passed to run_commands/2 as an additional parameter.
pretty_commands/6Like pretty_commands/5, but takes an API specification as an additional parameter.
run_commands/1Runs a list of commands specified by an abstract state machine in some client module Mod.
run_commands/2Behaves like run_commands/1, but also takes an environment containing values for additional variables that may be referred to in test cases.

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::eqc_statem: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::eqc_statem:metadata()) -> ok | term()

Get return value as set by the callouts. Default value 'ok'.

pretty_commands/4

pretty_commands(Mod::atom(), Cmds::[eqc_statem:command()], HSRes::{eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}, P::eqc:property()) -> eqc: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/4 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/1, and HSRes should be its result.

The pretty-printing can be customized using eqc_gen:with_parameter/3 to specify

Note that these parameters are parameters to the entire property, and can be specified when 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/5

pretty_commands(Mod::atom(), Cmds::[eqc_statem:command()], HSRes::{eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}, Env::[{atom(), term()}], P::eqc:property()) -> eqc:property()

Like pretty_commands/4, but also takes the environment passed to run_commands/2 as an additional parameter.

pretty_commands/6

pretty_commands(Mod::atom(), Cmds::[eqc_statem:command()], HSRes::{eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}, Env::[{atom(), term()}], ApiSpec::api_spec() | none, P::eqc:property()) -> eqc:property()

Like pretty_commands/5, but takes an API specification as an additional parameter.

run_commands/1

run_commands(Cmds::[eqc_statem:command()]) -> {eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}

Runs a list of commands specified by an abstract state machine in some 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/2

run_commands(Cmds::[eqc_statem:command()], Env::[{atom(), term()}]) -> {eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}

Behaves like run_commands/1, 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).

Note: can also be used as run_commands(Mod, Cmds) to run command sequences generated with QuickCheck < 1.39.


Generated by EDoc