Copyright © Quviq AB, 2012-2023
Version: 1.46.3
This module provides functions for testing operations with side-effects, which are
specified via a collection of abstract state machines with external
interactions. I.e. it is possible to compose several eqc_component
into one
cluster.
Modules using eqc_cluster should include -include_lib("eqc/include/eqc_cluster.hrl") to import the functions that eqc_cluster provides.
The majority of the modelling work is put into the models of the components. To cluster components (given that they actually fit together) is straighforward; all that is needed is to define two simple callbacks, and to write a property.
Returns the list of components that make up the cluster.
api_spec() :: eqc_mocking:api_spec()
.
Returns the API specification of the clustered components and their surroundings. Normally this function is defined as
api_spec() -> eqc_cluster:api_spec(?MODULE).I.e. it can be computed from the API specifications of the separate components. For the cluster to be able to correctly identify cluster internal callouts this needs to be specified in the respective API specification. As an example, if we have a fictive communication stack, with a frame layer and a packet layer, the API specification of the frame, with respect to the packet module, could look like:
#api_module{ name = packet, functions = [#api_fun{ name = wakeup, arity = 1}, #api_fun{ name = send_ack, arity = 1}, #api_fun{ name = recv, arity = 1}] }.If we later decide to cluster the frame_eqc and the packet_eqc models, we need to specify that callouts in frame_eqc to functions in packet should then be internal to the cluster. This is done by using the classify field in #api_fun:
#api_module{ name = packet, functions = [#api_fun{ name = wakeup, arity = 1, classify = packet_eqc}, #api_fun{ name = send_ack, arity = 1, classify = packet_eqc}, #api_fun{ name = recv, arity = 1, classify = packet_eqc}] }.This ensure that the correct updates are made to the model whenever the frame_eqc component makes a callout to packet. If the model function is not named the same as the mocked function (which is often the case when mocking C), the classify field may also be a two-tuple {Module, Function}. Further, it might also be necessary to adapt the arguments passed to the model function, in this situation the classify field may also be a three-tuple {Module, Function, AdaptArgsFun}, where AdaptArgsFun is a function that translates the passed arguments into what the model is expecting. An example could be where the (mocked) function takes a set as an argument, but where the model uses a list: {m, f, fun([Set]) -> [sets:to_list(Set)] end}. I.e. the AdaptArgsFun gets a list of arguments as input and should return a list of modified arguments.
The most general way to classify a callout is to give a function ClassifyFun in the classify field. This function is applied to the arguments to the mocked function and is expected to return a triple {Module, Function, Arguments} with the model call corresponding to the mocked call. This can be useful for clusters of parameterised components. For instance, suppose you have a system with a number of resources, where resources are modelled by a component resource_spec parameterised by the resource handle, but to access a resource you call a function use(Handle, Arg). You could then use the following classification:
#api_fun{ name = use, arity = 2, classify = fun([Handle, Arg]) -> {{resource_spec, Handle}, use, [Arg]} end }A limitation in this case is that the use function will always be mocked, since we cannot know beforehand whether it will be internal to the cluster.
When the components are tested in isolation, all of its API functions are normally tested. However, once components are composed into a cluster it is often the case that some API functions are internal. For example, in the fictive communication stack the frame layer has a send function. However, this send function is only called from the packet layer; thus, once the two modules are clustered it should not be called directly from the outside.
To specify this, we should add (given that we are using the grouped modelling style for the component):send_callers() -> [packet_eqc].
I.e. we specify that this API function is only called from packet_eqc. The callers definition is only taken into account in a cluster.
prop_cluster_correct() -> ?SETUP(fun() -> start_mocking(api_spec(), components()), fun() -> ok end end, ?FORALL(Cmds,commands(?MODULE), 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.
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{name = atom(), classify = any(), ret = atom() | api_arg_c(), args = [api_arg_c()], silent = false | {true, any()}}
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{name = atom(), fallback = atom(), functions = [api_fun_erl()] | [api_fun_c()]}
api_spec/1 | Computes a cluster api_spec by doing a merge of the api_specs of the components. |
commands/1 | Generates a list of commands, using the cluster defined in module Mod. |
commands/2 | Generates a list of commands, using the cluster defined in module Mod, where custom initial states for some or all components are given by S. |
run_commands/1 | Runs a list of commands, checking preconditions before, and postconditions after executing each command. |
run_commands/2 | Behaves like run_commands/1 , but also takes an environment
containing values for additional variables that may be referred
to in test cases. |
api_spec(Mod::atom()) -> #api_spec{language = erlang | c, mocking = atom(), config = any(), modules = [api_module()]}
Computes a cluster api_spec by doing a merge of the api_specs of the components. Components are given by Mod:components().
commands(Mod::module()) -> eqc_gen:gen([eqc_statem:command()])
Generates a list of commands, using the cluster defined in module Mod.
commands(Mod::module(), S::[{atom(), term()}]) -> eqc_gen:gen([eqc_statem:command()])
Generates a list of commands, using the cluster defined in module Mod, where custom initial states for some or all components are given by S.
run_commands(Cmds::[eqc_statem:command()]) -> {eqc_statem:history(), eqc_statem:dynamic_state(), eqc_statem:reason()}
Runs a list of commands, checking preconditions before, and postconditions after executing each command. The result contains the history of execution, the state after the last command that was executed successfully, and the reason execution stopped.
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).
Generated by EDoc