Module eqc_fsm

This module is designed for testing software with a finite number of abstract states--for example software described by UML statecharts.

Copyright © Quviq AB, 2006-2016

Version: 1.39.1

Description

This module is designed for testing software with a finite number of abstract states--for example software described by UML statecharts. It allows users to specify a collection of named states and the transitions between them, along with pre- and post-conditions and state transition functions. Users can assign weights to transitions, to achieve a good statistical distribution of test cases, and eqc_fsm can help users do so by generating visualizations of the state diagram, and by automated weight assignment.

eqc_fsm is closely related to eqc_statem, and generates test cases of precisely the same form. (One way to think of eqc_fsm is that it is to eqc_statem as gen_fsm is to gen_server). We assume that readers are already familiar with eqc_statem; if not, study the eqc_statem documentation before reading further. The cases in which you may prefer eqc_fsm over eqc_statem are when you have a test API for which some API calls are clearly only callable when the Software Under Test is in a specific state. This situation can be solved by adding preconditions to the eqc_statem QuickCheck model, but alternatively, can be handled using the eqc_fsm modeling approach.

Since release 1.35 of QuickCheck, the documentation of this module has been updated to the grouped style of writing callbacks. In case you are confronted with a legacy state machine model that you need to understand, please read the old documentation.

The examples directory distributed with QuickCheck contains a module lock_eqc.erl (source code) that illustrates how eqc_fsm can be used in a simple case.

Contents

Specifying State Machines

State machines are specified by a module defining callback functions that are invoked to test the state machine. The callbacks closely resemble those used by eqc_statem. The main differences are the addition of a finite state machine to specify when certain commands can be generated. A collection of functions corresponding to named states specify in what state a certain command can be added to a test case. The other difference is that callbacks have two more arguments: a From state and a To state.

The eqc_fsm Header File

Modules using eqc_fsm should begin by including the eqc_fsm header file:
  -include_lib("eqc/include/eqc_fsm.hrl"). 

(If QuickCheck is not installed in your Erlang library directory, then you will need to use -include and give a different path). This imports all the exported functions from eqc_fsm, together with those functions from eqc_statem that are usable with eqc_fsm too. Note that you should not include eqc_statem.hrl in the same module.

State Names and State Data

eqc_fsm tracks the state of each test case, just as eqc_statem does, but eqc_fsm splits the state into two parts: a state name (normally an atom), which corresponds to one of the states in a finite-state machine diagram, and state data, which may be any relevant information, but is normally a record. This is a similar distinction to that made between state names and state data by gen_fsm in the OTP libraries. Complete states are represented by a pair of the state name and the state data.

Specifying Named States

Specifying Transitions from each State

Each named state is defined by a function of the same name, which returns a list of target state names to which a transition can be made, paired with function calls whose execution follows that transition. For example, in a system with two named states, locked and unlocked, the unlocked state might be specified by

  unlocked(S) ->
    [{unlocked,read}},
     {locked,  lock}].

which specifies that a transition from the unlocked state to the locked state can be made by calling the lock function, or we can call the read function and remain in the same state. eqc_fsm generates test cases which follow the transitions specified in this way from state to state. The argument generators for the lock and read function are generated with an _args callback in the same way as eqc_statem provides argument generation.

history as a Target State

If the target state name is the atom history, then this represents a transition to the same state. This can be used to abstract a set of transitions that can be used in several different states. For example,

  read_transition() ->
    [{history, read}].

could be used to define a read transition that can be included in any other state by adding read_transition()++... to the state definition; whatever state it is used in, the read transition returns to the same state.

State Attributes

State functions may take additional parameters, called attributes. For example,

  unlocked(N) ->
    [{{unlocked,N+1}, add} || N<4] ++
    [...other transitions...].

might represent a locker containing N values. When attributes are used, then the state names are tuples of the function name and the attribute values. States with different attribute values are considered to be different states: {unlocked,0} and {unlocked,1} are different states in this example. Since QuickCheck enumerates every reachable state, then it is important that there are only finitely many reachable attribute values--this is why we only include an add transition when N is less than 4 in the example above--this ensures that states {unlocked,N} are not reachable for N greater than or equal to 5.

It is perfectly allowable for the list of transitions to depend on the values of attributes, as in this example.

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 following callback suffixes are provided for eqc_fsm.

In addition to specific callbacks for one command, there are a few more general callbacks:

The Property to Test

eqc_fsm specifications are tested using very similar properties to eqc_statem specifications: the only difference is that the commands/1 and run_commands/2 functions are imported from eqc_fsm instead (which is done by the eqc_fsm.hrl include file). Thus a suitable propery might look something like this:

  prop_locker() ->
    ?FORALL(Cmds,commands(?MODULE),
      begin
        locker:start(),
        {H,S,Res} = run_commands(Cmds),
        locker:stop(),
        Res == ok
      end).

Weighting Transitions

The definitions of state functions described above offer no opportunity to specify how often each transition should be chosen. This is done instead by a separate callback:

  weight(From, To, Cmd, Args) -> integer()

This callback is optional: if it is omitted (or not exported), then the transitions from each state are chosen with equal probability. If weight is defined, then the weights it assigns to each transition are used in the same way as the weights passed to the eqc_gen:frequency/1 function: the probability of choosing a transition is proportional to the weight assigned to it.

It is important to measure the resulting distribution of transitions in the generated test data. This can be done during testing by amending the last line of the property above to

  aggregate(zip(state_names(H), command_names(Cmds)),
            Res == ok)

using the functions eqc:aggregate/2, state_names/1, eqc_statem:command_names/1, and eqc_statem:zip/2. The output generated shows the proportion of each state name/function name combination in the total set of transitions run.

Visualizing State Machines

eqc_fsm can generate diagrams visualizing the state space and the transitions between states, along with the frequency with which each transition is tested.

Visualization Tools

QuickCheck uses external tools to generate and display visualizations. Users need to install these tools separately, and make them available to QuickCheck.

Graph Drawing Using GraphViz

QuickCheck generates visualizations of the state space in the dot graph description language. These can be converted to a wide variety of image formats using the GraphViz tools, which can be downloaded from www.graphviz.org for a wide variety of platforms, under the open-source Common Public Licence.

Once installed on your system, ensure that dot (or dot.exe) is accessible via your path. If you can invoke dot in your shell by typing dot, then QuickCheck should be able to make use of it. Alternatively, you can specify the location of this file in the environment variable EQC_DOT. QuickCheck will use dot to generate JPEG visualizations (or another supported image type of your choice).

Configuring a JPEG viewer

If you provide QuickCheck with a JPEG viewer, then it will use it to display visualizations automatically. Under Windows XP and Vista, nothing needs to be done--your default JPEG viewer will be used automatically. Under other operating systems (or if you want to use a different viewer), you should set the environment variable EQC_VIEWER to the location of the viewer of your choice. QuickCheck displays images by running a shell command of the form <EQC_VIEWER> <filename>.jpg. You can specify another image type supported by GraphViz when generating images; in this case, the viewer should of course be suitable for the type of image you choose.

Creating visualizations

Visualizations are created and displayed by visualize/1. If only the dot file is required, then it can be generated by dot/1. The visualizations include the estimated frequency of each transition when tests are run, such as this example:

The percentages shown are the number of times the labelled transition will be followed during testing, as a percentage of the total number of transitions followed. The result of the analysis should agree with measured transition frequencies when sufficiently any tests are run (several thousands)--but the analysis is much quicker.

The results can be used to help assign appropriate weights to transitions. Users should aim to avoid orphan transitions, which are tested very rarely, because bugs which depend on such orphans will take a very long time to find.

Analysing State Machines

QuickCheck can predict the frequency with which each transition in the state machine will be followed during testing, and can also use these predictions to suggest a suitable choice of weights.

Compensating for failed preconditions

The analysis assumes that once a transition has been chosen, then a suitable call can always be generated. If attempts to generate a call can fail--either because the generation raises an exception, or because the precondition is false--then the analysis will overestimate the frequency of that and subsequent transitions. It is important to compare the analysis results with actual measured transition frequencies, to see to what extent this is occuring.

To perform an accurate analysis, QuickCheck needs to know how often the attempt to generate a suitable call fails--which cannot be determined in advance. Users can provide an estimate of this by defining the (optional) callback _preprobability The result should be a float between 0 and 1, which is the estimated probability of succeeding to generate a call satisfying the precondition for this transition. For example, if we expect generation of a read call in an unlocked state to fail half the time, then we could define

  read_preprobability(unlocked, _, [_]) -> 0.5;
  read_preprobability(_, _, _) -> 1.0.

Automatic weight assignment

QuickCheck can assign weights to transitions automatically, taking into account the user's estimates of precondition probabilities specified above. QuickCheck compensates for a low precondition probability by trying to choose that transition more often. Weights are assigned so as to avoid orphan transitions, as far as possible--although in most cases, no assignment of weights can ensure an absolutely even distribution of testing effort.

The weight assignment is computed by automate_weights/1, which outputs a candidate definition of the weight callback, and (if GraphViz and a JPEG viewer are available) visualizes the resulting transition frequencies. The definition of weight can be pasted back into the eqc_fsm specification, to cause QuickCheck to use the computed weights.

The assigned weights are not necessarily "optimal" in any sense, but are often better than a hand-assignment. It is still important to measure actual transition distribution, and tune the assigned weights if necessary.

Prioritizing Transitions

Often, some transitions should be tested more often than others: for example, one transition may call a function with no arguments, while another may have many complex arguments, with a wide variety of choices to explore. Of course, the latter needs to be tested more often than the former. When weights are assigned manually, then the user can take this into account by weighting the latter transition more highly, but when they are assigned automatically then a different mechanism is required.

Users can prioritize transitions by defining the optional callback

  priority(From, To, Cmd, Args) -> integer() | float() 
with the same parameters as precondition_probability. The automated weight assignment will then choose weights that increase the execution frequency of highly prioritized transitions. For example, using the same state machine as in the diagram above, we could increase the priority of lock transitions by defining
  priority(unlocked,_,lock,_) -> 10;
  priority(_,_,_,_) -> 1.

The resulting transition frequencies are as shown here:

Note that both the lock and unlock transitions are assigned a greater weight--the latter, because choosing unlock is necessary to permit another lock, so unlocking more often permits more tests of locking. Automated weight assignment takes into account these kinds of interactions between transitions, which is hard to do well by hand.

External specification of FSM

By using the compiler directive
-eqc_fsm(external_fsm).
one can specify the state transition functions outside the actual callback module in a different module with same name as callback module and extension .fsm. This is useful when using a graphical editor to manipulate the state machine representation.

Data Types

callback_module()

callback_module() = atom()

The name of a module containing the eqc_fsm callbacks, as specified above.

command()

command() = eqc_statem:command()

As in eqc_statem.

dynamic_state()

dynamic_state() = any()

The type used by the callback module to represent the state of a test case during test execution. It is the same as symbolic_state(), except that symbolic variables and calls are replaced by their values.

flows()

flows() = [{float(), transition_pattern()}]

A list of transition patterns, paired with the proportion of executed transitions that match that pattern. The proportions sum to 1.

gen()

gen(A) = eqc_gen:gen(A)

As in eqc_gen.

pattern()

pattern() = any()

A term possibly containing the atom '_', which matches any similar term where occurrences of '_' may match any value.

state_data()

state_data() = any()

state_name()

state_name() = atom() | tuple()

transition_pattern()

transition_pattern() = {state_name(), state_name(), pattern()}

A pattern matching a transition from the first state to the second, making a symbolic call matching the pattern.

var()

var() = {var, integer()}

A symbolic variable, which is replace during test execution by the value bound by the corresponding command.

Function Index

automate_weights/1Computes an appropriate set of transition weights for the transitions in a callback module, using the priority callback to guide the distribution of transitions.
automate_weights/2Like automate_weights/1, but takes the image type as a parameter.
commands/1Generates a list of commands, just like eqc_statem:commands/1.
commands/2Generates a list of commands, starting from the given initial state with the given state data, just like eqc_statem:commands/2.
dot/1Visualizes the state graph of the callback module, creating a file M.dot which can be viewed with GraphViz.
parallel_commands/1Generate a parallel test case from the callbacks in the client module Mod.
parallel_commands/2Behaves like parallel_commands/1, but generates a test case starting in the state S.
run_commands/1Runs a list of commands generated using commands/1, just as does eqc_statem:run_commands/1.
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.
run_parallel_commands/1Runs a parallel test case, and returns the history of the prefix, each of the parallel tasks, and the overall result.
run_parallel_commands/2Like run_parallel_commands/1, but also takes an environment binding variables, like run_commands/2.
state_after/1Returns the symbolic state after a list of commands is run.
state_names/1Extracts the state names from a history.
visualize/1Visualizes the state graph of the callback module, and the transition frequencies.
visualize/2Like visualize/1, but takes the image type as a parameter.

Function Details

automate_weights/1

automate_weights(M::callback_module()) -> any()

Computes an appropriate set of transition weights for the transitions in a callback module, using the priority callback to guide the distribution of transitions. Outputs a definition of the weight callback that users can, if they wish, make use of by pasting the definition into their callback module. Generates a visualization of the resulting distribution of transitions in Mod.dot, which can be visualized using GraphViz. Displays the visualization immediately, if GraphViz and a JPEG viewer are available.

automate_weights/2

automate_weights(M::callback_module(), ImageType::atom()) -> any()

Like automate_weights/1, but takes the image type as a parameter. This permits generation of other image types than JPEG.

commands/1

commands(M::callback_module()) -> gen([command()])

Generates a list of commands, just like eqc_statem:commands/1. The form of commands generated is exactly the same.

commands/2

commands(M::callback_module(), InitS::{state_name(), any()}) -> gen([command()])

Generates a list of commands, starting from the given initial state with the given state data, just like eqc_statem:commands/2.

dot/1

dot(M::callback_module()) -> flows()

Visualizes the state graph of the callback module, creating a file M.dot which can be viewed with GraphViz. See visualize/1 for details.

parallel_commands/1

parallel_commands(Mod::atom()) -> gen(parallel_test_case())

Generate a parallel test case from the callbacks in the client module Mod. These test cases are used to test for race conditions that make the commands in the tests behave non-atomically. Blocking operations can be specified by defining the blocking/4 callback:

  blocking(From,To,S,Call) -> bool()
  
See the documentation of eqc_statem for details.

parallel_commands/2

parallel_commands(Mod::atom(), S::symbolic_state()) -> gen(parallel_test_case())

Behaves like parallel_commands/1, but generates a test case starting in the state S.

run_commands/1

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

Runs a list of commands generated using commands/1, just as does eqc_statem:run_commands/1. The result has the same form, except that the states are represented as pairs of state names and state data.

run_commands/2

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

Behaves like run_commands/1, but also takes an environment containing values for additional variables that may be referred to in test cases. Cf eqc_statem:run_commands/2.

run_parallel_commands/1

run_parallel_commands(ParCmds::parallel_test_case()) -> {command_history(), [command_history()], reason()}

Runs a parallel test case, and returns the history of the prefix, each of the parallel tasks, and the overall result.

run_parallel_commands/2

run_parallel_commands(ParCmds::parallel_test_case(), Env::[{atom(), term()}]) -> {command_history(), [command_history()], reason()}

Like run_parallel_commands/1, but also takes an environment binding variables, like run_commands/2.

state_after/1

state_after(Cmds::[command()]) -> symbolic_state()

Returns the symbolic state after a list of commands is run. The commands are not executed.

state_names/1

state_names(H::history()) -> [state_name()]

Extracts the state names from a history. This is useful in conjunction with eqc:aggregate/2.

To collect statistics on transitions together with their source states, use

aggregate(zip(state_names(H),command_names(Cmds)),...)
in your property.

visualize/1

visualize(M::callback_module()) -> ok

Visualizes the state graph of the callback module, and the transition frequencies. The graph is saved in a file M.dot, which can be viewed using GraphViz. If visualization tools are correctly installed, then a M.jpg file will also be generated, and opened in a JPEG viewer.

visualize/2

visualize(M::callback_module(), ImageType::atom()) -> ok

Like visualize/1, but takes the image type as a parameter. This permits generation of other image types than JPEG.


Generated by EDoc, Oct 26 2016, 18:41:58.