%%% Copyright 2010-2011 Manolis Papadakis , %%% Eirini Arvaniti %%% and Kostis Sagonas %%% %%% 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 . %%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas %%% @version {@version} %%% @author Eirini Arvaniti %%% @doc This module defines the `proper_statem' behaviour, useful for testing %%% stateful reactive systems whose internal state and side-effects are %%% specified via an abstract state machine. Given a callback module %%% implementing the `proper_statem' behaviour (i.e. defining an abstract state %%% machine of the system under test), PropEr can generate random symbolic %%% sequences of calls to that system. %%% As a next step, generated symbolic calls are actually performed, while %%% monitoring the system's responses to ensure it behaves as expected. Upon %%% failure, the shrinking mechanism attempts to find a minimal sequence of %%% calls provoking the same error. %%% %%% When including the "proper/include/proper.hrl" header file, %%% all API functions of {@module} are automatically %%% imported, unless `PROPER_NO_IMPORTS' is defined. %%% %%% === The role of commands === %%% Testcases generated for testing a stateful system are lists of symbolic API %%% calls to that system. Symbolic representation has several benefits, which %%% are listed here in increasing order of importance: %%%
    %%%
  • Generated testcases are easier to read and understand.
    • %%%
  • Failing testcases are easier to shrink.
    • %%%
  • The generation phase is side-effect free and this results in %%% repeatable testcases, which is essential for correct shrinking.
    • %%%
%%% Since the actual results of symbolic calls are not known at generation time, %%% we use symbolic variables ({@type symb_var()}) to refer to them. %%% A command ({@type command()}) is a symbolic term, used to bind a symbolic %%% variable to the result of a symbolic call. For example: %%% %%% ```[{set, {var,1}, {call,erlang,put,[a,42]}}, %%% {set, {var,2}, {call,erlang,erase,[a]}}, %%% {set, {var,3}, {call,erlang,put,[b,{var,2}]}}]''' %%% %%% is a command sequence that could be used to test the process dictionary. %%% In this example, the first call stores the pair `{a,42}' in the process %%% dictionary, while the second one deletes it. Then, a new pair `{b,{var,2}}' %%% is stored. `{var,2}' is a symbolic variable bound to the result of %%% `erlang:erase/1'. This result is not known at generation time, since none of %%% these operations is performed at that time. After evaluating the command %%% sequence at runtime, the process dictionary will eventually contain the %%% pair `{b,42}'. %%% %%% === The abstract model-state === %%% In order to be able to test impure code, we need a way to track its %%% internal state (at least the useful part of it). To this end, we use an %%% abstract state machine representing the possible configurations of the %%% system under test. When referring to the model state, we mean the %%% state of the abstract state machine. The model state can be either %%% symbolic or dynamic: %%%
    %%%
  • During command generation, we use symbolic variables to bind the %%% results of symbolic calls. Therefore, the model state might %%% (and usually does) contain symbolic variables and/or symbolic calls, which %%% are necessary to operate on symbolic variables. Thus, we refer to it as %%% symbolic state. For example, assuming that the internal state of the %%% process dictionary is modeled as a proplist, the model state after %%% generating the previous command sequence will be `[{b,{var,2}}]'.
    • %%%
  • During runtime, symbolic calls are evaluated and symbolic variables are %%% replaced by their corresponding real values. Now we refer to the state as %%% dynamic state. After running the previous command sequence, the model state %%% will be `[{b,42}]'.
    • %%%
%%% %%% === The callback functions === %%% The following functions must be exported from the callback module %%% implementing the abstract state machine: %%%
    %%%
  • `initial_state() ::' {@type symbolic_state()} %%%

    Specifies the symbolic initial state of the state machine. This state %%% will be evaluated at command execution time to produce the actual initial %%% state. The function is not only called at command generation time, but %%% also in order to initialize the state every time the command sequence is %%% run (i.e. during normal execution, while shrinking and when checking a %%% counterexample). For this reason, it should be deterministic and %%% self-contained.

    • %%%
  • `command(S::'{@type symbolic_state()}`) ::' {@type proper_types:type()} %%%

    Generates a symbolic call to be included in the command sequence, %%% given the current state `S' of the abstract state machine. However, %%% before the call is actually included, a precondition is checked. This %%% function will be repeatedly called to produce the next call to be %%% included in the test case.

    • %%%
  • `precondition(S::'{@type symbolic_state()}`, %%% Call::'{@type symb_call()}`) :: boolean()' %%%

    Specifies the precondition that should hold so that `Call' can be %%% included in the command sequence, given the current state `S' of the %%% abstract state machine. In case precondition doesn't hold, a new call is %%% chosen using the `command/1' generator. If preconditions are very strict, %%% it will take a lot of tries for PropEr to randomly choose a valid command. %%% Testing will be stopped in case the `constraint_tries' limit is reached %%% (see the 'Options' section in the {@link proper} module documentation). %%% Preconditions are also important for correct shrinking of failing %%% testcases. When shrinking command sequences, we try to eliminate commands %%% that do not contribute to failure, ensuring that all preconditions still %%% hold. Validating preconditions is necessary because during shrinking we %%% usually attempt to perform a call with the system being in a state %%% different from the state it was when initially running the test.

    • %%%
  • `postcondition(S::'{@type dynamic_state()}`, %%% Call::'{@type symbolic_call()}`, %%% Res::term()) :: boolean()' %%%

    Specifies the postcondition that should hold about the result `Res' of %%% performing `Call', given the dynamic state `S' of the abstract state %%% machine prior to command execution. This function is called during %%% runtime, this is why the state is dynamic.

    • %%%
  • `next_state(S::'{@type symbolic_state()} `|' {@type dynamic_state()}`, %%% Res::term(), %%% Call::'{@type symbolic_call()}`) ::' %%% {@type symbolic_state()} `|' {@type dynamic_state()} %%%

    Specifies the next state of the abstract state machine, given the %%% current state `S', the symbolic `Call' chosen and its result `Res'. This %%% function is called both at command generation and command execution time %%% in order to update the model state, therefore the state `S' and the %%% result `Res' can be either symbolic or dynamic.

    • %%%
%%% %%% === The property used === %%% Each test consists of two phases: %%%
    %%%
  • As a first step, PropEr generates random symbolic command sequences %%% deriving information from the callback module implementing the abstract %%% state machine. This is the role of {@link commands/1} generator.
    • %%%
  • As a second step, command sequences are executed so as to check that %%% the system behaves as expected. This is the role of %%% {@link run_commands/2}, a function that evaluates a symbolic command %%% sequence according to an abstract state machine specification.
    • %%%
%%% %%% These two phases are encapsulated in the following property, which can be %%% used for testing the process dictionary: %%% %%% ```prop_pdict() -> %%% ?FORALL(Cmds, proper_statem:commands(?MODULE), %%% begin %%% {_History, _State, Result} = proper_statem:run_commands(?MODULE, Cmds), %%% cleanup(), %%% Result =:= ok %%% end).''' %%% %%% When testing impure code, it is very important to keep each test %%% self-contained. For this reason, almost every property for testing stateful %%% systems contains some clean-up code. Such code is necessary to put the %%% system in a known state, so that the next test can be executed %%% independently from previous ones. %%% %%% == Parallel testing == %%% After ensuring that a system's behaviour can be described via an abstract %%% state machine when commands are executed sequentially, it is possible to %%% move to parallel testing. The same state machine can be used to generate %%% command sequences that will be executed in parallel to test for race %%% conditions. A parallel testcase ({@type parallel_testcase()}) consists of %%% a sequential and a parallel component. The sequential component is a %%% command sequence that is run first to put the system in a random state. %%% The parallel component is a list containing 2 command sequences to be %%% executed in parallel, each of them in a separate newly-spawned process. %%% %%% Generating parallel test cases involves the following actions. Initially, %%% we generate a command sequence deriving information from the abstract %%% state machine specification, as in the case of sequential statem testing. %%% Then, we parallelize a random suffix (up to 12 commands) of the initial %%% sequence by splitting it into 2 subsequences that will be executed %%% concurrently. Limitations arise from the fact that each subsequence should %%% be a valid command sequence (i.e. all commands should satisfy %%% preconditions and use only symbolic variables bound to the results of %%% preceding calls in the same sequence). Furthermore, we apply an additional %%% check: we have to ensure that preconditions are satisfied in all possible %%% interleavings of the concurrent tasks. Otherwise, an exception might be %%% raised during parallel execution and lead to unexpected (and unwanted) test %%% failure. In case these constraints cannot be satisfied for a specific test %%% case, the test case will be executed sequentially. Then an `f' is printed %%% on screen to inform the user. This usually means that preconditions need %%% to become less strict for parallel testing to work. %%% %%% After running a parallel testcase, PropEr uses the state machine %%% specification to check if the results observed could have been produced by %%% a possible serialization of the parallel component. If no such serialization %%% is possible, then an atomicity violation has been detected. In this case, %%% the shrinking mechanism attempts to produce a counterexample that is minimal %%% in terms of concurrent operations. Properties for parallel testing are very %%% similar to those used for sequential testing. %%% %%% ```prop_parallel_testing() -> %%% ?FORALL(Testcase, proper_statem:parallel_commands(?MODULE), %%% begin %%% {_Sequential, _Parallel, Result} = proper_statem:run_parallel_commands(?MODULE, Testcase), %%% cleanup(), %%% Result =:= ok %%% end).''' %%% %%% Please note that the actual interleaving of commands of the parallel %%% component depends on the Erlang scheduler, which is too deterministic. %%% For PropEr to be able to detect race conditions, the code of the system %%% under test should be instrumented with `erlang:yield/0' calls to the %%% scheduler. %%% @end -module(proper_statem). -export([behaviour_info/1]). -export([commands/1, commands/2, parallel_commands/1, parallel_commands/2, more_commands/2]). -export([run_commands/2, run_commands/3, run_parallel_commands/2, run_parallel_commands/3]). -export([state_after/2, command_names/1, zip/2]). -include("proper_internal.hrl"). -define(WORKERS, 2). -define(LIMIT, 12). %% ----------------------------------------------------------------------------- %% Exported only for testing purposes %% ----------------------------------------------------------------------------- -export([index/2, all_insertions/3, insert_all/2]). -export([is_valid/4, args_defined/2]). -export([get_next/6, mk_first_comb/3, fix_parallel/8, mk_dict/2]). -export([execute/4, check/6, run/3, get_initial_state/2]). %% ----------------------------------------------------------------------------- %% Type declarations %% ----------------------------------------------------------------------------- %% @type symbolic_state() -type symbolic_state() :: term(). %% @type dynamic_state() -type dynamic_state() :: term(). -type symb_var() :: {'var',pos_integer()}. -type symb_call() :: {'call',mod_name(),fun_name(),[term()]}. -type command() :: {'set',symb_var(),symb_call()} | {'init',symbolic_state()}. -type command_list() :: [command()]. -type parallel_testcase() :: {command_list(),[command_list()]}. -type parallel_history() :: [{command(),term()}]. -type history() :: [{dynamic_state(),term()}]. -type statem_result() :: 'ok' | 'initialization_error' | {'precondition', 'false' | proper:exception()} | {'postcondition', 'false' | proper:exception()} | proper:exception() | 'no_possible_interleaving'. -type indices() :: [pos_integer()]. -type combination() :: [{pos_integer(),indices()}]. -type lookup() :: orddict:orddict(). -export_type([symb_var/0, symb_call/0, statem_result/0]). %% ----------------------------------------------------------------------------- %% Proper_statem behaviour %% ---------------------------------------------------------------------------- %% @doc Specifies the callback functions that should be exported from a module %% implementing the `proper_statem' behaviour. -spec behaviour_info('callbacks') -> [{fun_name(),arity()}]. behaviour_info(callbacks) -> [{initial_state,0}, {command,1}, {precondition,2}, {postcondition,3}, {next_state,3}]; behaviour_info(_Attribute) -> undefined. %% ----------------------------------------------------------------------------- %% Sequential command generation %% ----------------------------------------------------------------------------- %% @doc A special PropEr type which generates random command sequences, %% according to an absract state machine specification. The function takes as %% input the name of a callback module, which contains the state machine %% specification. The initial state is computed by `Mod:initial_state/0'. -spec commands(mod_name()) -> proper_types:type(). commands(Mod) -> ?LET(InitialState, ?LAZY(Mod:initial_state()), ?SUCHTHAT( Cmds, ?LET(List, ?SIZED(Size, proper_types:noshrink( commands(Size, Mod, InitialState, 1))), proper_types:shrink_list(List)), is_valid(Mod, InitialState, 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 %% `{init,InitialState}' 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). In this case, %% `Mod:initial_state/0' is never called. -spec commands(mod_name(), symbolic_state()) -> proper_types:type(). commands(Mod, InitialState) -> ?SUCHTHAT( Cmds, ?LET(CmdTail, ?LET(List, ?SIZED(Size, proper_types:noshrink( commands(Size, Mod, InitialState, 1))), proper_types:shrink_list(List)), [{init,InitialState}|CmdTail]), is_valid(Mod, InitialState, Cmds, [])). -spec commands(size(), mod_name(), symbolic_state(), pos_integer()) -> proper_types:type(). commands(Size, Mod, State, Count) -> ?LAZY( proper_types:frequency( [{1, []}, {Size, ?LET(Call, ?SUCHTHAT(X, Mod:command(State), Mod:precondition(State, X)), begin Var = {var,Count}, NextState = Mod:next_state(State, Var, Call), ?LET( Cmds, commands(Size-1, Mod, NextState, Count+1), [{set,Var,Call}|Cmds]) end)}])). %% @doc Increases the expected length of command sequences generated from %% `CmdType' by a factor `N'. -spec more_commands(pos_integer(), proper_types:type()) -> proper_types:type(). more_commands(N, CmdType) -> ?SIZED(Size, proper_types:resize(Size * N, CmdType)). %% ----------------------------------------------------------------------------- %% Parallel command generation %% ----------------------------------------------------------------------------- %% @doc A special PropEr type which generates parallel testcases, %% according to an absract state machine specification. The function takes as %% input the name of a callback module, which contains the state machine %% specification. The initial state is computed by `Mod:initial_state/0'. -spec parallel_commands(mod_name()) -> proper_types:type(). parallel_commands(Mod) -> ?LET({ShrunkSeq, ShrunkPar}, ?LET({Seq, Par}, proper_types:noshrink(parallel_gen(Mod)), parallel_shrinker(Mod, Seq, Par)), move_shrinker(ShrunkSeq, ShrunkPar, ?WORKERS)). %% @doc Similar to {@link parallel_commands/1}, but generated command sequences %% always start at a given state. -spec parallel_commands(mod_name(), symbolic_state()) -> proper_types:type(). parallel_commands(Mod, InitialState) -> ?LET({ShrunkSeq, ShrunkPar}, ?LET({Seq, Par}, proper_types:noshrink(parallel_gen(Mod, InitialState)), parallel_shrinker(Mod, Seq, Par)), move_shrinker(ShrunkSeq, ShrunkPar, ?WORKERS)). -spec parallel_gen(mod_name()) -> proper_types:type(). parallel_gen(Mod) -> ?LET(Seq, commands(Mod), mk_parallel_testcase(Mod, Seq)). -spec parallel_gen(mod_name(), symbolic_state()) -> proper_types:type(). parallel_gen(Mod, InitialState) -> ?LET(Seq, commands(Mod, InitialState), mk_parallel_testcase(Mod, Seq)). -spec mk_parallel_testcase(mod_name(), command_list()) -> proper_types:type(). mk_parallel_testcase(Mod, Seq) -> {State, SymbEnv} = state_env_after(Mod, Seq), Count = case SymbEnv of [] -> 1; [{var,N}|_] -> N + 1 end, ?LET(Parallel, ?SUCHTHAT(C, commands(?LIMIT, Mod, State, Count), length(C) > ?WORKERS), begin LenPar = length(Parallel), Len = LenPar div ?WORKERS, Comb = mk_first_comb(LenPar, Len, ?WORKERS), LookUp = orddict:from_list(mk_dict(Parallel, 1)), {Seq, fix_parallel(LenPar, Len, Comb, LookUp, Mod, State, SymbEnv, ?WORKERS)} end). -spec parallel_shrinker(mod_name(), command_list(), [command_list()]) -> proper_types:type(). parallel_shrinker(Mod, [{init,I} = Init|Seq], Parallel) -> ?SUCHTHAT({Seq1, Parallel1}, ?LET(ParInstances, [proper_types:shrink_list(P) || P <- Parallel], ?LET(SeqInstance, proper_types:shrink_list(Seq), {[Init|SeqInstance], ParInstances})), lists:all( fun(P) -> is_valid(Mod, I, Seq1 ++ P, []) end, Parallel1)); parallel_shrinker(Mod, Seq, Parallel) -> I= Mod:initial_state(), ?SUCHTHAT({Seq1, Parallel1}, ?LET(ParInstances, [proper_types:shrink_list(P) || P <- Parallel], ?LET(SeqInstance, proper_types:shrink_list(Seq), {SeqInstance, ParInstances})), lists:all( fun(P) -> is_valid(Mod, I, Seq1 ++ P, []) end, Parallel1)). -spec move_shrinker(command_list(), [command_list()], pos_integer()) -> proper_types:type(). move_shrinker(Seq, Par, 1) -> ?SHRINK({Seq, Par}, [{Seq ++ Slice, remove_slice(1, Slice, Par)} || Slice <- get_slices(lists:nth(1, Par))]); move_shrinker(Seq, Par, I) -> ?LET({NewSeq, NewPar}, ?SHRINK({Seq, Par}, [{Seq ++ Slice, remove_slice(I, Slice, Par)} || Slice <- get_slices(lists:nth(I, Par))]), move_shrinker(NewSeq, NewPar, I-1)). %% ----------------------------------------------------------------------------- %% Sequential command execution %% ----------------------------------------------------------------------------- %% @doc Evaluates a given symbolic command sequence `Cmds' according to the %% state machine specified in `Mod'. The result is a triple of the form
%% `{History, DynamicState, Result}', where: %%
    %%
  • `History' contains the execution history of all commands that were %% executed without raising an exception. It contains tuples of the form %% {{@type dynamic_state()}, {@type term()}}, specifying the state prior to %% command execution and the actual result of the command.
    • %%
  • `DynamicState' contains the state of the abstract state machine at %% the moment when execution stopped.
    • %%
  • `Result' specifies the outcome of command execution. It can be %% classified in one of the following categories: %%
      %%
    • ok %%

      All commands were successfully run and all postconditions were true. %%

      • %%
    • initialization error %%

      There was an error while evaluating the initial state.

      • %%
    • postcondition error %%

      A postcondition was false or raised an exception.

      • %%
    • precondition error %%

      A precondition was false or raised an exception.

      • %%
    • exception %%

      An exception was raised while running a command.

      • %%
    • %%
-spec run_commands(mod_name(), command_list()) -> {history(),dynamic_state(),statem_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 during command execution. The %% environment consists of `{Key::atom(), Value::term()}' pairs. Keys may be %% used in symbolic variables (i.e. `{var,Key}') whithin the command sequence %% `Cmds'. These symbolic variables will be replaced by their corresponding %% `Value' during command execution. -spec run_commands(mod_name(), command_list(), proper_symb:var_values()) -> {history(),dynamic_state(),statem_result()}. run_commands(Mod, Cmds, Env) -> element(1, run(Mod, Cmds, Env)). %% @private -spec run(mod_name(), command_list(), proper_symb:var_values()) -> {{history(),dynamic_state(),statem_result()}, proper_symb:var_values()}. run(Mod, Cmds, Env) -> InitialState = get_initial_state(Mod, Cmds), try proper_symb:eval(Env, InitialState) of DynState -> run_commands(Cmds, Env, Mod, [], DynState) catch _Exc:_Reason -> {{[], undefined, initialization_error}, []} end. -spec run_commands(command_list(), proper_symb:var_values(), mod_name(), history(), dynamic_state()) -> {{history(),dynamic_state(),statem_result()}, proper_symb:var_values()}. run_commands(Cmds, Env, Mod, History, State) -> case Cmds of [] -> {{lists:reverse(History), State, ok}, Env}; [{init,_S}|Rest] -> run_commands(Rest, Env, Mod, History, State); [{set, {var,V}, {call,M,F,A}}|Rest] -> M2 = proper_symb:eval(Env, M), F2 = proper_symb:eval(Env, F), A2 = proper_symb:eval(Env, A), Call = {call,M2,F2,A2}, case check_precondition(Mod, State, Call) of true -> case safe_apply(M2, F2, A2) of {ok,Res} -> Env2 = [{V,Res}|Env], History2 = [{State,Res}|History], case check_postcondition(Mod, State, Call, Res) of true -> State2 = proper_symb:eval(Env2, Mod:next_state(State, Res, Call)), run_commands(Rest, Env2, Mod, History2, State2); false -> {{lists:reverse(History2), State, {postcondition,false}}, []}; {exception,_,_,_} = Exception -> {{lists:reverse(History2), State, {postcondition,Exception}}, []} end; {error,Exception} -> {{lists:reverse(History), State, Exception}, []} end; false -> {{lists:reverse(History), State, {precondition,false}}, []}; {exception,_,_,_} = Exc -> {{lists:reverse(History), State, {precondition,Exc}}, []} end end. -spec check_precondition(mod_name(), dynamic_state(), symb_call()) -> boolean() | proper:exception(). check_precondition(Mod, State, Call) -> try Mod:precondition(State, Call) catch Kind:Reason -> {exception, Kind, Reason, erlang:get_stacktrace()} end. -spec check_postcondition(mod_name(), dynamic_state(), symb_call(), term()) -> boolean() | proper:exception(). check_postcondition(Mod, State, Call, Res) -> try Mod:postcondition(State, Call, Res) catch Kind:Reason -> {exception, Kind, Reason, erlang:get_stacktrace()} end. -spec safe_apply(mod_name(), fun_name(), [term()]) -> {'ok', term()} | {'error', proper:exception()}. safe_apply(M, F, A) -> try apply(M, F, A) of Result -> {ok, Result} catch Kind:Reason -> {error, {exception, Kind, Reason, erlang:get_stacktrace()}} end. %% ----------------------------------------------------------------------------- %% Parallel command execution %% ----------------------------------------------------------------------------- %% @doc Runs a given parallel testcase according to the state machine %% specified in `Mod'. The result is a triple of the form
%% `@{Sequential_history, Parallel_history, Result@}', where: %%
    %%
  • `Sequential_history' contains the execution history of the %% sequential component.
    • %%
  • `Parallel_history' contains the execution history of each of the %% concurrent tasks.
    • %%
  • `Result' specifies the outcome of the attemp to serialize command %% execution, based on the results observed. It can be one of the following: %%
    • `ok'
    • `no_possible_interleaving'
    • %%
-spec run_parallel_commands(mod_name(), parallel_testcase()) -> {history(),[parallel_history()],statem_result()}. run_parallel_commands(Mod, {_Sequential, _Parallel} = Testcase) -> run_parallel_commands(Mod, Testcase, []). %% @doc Similar to {@link run_parallel_commands/2}, but also accepts an %% environment used for symbolic variable evaluation, exactly as described in %% {@link run_commands/3}. -spec run_parallel_commands(mod_name(), parallel_testcase(), proper_symb:var_values()) -> {history(),[parallel_history()],statem_result()}. run_parallel_commands(Mod, {Sequential, Parallel}, Env) -> case run(Mod, Sequential, Env) of {{Seq_history, State, ok}, SeqEnv} -> F = fun(T) -> execute(T, SeqEnv, Mod, []) end, Parallel_history = pmap(F, Parallel), case check(Mod, State, SeqEnv, false, [], Parallel_history) of true -> {Seq_history, Parallel_history, ok}; false -> {Seq_history, Parallel_history, no_possible_interleaving} end; {{Seq_history, _, Res}, _} -> {Seq_history, [], Res} end. %% @private -spec execute(command_list(), proper_symb:var_values(), mod_name(), parallel_history()) -> parallel_history(). execute(Cmds, Env, Mod, History) -> case Cmds of [] -> lists:reverse(History); [{set, {var,V}, {call,M,F,A}} = Cmd|Rest] -> M2 = proper_symb:eval(Env, M), F2 = proper_symb:eval(Env, F), A2 = proper_symb:eval(Env, A), Res = apply(M2, F2, A2), Env2 = [{V,Res}|Env], History2 = [{Cmd,Res}|History], execute(Rest, Env2, Mod, History2) end. -spec pmap(fun((command_list()) -> parallel_history()), [command_list()]) -> [parallel_history()]. pmap(F, L) -> await(lists:reverse(spawn_jobs(F,L))). -spec spawn_jobs(fun((command_list()) -> parallel_history()), [command_list()]) -> [pid()]. spawn_jobs(F, L) -> Parent = self(), [spawn_link_cp(fun() -> Parent ! {self(),catch {ok,F(X)}} end) || X <- L]. -spec await([pid()]) -> [parallel_history()]. await(Pids) -> await_tr(Pids, []). -spec await_tr([pid()], [parallel_history()]) -> [parallel_history()]. await_tr([], Acc) -> Acc; await_tr([H|T], Acc) -> receive {H, {ok, Res}} -> await_tr(T, [Res|Acc]); {H, {'EXIT',_} = Err} -> _ = [exit(Pid, kill) || Pid <- T], _ = [receive {P,_} -> d_ after 0 -> i_ end || P <- T], erlang:error(Err) end. %% @private -spec check(mod_name(), dynamic_state(), proper_symb:var_values(), boolean(), [parallel_history()], [parallel_history()]) -> boolean(). check(_Mod, _State, _Env, _Changed, [], []) -> true; check(_Mod, _State, _Env, false, _Tried, []) -> false; check(Mod, State, Env, true, Tried, []) -> check(Mod, State, Env, false, [], Tried); check(Mod, State, Env, Changed, Tried, [P|ToTry]) -> case P of [] -> check(Mod, State, Env, Changed, Tried, ToTry); [H|Tail] -> {{set, {var,N}, {call,M,F,A}}, Res} = H, M_ = proper_symb:eval(Env, M), F_ = proper_symb:eval(Env, F), A_ = proper_symb:eval(Env, A), Call = {call,M_,F_,A_}, case Mod:postcondition(State, Call, Res) of true -> Env2 = [{N, Res}|Env], NextState = proper_symb:eval( Env2, Mod:next_state(State, Res, Call)), check(Mod, NextState, Env2, true, Tried, [Tail|ToTry]) orelse check(Mod, State, Env, Changed, [P|Tried], ToTry); false -> check(Mod, State, Env, Changed, [P|Tried], ToTry) end end. %% ----------------------------------------------------------------------------- %% Other API functions %% ----------------------------------------------------------------------------- %% @doc Extracts the names of the commands from a given command sequence, in %% the form of MFAs. It is useful in combination with functions such as %% {@link proper:aggregate/2} in order to collect statistics about command %% execution. -spec command_names(command_list()) -> [mfa()]. command_names(Cmds) -> [{M, F, length(Args)} || {set, _Var, {call,M,F,Args}} <- Cmds]. %% @doc Returns the symbolic state after running a given command sequence, %% according to the state machine specification found in `Mod'. The commands %% are not actually executed. -spec state_after(mod_name(), command_list()) -> symbolic_state(). state_after(Mod, Cmds) -> element(1, state_env_after(Mod, Cmds)). -spec state_env_after(mod_name(), command_list()) -> {symbolic_state(), [symb_var()]}. state_env_after(Mod, Cmds) -> lists:foldl(fun({init,S}, _) -> {S, []}; ({set,Var,Call}, {S,Vars}) -> {Mod:next_state(S, Var, Call), [Var|Vars]} end, {get_initial_state(Mod, Cmds), []}, Cmds). %% @doc Behaves like `lists:zip/2', but the input lists do no not necessarily %% have equal length. Zipping stops when the shortest list stops. This is %% useful for zipping a command sequence with its (failing) execution history. -spec zip([A], [B]) -> [{A,B}]. zip(X, Y) -> zip(X, Y, []). -spec zip([A], [B], [{A,B}]) -> [{A,B}]. zip([], _, Accum) -> lists:reverse(Accum); zip(_, [], Accum) -> lists:reverse(Accum); zip([X|Tail1], [Y|Tail2], Accum) -> zip(Tail1, Tail2, [{X,Y}|Accum]). %% ----------------------------------------------------------------------------- %% Utility functions %% ----------------------------------------------------------------------------- %% @private -spec is_valid(mod_name(), symbolic_state(), command_list(), [symb_var()]) -> boolean(). is_valid(_Mod, _State, [], _SymbEnv) -> true; is_valid(Mod, _State, [{init,S}|Cmds], _SymbEnv) -> is_valid(Mod, S, Cmds, _SymbEnv); is_valid(Mod, State, [{set, Var, {call,_M,_F,A} = Call}|Cmds], SymbEnv) -> args_defined(A, SymbEnv) andalso Mod:precondition(State, Call) andalso is_valid(Mod, Mod:next_state(State, Var, Call), Cmds, [Var|SymbEnv]). %% @private -spec args_defined([term()], [symb_var()]) -> boolean(). args_defined(List, SymbEnv) -> lists:all(fun (A) -> arg_defined(A, SymbEnv) end, List). -spec arg_defined(term(), [symb_var()]) -> boolean(). arg_defined({var,I} = V, SymbEnv) when is_integer(I) -> lists:member(V, SymbEnv); arg_defined(Tuple, SymbEnv) when is_tuple(Tuple) -> args_defined(tuple_to_list(Tuple), SymbEnv); arg_defined(List, SymbEnv) when is_list(List) -> args_defined(List, SymbEnv); arg_defined(_, _) -> true. %% @private -spec get_initial_state(mod_name(), command_list()) -> symbolic_state(). get_initial_state(_, [{init,S}|_]) -> S; get_initial_state(Mod, Cmds) when is_list(Cmds) -> Mod:initial_state(). %% @private -spec fix_parallel(pos_integer(), non_neg_integer(), combination() | 'done', lookup(), mod_name(), symbolic_state(), [symb_var()], pos_integer()) -> [command_list()]. fix_parallel(_, 0, done, _, _, _, _, _) -> exit(error); %% not supposed to reach here fix_parallel(MaxIndex, Len, done, LookUp, Mod, State, SymbEnv, W) -> Comb = mk_first_comb(MaxIndex, Len-1, W), case Len of 1 -> io:format("f"); _ -> ok end, fix_parallel(MaxIndex, Len-1, Comb , LookUp, Mod, State, SymbEnv, W); fix_parallel(MaxIndex, Len, Comb, LookUp, Mod, State, SymbEnv, W) -> CmdLists = lookup_cmd_lists(Comb, LookUp), case can_parallelize(CmdLists, Mod, State, SymbEnv) of true -> lists:reverse(CmdLists); false -> C1 = proplists:get_value(1, Comb), C2 = proplists:get_value(2, Comb), Next = get_next(Comb, Len, MaxIndex, lists:sort(C1 ++ C2), W, 2), fix_parallel(MaxIndex, Len, Next, LookUp, Mod, State, SymbEnv, W) end. -spec can_parallelize([command_list()], mod_name(), symbolic_state(), [symb_var()]) -> boolean(). can_parallelize(CmdLists, Mod, State, SymbEnv) -> lists:all(fun(C) -> is_valid(Mod, State, C, SymbEnv) end, CmdLists) andalso lists:all(fun(C) -> is_valid(Mod, State, C, SymbEnv) end, possible_interleavings(CmdLists)). %% @private -spec possible_interleavings([command_list()]) -> [command_list()]. possible_interleavings([P1,P2]) -> insert_all(P1, P2); possible_interleavings([P1|Rest]) -> [I || L <- possible_interleavings(Rest), I <- insert_all(P1, L)]. %% @private %% Returns all possible insertions of the elements of the first list, %% preserving their order, inside the second list, i.e. all possible %% command interleavings between two parallel processes -spec insert_all([term()], [term()]) -> [[term()]]. insert_all([], List) -> [List]; insert_all([X], List) -> all_insertions(X, length(List) + 1, List); insert_all([X|[Y|Rest]], List) -> [L2 || L1 <- insert_all([Y|Rest], List), L2 <- all_insertions(X, index(Y, L1), L1)]. %% @private -spec all_insertions(term(), pos_integer(), [term()]) -> [[term()]]. all_insertions(X, Limit, List) -> all_insertions_tr(X, Limit, 0, [], List, []). -spec all_insertions_tr(term(), pos_integer(), non_neg_integer(), [term()], [term()], [[term()]]) -> [[term()]]. all_insertions_tr(X, Limit, LengthFront, Front, [], Acc) -> case LengthFront < Limit of true -> [Front ++ [X] | Acc]; false -> Acc end; all_insertions_tr(X, Limit, LengthFront, Front, Back = [BackH|BackT], Acc) -> case LengthFront < Limit of true -> all_insertions_tr(X, Limit, LengthFront+1, Front ++ [BackH], BackT, [Front ++ [X] ++ Back | Acc]); false -> Acc end. %% @private -spec index(term(), [term(),...]) -> pos_integer(). index(X, List) -> index(X, List, 1). -spec index(term(), [term(),...], pos_integer()) -> pos_integer(). index(X, [X|_], N) -> N; index(X, [_|Rest], N) -> index(X, Rest, N+1). %% @private -spec mk_dict(command_list(), pos_integer()) -> [{pos_integer(), command()}]. mk_dict([], _) -> []; mk_dict([{init,_}|T], N) -> mk_dict(T, N); mk_dict([H|T], N) -> [{N,H}|mk_dict(T, N+1)]. %% @private -spec mk_first_comb(pos_integer(), non_neg_integer(), pos_integer()) -> combination(). mk_first_comb(N, Len, W) -> mk_first_comb_tr(1, N, Len, [], W). -spec mk_first_comb_tr(pos_integer(), pos_integer(), non_neg_integer(), combination(), pos_integer()) -> combination(). mk_first_comb_tr(Start, N, _Len, Accum, 1) -> [{1,lists:seq(Start, N)}|Accum]; mk_first_comb_tr(Start, N, Len, Accum, W) -> K = Start + Len, mk_first_comb_tr(K, N, Len, [{W,lists:seq(Start, K-1)}|Accum], W-1). -spec lookup_cmds(indices(), lookup()) -> command_list(). lookup_cmds(Indices, LookUp) -> [orddict:fetch(Index, LookUp) || Index <- Indices]. -spec lookup_cmd_lists(combination(), lookup()) -> [command_list()]. lookup_cmd_lists(Combination, LookUp) -> [lookup_cmds(Indices, LookUp) || {_, Indices} <- Combination]. %% @private -spec get_next(combination(), non_neg_integer(), pos_integer(), indices(), pos_integer(), pos_integer()) -> combination() | 'done'. get_next(L, _Len, _MaxIndex, Available, _Workers, 1) -> [{1,Available}|proplists:delete(1, L)]; get_next(L, Len, MaxIndex, Available, Workers, N) -> C = case proplists:is_defined(N, L) of true -> next_comb(MaxIndex, proplists:get_value(N, L), Available); false -> lists:sublist(Available, Len) end, case C of done -> if N =:= Workers -> done; N =/= Workers -> C2 = proplists:get_value(N+1, L), NewList = [E || {M,_}=E <- L, M > N], get_next(NewList, Len, MaxIndex, lists:sort(C2 ++ Available), Workers, N+1) end; _ -> get_next([{N,C}|proplists:delete(N, L)], Len, MaxIndex, Available -- C, Workers, N-1) end. -spec next_comb(pos_integer(), indices(), indices()) -> indices() | 'done'. next_comb(MaxIndex, Indices, Available) -> Res = next_comb_tr(MaxIndex, lists:reverse(Indices), []), case is_well_defined(Res, Available) of true -> Res; false -> next_comb(MaxIndex, Res, Available) end. -spec is_well_defined(indices() | 'done', indices()) -> boolean(). is_well_defined(done, _) -> true; is_well_defined(Comb, Available) -> lists:usort(Comb) =:= Comb andalso lists:all(fun(X) -> lists:member(X, Available) end, Comb). -spec next_comb_tr(pos_integer(), indices(), indices()) -> indices() | 'done'. next_comb_tr(_MaxIndex, [], _Acc) -> done; next_comb_tr(MaxIndex, [MaxIndex | Rest], Acc) -> next_comb_tr(MaxIndex, Rest, [1 | Acc]); next_comb_tr(_MaxIndex, [X | Rest], Acc) -> lists:reverse(Rest) ++ [X+1] ++ Acc. -spec remove_slice(pos_integer(), command_list(), [command_list(),...]) -> [command_list(),...]. remove_slice(Index, Slice, List) -> remove_slice_tr(Index, Slice, List, [], 1). -spec remove_slice_tr(pos_integer(), command_list(), [command_list(),...], [command_list()], pos_integer()) -> [command_list(),...]. remove_slice_tr(Index, Slice, [H|T], Acc, Index) -> lists:reverse(Acc) ++ [H -- Slice] ++ T; remove_slice_tr(Index, Slice, [H|T], Acc, N) -> remove_slice_tr(Index, Slice, T, [H|Acc], N+1). -spec get_slices(command_list()) -> [command_list()]. get_slices(List) -> get_slices_tr(List, List, 1, []). -spec get_slices_tr(command_list(), command_list(), pos_integer(), [command_list()]) -> [command_list()]. get_slices_tr([], _, _, Acc) -> Acc; get_slices_tr([_|Tail], List, N, Acc) -> get_slices_tr(Tail, List, N+1, [lists:sublist(List, N)|Acc]). -spec spawn_link_cp(fun(() -> _)) -> pid(). spawn_link_cp(ActualFun) -> PDictStuff = [Pair || {K,_V} = Pair <- get(), is_atom(K), re:run(atom_to_list(K), ["^[$]"], [{capture,none}]) =:= match], Fun = fun() -> lists:foreach(fun({K,V}) -> put(K,V) end, PDictStuff), proper_arith:rand_reseed(), ActualFun() end, spawn_link(Fun).