Module proper_fsm

This module defines the proper_fsm behaviour, useful for testing systems that can be modeled as finite state machines.

Copyright 2010-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas

Version: Apr 3 2013 10:43:12

Authors: Eirini Arvaniti.

Description

This module defines the proper_fsm behaviour, useful for testing systems that can be modeled as finite state machines. That is, a finite collection of named states and transitions between them. proper_fsm is closely related to proper_statem and is, in fact, implemented in terms of that. Testcases generated using proper_fsm will be on precisely the same form as testcases generated using proper_statem. The difference lies in the way the callback modules are specified. The relation between proper_statem and proper_fsm is similar to the one between gen_server and gen_fsm in OTP libraries.

Due to name conflicts with functions automatically imported from proper_statem, a fully qualified call is needed in order to use the API functions of proper_fsm.

The states of the finite state machine

Following the convention used in gen_fsm behaviour, the state is separated into a StateName::state_name() and some StateData::state_data(). StateName is used to denote a state of the finite state machine and StateData is any relevant information that has to be stored in the model state. States are fully represented as tuples {StateName, StateData}.

StateName is usually an atom (i.e. the name of the state), but can also be a tuple. In the latter case, the first element of the tuple must be an atom specifying the name of the state, whereas the rest of the elements can be arbitrary terms specifying state attributes. For example, when implementing the fsm of an elevator which can reach N different floors, the StateName for each floor could be {floor,K}, 1 <= K <= N.
StateData can be an arbitrary term, but is usually a record.

Transitions between states

A transition (transition()) is represented as a tuple {TargetState, {call,M,F,A}}. This means that performing the specified symbolic call at the current state of the fsm will lead to TargetState. The atom history can be used as TargetState to denote that a transition does not change the current state of the fsm.

The callback functions

The following functions must be exported from the callback module implementing the finite state machine:

The property used

This is an example of a property that can be used to test a finite state machine specification:

      prop_fsm() ->
          ?FORALL(Cmds, proper_fsm:commands(?MODULE),
                  begin
                      {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds),
                      cleanup(),
                      Result =:= ok
                  end).

Data Types

cmd_result()

abstract datatype: cmd_result()

command()

command() = {set, symb_var(), symb_call()}
          | {init, fsm_state()}

command_list()

command_list() = [command()]

fsm_result()

fsm_result() = proper_statem:statem_result()

fsm_state()

fsm_state() = {state_name(), state_data()}

fun_name()

fun_name() = atom()

history()

history() = [{fsm_state(), cmd_result()}]

mod_name()

mod_name() = atom()

state_data()

abstract datatype: state_data()

state_name()

state_name() = atom() | tuple()

symb_call()

symb_call() = proper_statem:symb_call()

symb_var()

symb_var() = proper_statem:symb_var()

Function Index

behaviour_info/1Specifies the callback functions that should be exported from a module implementing the proper_fsm behaviour.
commands/1A special PropEr type which generates random command sequences, according to a finite state machine specification.
commands/2Similar to commands/1, but generated command sequences always start at a given state.
run_commands/2Evaluates a given symbolic command sequence Cmds according to the finite state machine specified in Mod.
run_commands/3Similar to run_commands/2, but also accepts an environment used for symbolic variable evaluation, exactly as described in proper_statem:run_commands/3.
state_names/1Extracts the names of the states from a given command execution history.

Function Details

behaviour_info/1

behaviour_info(Attribute :: callbacks) -> [{fun_name(), arity()}]

Specifies the callback functions that should be exported from a module implementing the proper_fsm behaviour.

commands/1

commands(Mod :: mod_name()) -> proper_types:type()

A special PropEr type which generates random command sequences, according to a finite state machine specification. The function takes as input the name of a callback module, which contains the fsm specification. The initial state is computed by
{Mod:initial_state/0, Mod:initial_state_data/0}.

commands/2

commands(Mod :: mod_name(), InitialState :: fsm_state()) ->
            proper_types:type()

Similar to commands/1, but generated command sequences always start at a given state. In this case, the first command is always
{init, InitialState = {Name,Data}} and is used to correctly initialize the state every time the command sequence is run (i.e. during normal execution, while shrinking and when checking a counterexample).

run_commands/2

run_commands(Mod :: mod_name(), Cmds :: command_list()) ->
                {history(), fsm_state(), fsm_result()}

Evaluates a given symbolic command sequence Cmds according to the finite state machine specified in Mod. The result is a triple of the form
{History, FsmState, Result}, similar to proper_statem:run_commands/2.

run_commands/3

run_commands(Mod :: mod_name(),
             Cmds :: command_list(),
             Env :: proper_symb:var_values()) ->
                {history(), fsm_state(), fsm_result()}

Similar to run_commands/2, but also accepts an environment used for symbolic variable evaluation, exactly as described in proper_statem:run_commands/3.

state_names/1

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

Extracts the names of the states from a given command execution history. It is useful in combination with functions such as proper:aggregate/2 in order to collect statistics about state transitions during command execution.


Generated by EDoc, Apr 3 2013, 10:43:12.