Module proper_fsm

Description
Data Types
Function Index
Function Details

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

Version: Jun 20 2016 16:27: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:

initial_state() -> state_name()
Specifies the initial state of the finite state machine. As with proper_statem:initial_state/0, its result should be deterministic.
initial_state_data() :: state_data()
Specifies what the state data should initially contain. Its result should be deterministic
StateName(S::state_data()) :: [transition()]
There should be one instance of this function for each reachable state StateName of the finite state machine. In case StateName is a tuple the function takes a different form, described just below. The function returns a list of possible transitions (transition()) from the current state. At command generation time, the instance of this function with the same name as the current state's name is called to return the list of possible transitions. Then, PropEr will randomly choose a transition and, according to that, generate the next symbolic call to be included in the command sequence. However, before the call is actually included, a precondition that might impose constraints on StateData is checked.
Note also that PropEr detects transitions that would raise an exception of class <error> at generation time (not earlier) and does not choose them. This feature can be used to include conditional transitions that depend on the StateData.
StateName(Attr1::term(), ..., AttrN::term(), S::state_data()) :: [transition()]
There should be one instance of this function for each reachable state {StateName,Attr1,...,AttrN} of the finite state machine. The function has similar beaviour to StateName/1, described above.
weight(From::state_name(), Target::state_name(), Call::symbolic_call()) -> integer()
This is an optional callback. When it is not defined (or not exported), transitions are chosen with equal probability. When it is defined, it assigns an integer weight to transitions from From to Target triggered by symbolic call Call. In this case, each transition is chosen with probability proportional to the weight assigned.
precondition(From::state_name(), Target::state_name(), StateData::state_data(), Call::symbolic_call()) -> boolean()
Similar to proper_statem:precondition/2. Specifies the precondition that should hold about StateData so that Call can be included in the command sequence. In case precondition doesn't hold, a new transition is chosen using the appropriate StateName/1 generator. It is possible for more than one transitions to be triggered by the same symbolic call and lead to different target states. In this case, at most one of the target states may have a true precondition. Otherwise, PropEr will not be able to detect which transition was chosen and an exception will be raised.
postcondition(From::state_name(), Target::state_name(), StateData::state_data(), Call::symbolic_call(), Res::cmd_result()) -> boolean()
Similar to proper_statem:postcondition/3. Specifies the postcondition that should hold about the result Res of the evaluation of Call.
next_state_data(From::state_name(), Target::state_name(), StateData::state_data(), Res::cmd_result(), Call::symbolic_call()) -> state_data()
Similar to proper_statem:next_state/3. Specifies how the transition from FromState to Target triggered by Call affects the StateData. Res refers to the result of Call and can be either symbolic or dynamic.

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, symbolic_var(), symbolic_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()}

history()

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

mod_name()

mod_name() = atom()

state_data()

abstract datatype: state_data()

state_name()

state_name() = atom() | tuple()

symbolic_call()

symbolic_call() = proper_statem:symbolic_call()

symbolic_var()

symbolic_var() = proper_statem:symbolic_var()

Function Index

commands/1	A special PropEr type which generates random command sequences, according to a finite state machine specification.
commands/2	Similar to `commands/1`, but generated command sequences always start at a given state.
run_commands/2	Evaluates a given symbolic command sequence `Cmds` according to the finite state machine specified in `Mod`.
run_commands/3	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	Extracts the names of the states from a given command execution history.

Function Details

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, Jun 20 2016, 16:27:12.