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

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

?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

• initial_state/0

  initial_state() :: eqc_statem: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.

The following call-back suffixes are provided for eqc_component.

• _pre/1

  COMMAND_pre(S::symbolic_state()) :: bool()

  Returns true if the command COMMAND may be generated in state S. The precondition is also used when shrinking to make sure that invalid commands do not pop-up in a test case while shrinking.

  default: true

• _pre/2

  COMMAND_pre(S::symbolic_state(), Args::[term()]) :: bool()

  Returns true if the symbolic call {call,_,COMMAND,Args} can be performed in the state S. The precondition is also used when shrinking to make sure that invalid commands do not pop-up in a test case while shrinking.

  default: true

  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.

  During shrinking, eqc_component also automatically checks whether the callouts (contained in the MetaData) are valid for this state and this call and re-computes the callouts if they are invalid.

• _adapt/2

  COMMAND_adapt(S::symbolic_state(), Args::[term()]) :: false | gen(call())

  This is an optional callback used during shrinking; when a precondition does not hold, adapt is called to try to repair/patch a call before it is discarded. Typically metadata in the call tuple can be adjusted. After adapt is finished, the precondition is checked again to see whether the changes were sufficient.

  Note that eqc_component will automatically try to adapt by regenerating callouts by calling _callouts/2; this function should only be defined if additional strategies should be tried.

  default: false

• _args/1

  COMMAND_args(S::symbolic_state()) :: gen([term()])

  Generates appropriate arguments for the function under test. The result are arguments Args that are used in the symbolic call

  {call, ?MODULE, COMMAND, Args}

  in the test case generator, given that COMMAND_pre(S) returns true for the symbolic state S at generation time.

• {no_suffix}/N

  COMMAND(...) :: term()

  This is the function that is called during test case execution.

• _callouts/2

  COMMAND_callouts(S::symbolic_state(), Args::[term()]) :: eqc_component:callout()

  Generates an appropriate callout descrition for a freshly generated call. Generating a symbolic call for eqc_component is a two stage process. First a command is generated (exactly as for eqc_statem), then the callout description is generated.

  Callouts are constructed using macros; in fact the macros define a small domain specific language (DSL) for describing callouts. See Constructing Callouts below.

  default: ?EMPTY

• _next/3

  COMMAND_next(S::symbolic_state(), V::var(), Args::[term()]) :: 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 {call, _, COMMAND, Args}, performed in symbolic state S, with result V. Because it is applied to symbolic states and symbolic calls, the result of the call must also be symbolic-- in fact, V is the symbolic variable which will be set to the result of the call.

  For example, if the state were a list of pids, and COMMAND applied to Args spawned a new process, then the variable V 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, and Args are the actual values passed (not symbolic argument expressions), and V is the actual value returned--in other words, all the symbolic inputs are replaced by their values. A correctly written COMMAND_next 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 COMMAND_next 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.

  Behind the scene the computation of the next state in eqc_component is more involved than for eqc_statem since local commands may also make changes to the next state. In this case the state supplied to the next_state function is the state after the changes made by local commands in the callouts callback.

  default: S, i.e., leave state unchanged

• _return/2

  COMMAND_return(S::symbolic_state(), Args::[term()]) :: term()

  This is an optional callback that computes the expected return value from the model state. This return value is used when clustering components. It is often good practice to check the return value in the postcondition by explicitely calling this return callback to check whether the actual returned value is equivalent with the return value computed by this function using the model state.

  default: ok

• _post/3

  COMMAND_post(S::dynamic_state(), Args::[term()], R::term()) :: bool()

  Checks the postcondition of symbolic call {call,_,COMMAND,Args}, executed in dynamic state S, with result R.

  In addition to the checks defined in the function, it is also checked that the expected callouts were made. Thus, this needs not be checked explicitly!

  default: true

  Of course, postconditions are checked during test execution, not test generation.

• _process/2

  COMMAND_process(S::symbolic_state(), Args::[term()]) :: default | root | worker | spawn | symbolic_pid()

  Specifies which process should execute COMMAND. The choices are

  • root The process running the tests. This is the most efficient, but if the command crashes it will take the whole test with it, which results in poor feedback from the failure.
  • worker Run the command in a designated worker process.
  • spawn Spawn a new worker process to run the command. The pid of the new process is available in the _callouts callback as ?SELF.
  • symbolic_pid() A previously spawned worker process.
  • default Use the value of the default_process parameter, which can be set using eqc_gen:with_parameter/3. If the default process is root and the command is blocking (see Testing blocking operations below) then spawn is used instead, since we must not block the QuickCheck process.
  default: default

• _features/3

  COMMAND_features(S::dynamic_state(), Args::[term()],R::term()) :: list(any())

  Collects a list of features of the symbolic call {call,_,COMMAND,Args}, 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. The features can be recovered later using call_features/1.

  default: []

  Features are collected during test execution, not test generation.

• _callers/0

  COMMAND_callers() :: [atom()]

  Returns a list of allowed callers for the COMMAND. This information is only used when the component is part of a cluster. If there are no restrictions for the command, [anyone] (the default) can be used. If used in a cluster, during command generation, this command is excluded from generation unless there is at least one caller in the list of callers that is not in the cluster!

  default: [anyone]

Additional callbacks

• command_precondition_common/2

  command_precondition_common(S::symbolic_state(),COMMAND :: atom()) :: bool()

  Used to specify a general command filtering precondition. The condition is applied to the symbolic state before we try to generate a command. A typical usage is:

  command_precondition_common(S, Cmd) ->
      S /= uninitialized orelse Cmd == init.

  This precondition ensures that unless the state is not uninitialized the command must be init.

• precondition_common/2

  precondition_common(S::symbolic_state(),Call::[call()]) :: bool()

  Used to specify a general precondition. This precondition is applied after command generation, but before the specific (COMMAND_pre/2 or COMMAND_pre/3) is applied. Thus in COMMAND_pre/2 (or COMMAND_pre/3) one may assume that the general precondition holds.

• postcondition_common/3

  postcondition_common(S::symbolic_state(),Call::[call()],Res::term()) :: bool()

  Used to specify a general postcondition. This precondition is applied after the specific (COMMAND_post/3 or COMMAND_post/4) is applied. A typical usage for eqc_component is to check that all return values follow what we expect:

  postcondition_common(S, Call, Res) ->
      eq(Res, return_value(S, Call)).

• call_features_common/3

  call_features_common(S::symbolic_state(),Call::[call()],Res::term()) :: bool()

  Used to specify features for all commands. These features are in addition to the features specified in specific COMMAND_features callbacks.

• process_common/2

  process_common(S::symbolic_state(),Call::[call()]) :: default | root | worker | spawn | symbolic_pid()

  Used to specify a process for all commands. The process from process_common is used if no specfic process (from COMMAND_process callbacks) is given.

• invariant/1

  invariant(S::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.

• api_spec/0

  api_spec() :: eqc_mocking:api_spec().

  In case mocking is used, the API specification should be returned by this callback function. See eqc_mocking/eqc_mocking_c for examples of how the API specification can be written. Together with the specification of expected calls (see ?CALLOUT below) the mocking behavior of components surrounding the SUT is conveniently specified.

• weight/2

  weight(S::dynamic_state(), Cmd :: atom()) :: bool()

  This is an optional callback which specifies the distribution with which commands are generated. Commands are normally generated with a the oneof generator unless a weight function is provided. In this case the weight computed from the symbolic state S is used as frequency in the frequency generator (used instead of oneof).

• ?CALLOUT(Mod, Fun, Args, ResultGen)

  Represents an expected callout, that is a call to a mocked function. The function should appear in the api_spec to let QuickCheck know that it should be mocked. The last argument is a generator for the return value of the function. If the generated value is needed in the rest of the callout specification, ?MATCH can be used to bind it.

  In most cases Args is the literal arguments expected by the call, but it may also contain the special values ?WILDCARD and ?VAR. In both cases an arbitrary term is accepted at the corresponding position in the call, but ?VAR also allows the actual value to be bound using a ?MATCH. In this case the ?CALLOUT returns a tuple of the bound ?VARs and the result generated by ResultGen. For instance, suppose you are testing a client that is expected to register itself with a server using a call server:register({client_id, Id}), for some Id picked by the client. You can then use a ?VAR to capture the value of Id as follows:

   ?MATCH({Id, _Ok}, ?CALLOUT(server, register, [{client_id, ?VAR}], ok)),
   ?APPLY(set_client_id, [Id])
   

  Using a ?VAR is also useful in combination with ?ASSERT when you don't know the exact value of an argument, but you want to check some property of it. For instance,

   ?MATCH({Arg, _}, ?CALLOUT(do, stuff, [?VAR], ok),
   ?ASSERT(erlang, is_integer, [Arg])
   

• ?MATCH(Pat, Callout)

  This is the callout command equivalent of an Erlang match statement Pat = Exp. It binds Pat to the result of the callout command Callout.

• ?MATCH_GEN(Pat, Gen)

  QuickCheck generators can be used inside callout specifications. They are typically used to generate the result of mocked functions in the ?CALLOUT command, but they can also be used freely with the ?MATCH_GEN command. This generates a value using Gen and binds it to Pat.

• Pat = Exp

  Used to run Erlang code at callout construction time, for instance extracting data from the state.

• ?APPLY(F, Args)

  Represents a call to a local command F. The local command should have a next state or callouts callback defined (or in some cases just a precondition), but does not necessarily have to be an API command. The ?APPLY command provides a convenient mechanism for abstraction and reuse of callout specifications.

  As an example, imagine that you have a component that contains three API-functions, a, b, and ab, where ab simply calls a and b in that order. Then, if we have already modelled a and b we can simply define the callouts of ab as:

  ab_callouts(_S, Args) ->
    ?APPLY(a, Args),
    ?APPLY(b, Args).

  (Under the assumption that a and b takes the same list of arguments.) As with ?CALLOUT the result of ?APPLY can be bound using ?MATCH.

• ?APPLY(Mod, F, Args)

  Represents a call to a command in another component Mod. If the component is in the current cluster, the specification in that module is used, otherwise this is a no-op.

  One common use case for this feature is cluster-wide preconditions. For instance, imagine that you have two components and that one has to be started before the other component can be started. Then the start command of the second component should call into the first component and ensure that it is properly started:

  %% Component A (a_spec.erl)
   ensure_started_pre(S, []) -> is_started(S).
  
   %% Component B (b_spec.erl)
   start_callouts(_S, []) ->
     ?APPLY(a_spec, ensure_started, []),
     ...

• ?EMPTY

  The default callout definition, no callouts are expected.

• ?RET(X)

  Defines the return value of the callout structure. Note that a defined return_value-function takes precedence.

• ?SEQ(C1, C2)

  Perform two callout commands in sequence. Equivalent to C1, C2.

• ?SEQ(Cs)

  Defines a callout structure where Cs are performed in sequence. (Cs should be a list of callout commands.)

• ?PAR(C1, C2)

  Defines a callout specification where C1 and C2 are performed in parallel. I.e. the order of the callouts is not specified. Note that when there are ?APPLY calls in C1 and C2 that modify the state, the state changes are applied in the order given.

• ?PAR(Cs)

  Defines a callout structure where Cs are performed in parallel. (Cs should be a list of callout commands.)

• ?EITHER(C1, C2)

  Defines a callout structure where either C1 or C2 is performed (but not both). The fact that we do not know which of the two will be called imposes a restriction on C1 and C2: they may not contain ?APPLY. The return value of an ?EITHER is always exactly 'ok'.

• ?EITHER(Tag, C1, C2)

  Same as ?EITHER(C1, C2), but all ?EITHER calls with the same tag must make the same choice (left or right). The scope of the tag is a single API command, so subsequent calls to the same API function may make a different choice.

• ?OPTIONAL(C)

  Shorthand for ?EITHER(C, ?EMPTY).

• ?WHEN(Test, C)

  Equivalent to

  case Test of
     true  -> C;
     false -> ?EMPTY
   end

• ?REPLICATE(C)

  Defines a callout structure where C is performed any number of times (including 0). Here C is not allowed to modify the state, since we do not know how many times it will be run.

• ?FAIL(X)

  Defines a failure, if we generate a ?FAIL as part of our callout specification it will fail during postcondition checking, with the error being X. This is sometimes useful for marking "impossible" cases in testing. Note that the absence or presence of a ?FAIL is determined at generation time and thus cannot depend on run-time data. This means that ?FAIL can be used as a sanity check on the model, but not for checking run-time postconditions. To do that, use ?ASSERT.

• ?ASSERT(Mod, Fun, Args, ErrorMsg)

  Define an assertion that should be checked at run-time. When checking postconditions, apply(Mod, Fun, Args) is evaluated and if the result is not true the postcondition check fails with the error message ErrorMsg. This is used to embed postconditions in the callout language which is often more convenient than writing separate postconditions.

• ?SEND(Pid, Msg)

  Specifies that the message Msg is expected to be sent to the process Pid. The process must be one of the worker processes (or the root process) executing commands. The pid of the current worker process is available as ?SELF in the callouts callback of a command, from where it can be saved in the state for future reference. See the process callback for more information.

• (obsolete) ?SAFELET(Pat, G, Callout)

  Equivalent to ?MATCH_GEN(Pat, G), Callout.

• (obsolete) ?BIND(Pat, C, Body)

  Equivalent to ?MATCH(Pat, C), Body.

• (obsolete) ?SELFCALL(Fun, Args), ?SELFCALL(Mod, Fun, Args)

  Equivalent to ?APPLY(Fun, Args) and ?APPLY(Mod, Fun, Args).

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.

   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.

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?

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 = 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()]}

api_spec()

api_spec() = #api_spec{language = erlang | c, mocking = atom(), config = undefined | 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

Function Details

commands/1

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

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 as set by the callouts. Default value 'ok'.

pretty_commands/4

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

• show_states (true or false), to determine whether model states should be included in the output,
• pretty_width (an integer), to specify the width available for pretty-printing.

Alternatively, the simplest way to show the states when a property fails is to call

 eqc:quickcheck(eqc_statem:show_states(...property...)).  

pretty_commands/5

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

pretty_commands/6

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

run_commands/1

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

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.

Overview