Overview

• Description
• Data Types
• Function Index
• Function Details

Copyright © Quviq AB, 2012-2017

Version: 1.42.1

Description

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.

Callback Functions

• components/0

  components() :: [atom()]

  Returns the list of components that make up the cluster.

• api_spec/0

  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() -> 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.

Respecting API's

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.

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.

What Property Should We Test?

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)).

Data Types

api_arg_c()

api_arg_c() = #api_arg_c{type = undefined | atom() | string(), stored_type = atom() | string(), name = undefined | 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 = undefined | atom(), classify = undefined | any(), ret = atom() | api_arg_c(), args = [api_arg_c()], silent = false | {true, any()}}

api_fun_erl()

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

api_module()

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

Function Index

Function Details

api_spec/1

Computes a cluster api_spec by doing a merge of the api_specs of the components. Components are given by Mod: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. 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

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).

Overview