Overview

• Description
• Function Index
• Function Details

Copyright © Quviq AB, 2013-2017

Version: 1.42.1

Description

This module lets you do dynamic test case generation for a component or cluster of components.

Dynamic generation means that the next command in a command sequence is not generated until the previous commands have been executed and we have access to their results. This lets us model systems which behave nondeterministically, or systems whose behaviour we don't want to model in detail, in which case we cannot predict the final state of the system without actually running it and see how it behaves. There are two differences between dynamic testing and the ordinary testing that eqc_component and eqc_cluster provides:

• Command generation, preconditions and next state functions always have access to concrete data, there is never any symbolic data.
• Self callouts and cluster internal callouts are allowed in ?EITHER, ?OPTIONAL and ?REPLICATE, allowing state updates that depend on which callouts are performed at run-time.

Other than the above relaxations there is no difference between a dynamic component or cluster and a normal one. A property for a dynamic component has the following shape:

    prop_test() ->
      ?SETUP(fun() -> eqc_mocking:start_mocking(api_spec()), fun() -> ok end end,
      ?FORALL(Cmds, dynamic_commands(?MODULE),
      ?CHECK_COMMANDS(HSR={_History, _FinalState, Result}, ?MODULE, Cmds,
      pretty_commands(?MODULE, Cmds, HSR,
        Result == ok)))).

The dynamic_commands/1 generator executes the commands as they are generated, so Cmds contains not only the generated commands but their callouts and results, as well as any postcondition or callout specification failures. The ?CHECK_COMMANDS macro decomposes the generated commands into a history, a final state and a test result compatible with eqc_component:pretty_commands/4.

Macros

?CHECK_COMMANDS is defined in the eqc/include/eqc_dynamic_cluster.hrl header file and binds the history, the final state and result of the commands for use in the property. The result is ok when the test succeeded, otherwise it is a description of why it failed. During normal operation ?CHECK_COMMANDS simply extracts the history and the result already present in the command sequence, but if a test is repeated, either with eqc:check/2 or in an ?ALWAYS or a ?SOMETIMES, ?CHECK_COMMANDS reruns the sequence discarding the results from the first run.

Examples

Since there are no symbolic values in a dynamic test it is possible to model components whose behaviour we can't predict precisely. For instance, here is the model for a lock function that is allowed to fail unpredictably:

 lock_next(S, V, {call, _, lock, []}) ->
   case V of %% V is never symbolic
     ok         -> S#state{ lock = locked };
     {error, _} -> S
   end.

Dynamic components can also make state updates based on callouts that are not certain to happen. For example, we can model a component that can choose to go to sleep by calling a go_to_sleep function as follows:

 main_callouts(_S, []) ->
   ?OPTIONAL(?SEQ(?CALLOUT(controller, go_to_sleep, [], ok),
                  ?APPLY(set_mode, [sleeping]))).

 set_mode_next(S, _, [Mode]) -> S#state{ mode = Mode }.

Function Index

Function Details

dynamic_commands/1

Generator for a random command sequence. Mod is the name of a module defining a component or a cluster (see eqc_component and eqc_cluster). The commands are executed as they are generated so the resulting command sequence contains not only the generated commands but also a trace of the execution and any errors encountered during the run. The command sequence should be given to ?CHECK_COMMANDS which will decompose it into a history, a final state and the result of the test.

dynamic_commands/2

Generator for a random command sequence starting from a given initial state. In the case Mod defines a cluster InitState should be a list of pairs of a component name and the initial state for that component. Only components for which the state is different from the default initial state need to be present in the list. Aside from setting the initial state this function works in the same way as dynamic_commands/1.

Overview