gproc/src/Unit-Quick-Files/gproc_eqc.erl

%%% File        : gproc_eqc.erl
%%% Author      : <norton@alum.mit.edu>
%%%             : <Ulf.Wiger@erlang-consulting.com>
%%%             : <John.Hughes@quviq.com>
%%% Description : QuickCheck test model for gproc
%%% Created     : 11 Dec 2008 by  <John Hughes@JTABLET2007>

-module(gproc_eqc).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

-compile(export_all).

%%
%% QUESTIONS:
%%
%%  - does set_value for Class==a make sense?
%%  - shouldn't mreg return {true, keys()} rather than the {true,
%%    objects()} upon success?

%%
%% TODO:
%%
%%  - implement mreg
%%  - implement send
%%  - implement info
%%  - implement select
%%  - implement first/next/prev/last
%%  - implement table
%%

%% records
-record(key,
        {class          %% class()
         , scope        %% scope()
         , name         %% name()
        }).

-record(reg,
        {pid            %% pid()
         , key          %% key()
         , value        %% int()
        }).

-record(state,
        {pids=[]        %% [pid()]
         , killed=[]    %% [pid()]
         , regs=[]      %% [reg()]
        }).


%% external API
start_test() ->
    eqc:module({numtests, 500}, ?MODULE).

run() ->
    run(500).

run(Num) ->
    eqc:quickcheck(eqc:numtests(Num, prop_gproc())).


%% Command generator, S is the state
command(S) ->
    oneof(
      %% spawn
      [ {call,?MODULE,spawn, []} ]

      %% where
      ++ [ {call,?MODULE,where, [key()]} ]

      %% kill
      ++ [ oneof([
                  %% kill
                  {call,?MODULE,kill,             [elements(S#state.pids)]}
                  %% register
                  , {call,?MODULE,reg,            ?LET(Key, key(),[elements(S#state.pids), Key, reg_value(Key)])}
                  %% unregister
                  , {call,?MODULE,unreg,          [elements(S#state.pids), key()]}
                  %% many register
                  %%, {call,?MODULE,mreg,           [elements(S#state.pids), class(), scope()
                  %%                                 , list({name(), value()})]}

                  %% set_value
                  , {call,?MODULE,set_value,      ?LET(Key, key(),[elements(S#state.pids), Key, reg_value(Key)])}
                  %% update_counter
                  , {call,?MODULE,update_counter, [elements(S#state.pids), key(), value()]}

                  %% get_value
                  , {call,?MODULE,get_value,      [elements(S#state.pids), key()]}
                  %% lookup_pid
                  , {call,?MODULE,lookup_pid,     [key()]}
                  %% lookup_pids
                  , {call,?MODULE,lookup_pids,    [key()]}
                 ])
           || S#state.pids/=[] ]
     ).

%% generator class
class() -> elements([n,p,c,a]).

%% generator scope
scope() -> l.

%% generator name
name() -> elements([x,y,z,w]).

%% generator key
key() -> #key{class=class(), scope=scope(), name=name()}.


%% generator value
value() -> frequency([{8, int()}, {1, undefined}, {1, make_ref()}]).

%% value for reg and set_value
%% 'a' and 'c' should only have integers as values (reg: value is ignored for 'a') 
reg_value(#key{class=C}) when C == a; C == c -> int();
reg_value(_) -> value().

%% helpers
is_register_ok(_S,_Pid,#key{class=c},Value) when not is_integer(Value) ->
    false;
is_register_ok(_S,_Pid,#key{class=a},Value) when not is_integer(Value) ->
    false;
is_register_ok(S,Pid,Key,_Value) ->
    [] == [ Pid1 || #reg{pid=Pid1,key=Key1}
                        <- S#state.regs, is_register_eq(Pid,Key,Pid1,Key1) ].

is_register_eq(_PidA,#key{class=Class}=KeyA,_PidB,KeyB)
  when Class == n; Class ==a ->
    KeyA==KeyB;
is_register_eq(PidA,KeyA,PidB,KeyB) ->
    PidA==PidB andalso KeyA==KeyB.

is_unregister_ok(S,Pid,Key) ->
    [] /= [ Pid1 || #reg{pid=Pid1,key=Key1}
                        <- S#state.regs, is_unregister_eq(Pid,Key,Pid1,Key1) ].

is_unregister_eq(PidA,KeyA,PidB,KeyB) ->
    KeyA==KeyB andalso PidA==PidB.

is_registered_and_alive(S,Pid,Key) ->
    is_unregister_ok(S,Pid,Key)
        andalso lists:member(Pid,S#state.pids).


%% Initialize the state
initial_state() ->
    #state{}.


%% Next state transformation, S is the current state
%% spawn
next_state(S,V,{call,_,spawn,_}) ->
    S#state{pids=[V|S#state.pids]};
%% kill
next_state(S,_V,{call,_,kill,[Pid]}) ->
    S#state{pids=S#state.pids -- [Pid]
            , killed=[Pid|S#state.killed]
            , regs=[ X || #reg{pid=Pid1}=X <- S#state.regs, Pid/=Pid1 ]
           };
%% reg
next_state(S,_V,{call,_,reg,[Pid,Key,Value]}) ->
    case is_register_ok(S,Pid,Key,Value) of
        false ->
            S;
        true ->
            case Key of
                #key{class=a,name=Name} ->
                    %% initialize aggr counter
                    FunC = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == c andalso Name==Name1) end,
                    {Regs, _Others} = lists:partition(FunC, S#state.regs),
                    InitialValue = lists:sum([ V || #reg{value=V} <- Regs ]),
                    S#state{regs=[#reg{pid=Pid,key=Key,value=InitialValue}|S#state.regs]};
                #key{class=c,name=Name} ->
                    S1 = S#state{regs=[#reg{pid=Pid,key=Key,value=Value}|S#state.regs]},
                    %% update aggr counter
                    FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
                    case lists:partition(FunA, S1#state.regs) of
                        {[Reg], Others} ->
                            S1#state{regs=[Reg#reg{value=Reg#reg.value+Value}|Others]};
                        {[], _Others} ->
                            S1
                    end;
                _ ->
                    S#state{regs=[#reg{pid=Pid,key=Key,value=Value}|S#state.regs]}
            end
    end;
%% unreg
next_state(S,_V,{call,_,unreg,[Pid,Key]}) ->
    case is_unregister_ok(S,Pid,Key) of
        false ->
            S;
        true ->
            FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
            case lists:partition(FunC, S#state.regs) of
                {[#reg{value=Value}], Others} ->
                    S1 = S#state{regs=Others},
                    case Key of
                        #key{class=c,name=Name} ->
                            %% update aggr counter
                            FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
                            case lists:partition(FunA, S1#state.regs) of
                                {[], _Others1} ->
                                    S1;
                                {[Reg], Others1} ->
                                    S1#state{regs=[Reg#reg{value=Reg#reg.value-Value}|Others1]}
                            end;
                        _ ->
                            S1
                    end
            end
    end;
%% set_value
next_state(S,_V,{call,_,set_value,[Pid,Key,Value]}) ->
    case is_registered_and_alive(S,Pid,Key) of
        false ->
            S;
        true ->
            FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
            case lists:partition(FunC, S#state.regs) of
                {[#reg{value=OldValue}=OldReg], Others} ->
                    S1 = S#state{regs=[OldReg#reg{value=Value}|Others]},
                    case Key of
                        #key{class=c,name=Name} ->
                            %% aggr counter update
                            FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
                            case lists:partition(FunA, S1#state.regs) of
                                {[], _Others1} ->
                                    S1;
                                {[Reg], Others1} ->
                                    S1#state{regs=[Reg#reg{value=Reg#reg.value-OldValue+Value}|Others1]}
                            end;
                        _ ->
                            S1
                    end
            end
    end;
%% update_counter
next_state(S,_V,{call,_,update_counter,[Pid,#key{class=Class}=Key,Incr]})
  when Class == c ->
    case is_registered_and_alive(S,Pid,Key) of
        false ->
            S;
        true ->
            FunC = fun(#reg{pid=Pid1,key=Key1}) -> (Pid==Pid1 andalso Key==Key1) end,
            case lists:partition(FunC, S#state.regs) of
                {[#reg{value=OldValue}=OldReg], Others} ->
                    S1 = S#state{regs=[OldReg#reg{value=OldValue+Incr}|Others]},
                    case Key of
                        #key{class=c,name=Name} ->
                            %% aggr counter update
                            FunA = fun(#reg{key=#key{class=Class1,name=Name1}}) -> (Class1 == a andalso Name==Name1) end,
                            case lists:partition(FunA, S1#state.regs) of
                                {[], _Others1} ->
                                    S1;
                                {[Reg], Others1} ->
                                    S1#state{regs=[Reg#reg{value=Reg#reg.value+Incr}|Others1]}
                            end;
                        _ ->
                            S1
                    end
            end
    end;
%% otherwise
next_state(S,_V,{call,_,_,_}) ->
    S.


%% Precondition, checked before command is added to the command
%% sequence
precondition(_S,{call,_,_,_}) ->
    true.


%% Postcondition, checked after command has been evaluated.  S is the
%% state before next_state(S,_,<command>)

%% spawn
postcondition(_S,{call,_,spawn,_},_Res) ->
    true;
%% kill
postcondition(_S,{call,_,kill,_},_Res) ->
    true;
%% where
postcondition(S,{call,_,where,[#key{class=Class}=Key]},Res) ->
    if Class == n orelse Class == a ->
            case lists:keysearch(Key,#reg.key,S#state.regs) of
                {value, #reg{pid=Pid}} ->
                    Res == Pid;
                false ->
                    Res == undefined
            end;
       true ->
            case Res of
                {'EXIT', {badarg, _}} ->
                    true;
                _ ->
                    false
            end
    end;
%% reg
postcondition(S,{call,_,reg,[Pid,Key,Value]},Res) ->
    case Res of
        true ->
            is_register_ok(S,Pid,Key,Value);
        {'EXIT', {badarg, _}} ->
            is_unregister_ok(S,Pid,Key)
                orelse not is_register_ok(S,Pid,Key,Value)
    end;
%% unreg
postcondition(S,{call,_,unreg,[Pid,Key]},Res) ->
    case Res of
        true ->
            is_unregister_ok(S,Pid,Key);
        {'EXIT', {badarg, _}} ->
            not is_unregister_ok(S,Pid,Key)
    end;
%% set_value
postcondition(S,{call,_,set_value,[Pid,Key,_Value]},Res) ->
    case Res of
        true ->
            is_registered_and_alive(S,Pid,Key);
        {'EXIT', {badarg, _}} ->
            not is_registered_and_alive(S,Pid,Key)
                orelse (Key#key.class == c
                        andalso is_registered_and_alive(S, Pid, Key))
    end;
%% update_counter
postcondition(S,{call,_,update_counter,[Pid,#key{class=Class}=Key,Incr]},Res)
  when Class == c ->
    case [ Value1 || #reg{pid=Pid1,key=Key1,value=Value1} <- S#state.regs
                         , (Pid==Pid1 andalso Key==Key1) ] of
        [] ->
            case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
        [Value] ->
            Res == Value+Incr
    end;
postcondition(_S,{call,_,update_counter,[_Pid,_Key,_Incr]},Res) ->
    case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
%% get_value
postcondition(S,{call,_,get_value,[Pid,Key]},Res) ->
    case [ Value1 || #reg{pid=Pid1,key=Key1,value=Value1} <- S#state.regs
                         , (Pid==Pid1 andalso Key==Key1) ] of
        [] ->
            case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
        [Value] ->
            Res == Value
    end;
%% lookup_pid
postcondition(S,{call,_,lookup_pid,[#key{class=Class}=Key]},Res)
  when Class == n; Class == a ->
    case [ Pid1 || #reg{pid=Pid1,key=Key1} <- S#state.regs
                       , Key==Key1 ] of
        [] ->
            case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
        [Pid] ->
            Res == Pid
    end;
postcondition(_S,{call,_,lookup_pid,[_Key]},Res) ->
    case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
%% lookup_pids
postcondition(S,{call,_,lookup_pids,[#key{class=Class}=Key]},Res)
  when Class == n; Class == a; Class == c; Class == p ->
    Pids = [ Pid1 || #reg{pid=Pid1,key=Key1} <- S#state.regs
                         , Key==Key1 ],
    lists:sort(Res) == lists:sort(Pids);
%% postcondition(_S,{call,_,lookup_pids,[_Key]},Res) ->
%%     case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
%% otherwise
postcondition(_S,{call,_,_,_},_Res) ->
    false.

%% property
prop_gproc() ->
    ?FORALL(Cmds,commands(?MODULE),
            ?TRAPEXIT(
               begin
                   ok = stop_app(),
                   ok = start_app(),
                   {H,S,Res} = run_commands(?MODULE,Cmds),
                   kill_all_pids({H,S}),

                   %% whenfail
                   ?WHENFAIL(
                      begin
                          io:format("~nHISTORY:"),
                          if
                              length(H) < 1 ->
                                  io:format(" none~n");
                              true ->
                                  CmdsH = eqc_statem:zip(Cmds,H),
                                  [ begin
                                        {Cmd,{State,Reply}} = lists:nth(N,CmdsH),
                                        io:format("~n #~p:~n\tCmd: ~p~n\tReply: ~p~n\tState: ~p~n",
                                                  [N,Cmd,Reply,State])
                                    end
                                    || N <- lists:seq(1,length(CmdsH)) ]
                          end,
                          io:format("~nRESULT:~n\t~p~n",[Res]),
                          io:format("~nSTATE:~n\t~p~n",[S])
                      end,
                      Res == ok)
               end)).

%% helpers
start_app() ->
    application:start(sasl),
    case application:start(gproc) of
        {error, {already_started,_}} ->
            stop_app(),
            ok = application:start(gproc);
        ok ->
            ok
    end.

stop_app() ->
    case application:stop(gproc) of
        {error, {not_started,_}} ->
            ok;
        ok ->
            ok
    end.

%% If using the scheduler... This code needs to run in a separate
%% module, so it can be compiled without instrumentation.
kill_all_pids(Pid) when is_pid(Pid) ->
    case is_process_alive(Pid) of
        true ->
            exit(Pid,kill);
        false ->
            ok
    end;
kill_all_pids(Tup) when is_tuple(Tup) ->
    kill_all_pids(tuple_to_list(Tup));
kill_all_pids([H|T]) ->
    kill_all_pids(H),
    kill_all_pids(T);
kill_all_pids(_) ->
    ok.


%% spawn
spawn() ->
    spawn(fun() -> loop() end).

loop() ->
    receive
        {From, Ref, F} ->
            From ! {Ref, catch F()},
            loop();
        stop -> ok
    end.

%% kill
kill(Pid) ->
    exit(Pid,foo),
    timer:sleep(10).

%% where
where(#key{class=Class,scope=Scope,name=Name}) ->
    catch gproc:where({Class,Scope,Name}).

%% reg
reg(Pid,#key{class=Class,scope=Scope,name=Name},Value) ->
    do(Pid, fun() -> catch gproc:reg({Class,Scope,Name},Value) end).

%% unreg
unreg(Pid,#key{class=Class,scope=Scope,name=Name}) ->
    do(Pid, fun() -> catch gproc:unreg({Class,Scope,Name}) end).

%% set_value
set_value(Pid,#key{class=Class,scope=Scope,name=Name},Value) ->
    do(Pid, fun() -> catch gproc:set_value({Class,Scope,Name},Value) end).

%% update_counter
update_counter(Pid, #key{class=Class,scope=Scope,name=Name},Incr) ->
    do(Pid, fun() -> catch gproc:update_counter({Class,Scope,Name},Incr) end).

%% get_value
get_value(Pid,#key{class=Class,scope=Scope,name=Name}) ->
    do(Pid, fun() -> catch gproc:get_value({Class,Scope,Name}) end).

%% lookup_pid
lookup_pid(#key{class=Class,scope=Scope,name=Name}) ->
    catch gproc:lookup_pid({Class,Scope,Name}).

%% lookup_pids
lookup_pids(#key{class=Class,scope=Scope,name=Name}) ->
    catch gproc:lookup_pids({Class,Scope,Name}).

%% do
do(Pid, F) ->
    Ref = erlang:monitor(process, Pid),
    Pid ! {self(), Ref, F},
    receive
        {'DOWN', Ref, process, Pid, Reason} ->
            {'EXIT', {'DOWN', Reason}};
        {Ref, Result} ->
            erlang:demonitor(Ref),
            Result
    after 3000 ->
            {'EXIT', timeout}
    end.