Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

405 lines (358 sloc) 17.53 kb
%%% Copyright 2010-2013 Manolis Papadakis <manopapad@gmail.com>,
%%% Eirini Arvaniti <eirinibob@gmail.com>
%%% and Kostis Sagonas <kostis@cs.ntua.gr>
%%%
%%% This file is part of PropEr.
%%%
%%% PropEr is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU General Public License as published by
%%% the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% PropEr is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%%% GNU General Public License for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>.
%%% @copyright 2010-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @author Eirini Arvaniti
%%% @doc 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. `{@module}' is
%%% closely related to {@link proper_statem} and is, in fact, implemented in
%%% terms of that. Testcases generated using `{@module}' will be on precisely
%%% the same form as testcases generated using {@link proper_statem}. The
%%% difference lies in the way the callback modules are specified.
%%% The relation between {@link proper_statem} and `{@module}' is similar
%%% to the one between `gen_server' and `gen_fsm' in OTP libraries.
%%%
%%% Due to name conflicts with functions automatically imported from
%%% {@link proper_statem}, a fully qualified call is needed in order to
%%% use the <a href="#index">API functions </a> of `{@module}'.
%%%
%%% === The states of the finite state machine ===
%%% Following the convention used in `gen_fsm behaviour', the state is
%%% separated into a `StateName::'{@type state_name()} and some
%%% `StateData::'{@type 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'.<br/>
%%% `StateData' can be an arbitrary term, but is usually a record.
%%%
%%% === Transitions between states ===
%%% A transition ({@type 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:
%%% <ul>
%%% <li> `initial_state() ::' {@type state_name()}
%%% <p>Specifies the initial state of the finite state machine. As with
%%% `proper_statem:initial_state/0', its result should be deterministic.
%%% </p></li>
%%% <li> `initial_state_data() ::' {@type state_data()}
%%% <p>Specifies what the state data should initially contain. Its result
%%% should be deterministic</p></li>
%%% <li> `StateName(S::'{@type state_data()}`) ::'
%%% `['{@type transition()}`]'
%%% <p>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 ({@type 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.<br/>
%%% 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'.</p></li>
%%% <li> `StateName(Attr1::term(), ..., AttrN::term(),
%%% S::'{@type state_data()}`) ::'
%%% `['{@type transition()}`]'
%%% <p>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.</p></li>
%%% <li> `weight(From::'{@type state_name()}`,
%%% Target::'{@type state_name()}`,
%%% Call::'{@type symb_call()}`) :: integer()'
%%% <p>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.</p></li>
%%% <li> `precondition(From::'{@type state_name()}`,
%%% Target::'{@type state_name()}`,
%%% StateData::'{@type state_data()}`,
%%% Call::'{@type symb_call()}`) :: boolean()'
%%% <p>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.</p></li>
%%% <li> `postcondition(From::'{@type state_name()}`,
%%% Target::'{@type state_name()}`,
%%% StateData::'{@type state_data()}`,
%%% Call::'{@type symb_call()}`,
%%% Res::'{@type result()}`) :: boolean()'
%%% <p>Similar to `proper_statem:postcondition/3'. Specifies the
%%% postcondition that should hold about the result `Res' of the evaluation
%%% of `Call'.</p></li>
%%% <li> `next_state_data(From::'{@type state_name()}`,
%%% Target::'{@type state_name()}`,
%%% StateData::'{@type state_data()}`,
%%% Res::'{@type result()}`,
%%% Call::'{@type symb_call()}`) ::'
%%% {@type state_data()}
%%% <p>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.</p></li>
%%% </ul>
%%%
%%% === 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).'''
%%% @end
-module(proper_fsm).
-export([behaviour_info/1]).
-export([commands/1, commands/2, run_commands/2, run_commands/3,
state_names/1]).
-export([command/1, precondition/2, next_state/3, postcondition/3]).
-export([target_states/4]).
-include("proper_internal.hrl").
%% -----------------------------------------------------------------------------
%% Type declarations
%% -----------------------------------------------------------------------------
-type symb_var() :: proper_statem:symb_var().
-type symb_call() :: proper_statem:symb_call().
-type fsm_result() :: proper_statem:statem_result().
-type state_name() :: atom() | tuple().
%% @type state_data()
-type state_data() :: term().
-type fsm_state() :: {state_name(),state_data()}.
-type transition() :: {state_name(),symb_call()}.
-type command() :: {'set',symb_var(),symb_call()}
| {'init',fsm_state()}.
-type command_list() :: [command()].
%% @type cmd_result()
-type cmd_result() :: term().
-type history() :: [{fsm_state(),cmd_result()}].
-type tmp_command() :: {'init',state()}
| {'set',symb_var(),symb_call()}.
-record(state, {name :: state_name(),
data :: state_data(),
mod :: mod_name()}).
-type state() :: #state{}.
%% -----------------------------------------------------------------------------
%% Proper_fsm behaviour
%% ----------------------------------------------------------------------------
%% @doc Specifies the callback functions that should be exported from a module
%% implementing the `proper_fsm' behaviour.
-spec behaviour_info('callbacks') -> [{fun_name(),arity()}].
behaviour_info(callbacks) ->
[{initial_state,0},
{initial_state_data,0},
{precondition,4},
{postcondition,5},
{next_state_data,5}];
behaviour_info(_Attribute) ->
undefined.
%% -----------------------------------------------------------------------------
%% API
%% -----------------------------------------------------------------------------
%% @doc 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 <br/>
%% `{Mod:initial_state/0, Mod:initial_state_data/0}'.
-spec commands(mod_name()) -> proper_types:type().
commands(Mod) ->
?LET([_|Cmds],
proper_statem:commands(?MODULE, initial_state(Mod)),
Cmds).
%% @doc Similar to {@link commands/1}, but generated command sequences always
%% start at a given state. In this case, the first command is always <br/>
%% `{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).
-spec commands(mod_name(), fsm_state()) -> proper_types:type().
commands(Mod, {Name,Data} = InitialState) ->
State = #state{name = Name, data = Data, mod = Mod},
?LET([_|Cmds],
proper_statem:commands(?MODULE, State),
[{init,InitialState}|Cmds]).
%% @doc Evaluates a given symbolic command sequence `Cmds' according to the
%% finite state machine specified in `Mod'. The result is a triple of the
%% form<br/> `{History, FsmState, Result}', similar to
%% {@link proper_statem:run_commands/2}.
-spec run_commands(mod_name(), command_list()) ->
{history(),fsm_state(),fsm_result()}.
run_commands(Mod, Cmds) ->
run_commands(Mod, Cmds, []).
%% @doc Similar to {@link run_commands/2}, but also accepts an environment
%% used for symbolic variable evaluation, exactly as described in
%% {@link proper_statem:run_commands/3}.
-spec run_commands(mod_name(), command_list(), proper_symb:var_values()) ->
{history(),fsm_state(),fsm_result()}.
run_commands(Mod, Cmds, Env) ->
Cmds1 = tmp_commands(Mod, Cmds),
{H,S,Res} = proper_statem:run_commands(?MODULE, Cmds1, Env),
History = [{{Name,Data},R} || {#state{name = Name, data = Data},R} <- H],
State = {S#state.name, S#state.data},
{History, State, Res}.
%% @doc Extracts the names of the states from a given command execution history.
%% It is useful in combination with functions such as {@link proper:aggregate/2}
%% in order to collect statistics about state transitions during command
%% execution.
-spec state_names(history()) -> [state_name()].
state_names(History) ->
[SName || {{SName,_},_Res} <- History].
%% -----------------------------------------------------------------------------
%% Proper_statem bahaviour callback functions
%% -----------------------------------------------------------------------------
-spec initial_state(mod_name()) -> state().
initial_state(Mod) ->
S_name = Mod:initial_state(),
S_data = Mod:initial_state_data(),
#state{name = S_name, data = S_data, mod = Mod}.
%% @private
-spec command(state()) -> proper_types:type().
command(#state{name = From, data = Data, mod = Mod}) ->
choose_transition(Mod, From, get_transitions(Mod, From, Data)).
%% @private
-spec precondition(state(), symb_call()) -> boolean().
precondition(#state{name = From, data = Data, mod = Mod}, Call) ->
Targets = target_states(Mod, From, Data, Call),
case [To || To <- Targets,
Mod:precondition(From, cook_history(From, To), Data, Call)] of
[] ->
false;
[_T] ->
true;
_ ->
io:format(
"\nError: The transition from \"~w\" state triggered by ~w "
"call leads to multiple target states.\nUse the precondition/5 "
"callback to specify which target state should be chosen.\n",
[From, get_mfa(Call)]),
erlang:error(too_many_targets)
end.
%% @private
-spec next_state(state(), symb_var() | cmd_result(), symb_call()) -> state().
next_state(S = #state{name = From, data = Data, mod = Mod} , Var, Call) ->
To = cook_history(From, transition_target(Mod, From, Data, Call)),
S#state{name = To,
data = Mod:next_state_data(From, To, Data, Var, Call)}.
%% @private
-spec postcondition(state(), symb_call(), cmd_result()) -> boolean().
postcondition(#state{name = From, data = Data, mod = Mod}, Call, Res) ->
To = cook_history(From, transition_target(Mod, From, Data, Call)),
Mod:postcondition(From, To, Data, Call, Res).
%% -----------------------------------------------------------------------------
%% Utility functions
%% -----------------------------------------------------------------------------
-spec tmp_commands(mod_name(), command_list()) -> [tmp_command()].
tmp_commands(Mod, Cmds) ->
case Cmds of
[{init, {Name,Data}}|Rest] ->
I = #state{name = Name, data = Data, mod = Mod},
[{init,I}|Rest];
Rest ->
I = initial_state(Mod),
[{init,I}|Rest]
end.
-spec get_transitions(mod_name(), state_name(), state_data()) ->
[transition()].
get_transitions(Mod, StateName, Data) ->
case StateName of
From when is_atom(From) ->
Mod:From(Data);
From when is_tuple(From) ->
Fun = element(1, From),
Args = tl(tuple_to_list(From)),
apply(Mod, Fun, Args ++ [Data])
end.
-spec choose_transition(mod_name(), state_name(), [transition()]) ->
proper_types:type().
choose_transition(Mod, From, T_list) ->
case is_exported(Mod, {weight,3}) of
false ->
choose_uniform_transition(T_list);
true ->
choose_weighted_transition(Mod, From, T_list)
end.
-spec choose_uniform_transition([transition()]) -> proper_types:type().
choose_uniform_transition(T_list) ->
List = [CallGen || {_,CallGen} <- T_list],
proper_types:safe_union(List).
-spec choose_weighted_transition(mod_name(), state_name(), [transition()]) ->
proper_types:type().
choose_weighted_transition(Mod, From, T_list) ->
List = [{Mod:weight(From, cook_history(From, To), CallGen), CallGen}
|| {To,CallGen} <- T_list],
proper_types:safe_weighted_union(List).
-spec cook_history(state_name(), state_name()) -> state_name().
cook_history(From, history) -> From;
cook_history(_, To) -> To.
-spec is_exported(mod_name(), {fun_name(),arity()}) -> boolean().
is_exported(Mod, Fun) ->
lists:member(Fun, Mod:module_info(exports)).
-spec transition_target(mod_name(), state_name(), state_data(), symb_call()) ->
state_name().
transition_target(Mod, From, Data, Call) ->
Targets = target_states(Mod, From, Data, Call),
[To] = [T || T <- Targets,
Mod:precondition(From, cook_history(From, T), Data, Call)],
To.
%% @private
-spec target_states(mod_name(), state_name(), state_data(), symb_call()) ->
[state_name()].
target_states(Mod, From, StateData, Call) ->
find_target(get_transitions(Mod, From, StateData), Call, []).
-spec find_target([transition()], symb_call(), [state_name()]) ->
[state_name()].
find_target([], _, Accum) -> Accum;
find_target(Transitions, Call, Accum) ->
[{Target,CallGen}|Rest] = Transitions,
case is_compatible(Call, CallGen) of
true -> find_target(Rest, Call, [Target|Accum]);
false -> find_target(Rest, Call, Accum)
end.
-spec is_compatible(symb_call(), symb_call()) -> boolean().
is_compatible({call,M,F,A1}, {call,M,F,A2})
when length(A1) =:= length(A2) ->
true;
is_compatible(_, _) ->
false.
-spec get_mfa(symb_call()) -> mfa().
get_mfa({call,M,F,A}) -> {M,F,length(A)}.
Jump to Line
Something went wrong with that request. Please try again.