%%% File        : gproc_eqc_tests.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_tests).

-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()]
         , waiters=[]   %% [{key(),pid()}]
        }).


%% external API

good_number_of_tests() ->
    3000.

%% When run from eunit, we need to set the group leader so that EQC
%% reporting (the dots) are made visible - that is, if that's what we want.
verbose_run(N) ->
    erlang:group_leader(whereis(user), self()),
    run(N).

%% 3000 tests seems like a large number, but this seems to be needed
%% to reach enough variation in the tests.
all_tests() ->
    eqc:module({numtests, good_number_of_tests()}, ?MODULE).

run() ->
    run(good_number_of_tests()).

run(Num) ->
    error_logger:delete_report_handler(error_logger_tty_h),
    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()]} ]

      ++ [ {call,?MODULE,await_new, [name_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,         ?LET({Pid,Class,Scope}, {elements(S#state.pids),class(),scope()}, [Pid, Class, Scope, mreg_values(S, Class, Scope)])}
                  %%, {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/=[] ]

      ++ [
          %% await on existing value
          {call,?MODULE,await_existing, [elements(S#state.regs)]}
          || S#state.regs/=[] ]


     ).

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

%% generator scope
scope() -> l.

%% generator name
name() -> elements(names()).

names() -> [x,y,z,w].
    

%% generator key
key() -> key(class(), scope(), name()).

key(Class, Scope, Name) ->
    #key{class=Class, scope=Scope, name=Name}.

name_key() ->
    key(n, scope(), 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().


mreg_values(_S, Class, Scope) ->
    ?LET(Names, subset(names()),
         [?LET(K, key(Class, Scope, N), {K, reg_value(K)}) || N <- Names]).


%% Snipped from the TrapExit QuickCheck tutorials
%% http://trapexit.org/SubSetGenerator
subset(Generators) ->
   ?LET(Keep,[ {bool(),G} || G<-Generators],
	[ G || {true,G}<-Keep]).

%% 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) ->
    Value == undefined;
is_register_ok(S,Pid,Key,_Value) ->
    [] == [ Pid1 || #reg{pid=Pid1,key=Key1}
                        <- S#state.regs, is_register_eq(Pid,Key,Pid1,Key1) ].

is_mreg_ok(S, Pid, List) ->
    lists:all(fun({Key, Value}) ->
                      is_register_ok(S, Pid, Key, Value)
              end, List).

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 ->
            update_state_reg(S, Pid, Key, Value)
    end;
next_state(S,_V,{call,_,mreg,[Pid, _Class, _Scope, List]}) ->
    case is_mreg_ok(S, Pid, List) of
        false ->
            S;
        true ->
            lists:foldl(
              fun({Key, Value}, Acc) ->
                      update_state_reg(Acc, Pid, Key, Value)
              end, S, List)
    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, is_integer(Incr) ->
    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;
next_state(S,V,{call,_,await_new,[Key]}) ->
    S#state{waiters = [{Key,V}|S#state.waiters]};
%% otherwise
next_state(S,_V,{call,_,_,_}) ->
    S.


update_state_reg(S, Pid, Key, Value) ->
    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],
                    waiters = [W || {K,_} = W <- S#state.waiters,
                                    K =/= Key]}
    end.



%% Precondition, checked before command is added to the command
%% sequence
precondition(S, {call,_,reg, [Pid, _Key, _Value]}) ->
    lists:member(Pid, S#state.pids);
precondition(S, {call,_,unreg, [Pid, _Key]}) ->
    lists:member(Pid, S#state.pids);
precondition(S, {call,_,await_new,[#key{class=C}=Key]}) ->
    C == n andalso
        not lists:keymember(Key,#reg.key,S#state.regs);
precondition(S, {call,_,mreg,[Pid, Class, _Scope, List]}) ->
    %% TODO: lift this restriction to generate all classes mreg can handle
    Class == n andalso
	lists:member(Pid, S#state.pids) andalso
        lists:all(fun({#key{class=C},_}) -> C == n end, List);
precondition(S, {call,_,await_existing,[#reg{key=#key{class=C}=Key}]}) ->
    C == n andalso
	lists:keymember(Key, #reg.key, S#state.regs);
precondition(S,{call,_,get_value,[Pid,_]}) ->
	lists:member(Pid,S#state.pids);
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) andalso
                check_waiters(Pid, Key, Value, S#state.waiters);
        {'EXIT', {badarg, _}} ->
            is_unregister_ok(S,Pid,Key)
                orelse not is_register_ok(S,Pid,Key,Value)
    end;
postcondition(S,{call,_,mreg,[Pid,_Class,_Scope,List]},Res) ->
    case Res of
        true ->
            is_mreg_ok(S,Pid,List)
                andalso lists:all(fun({K,V}) ->
                                          check_waiters(Pid,K,V, S#state.waiters)
                                  end, List);
        {'EXIT', {badarg,_}} ->
            not is_mreg_ok(S,Pid,List)
    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, is_integer(Incr) ->
    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] when is_integer(Value) ->
            Res == Value+Incr;
		[_] ->
            case Res of {'EXIT', {badarg, _}} -> true; _ -> false end
    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,_,await_new,[#key{}]}, Pid) ->
    is_pid(Pid);
postcondition(S,{call,_,await_existing,[#reg{key=Key}]}, {P1,V1}) ->
    case lists:keyfind(Key, #reg.key, S#state.regs) of
        #reg{pid=P1, value = V1} -> true;
        _ -> false
    end;
%% postcondition(_S,{call,_,lookup_pids,[_Key]},Res) ->
%%     case Res of {'EXIT', {badarg, _}} -> true; _ -> false end;
%% otherwise
postcondition(_S,{call,_,_,_},_Res) ->
    false.


%%% Spec fixes
%%% 
%%% - added precondition for set_value must be integer (could be changed 
%%%   to neg. test)
%%% - updated postcondition for update_counter to check for non-integers
%%%
%%% It still crashes on lists:sum in next_state... Maybe we should change
%%% the generators instead!

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() ->
    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).

mreg(Pid, Class, Scope, List) ->
    do(Pid, fun() -> catch gproc:mreg(Class,Scope,[{Name,Value} || {#key{name = Name}, Value} <- List]) 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.


await_existing(#reg{key = #key{class=Class,scope=Scope,name=Name}}) ->
    %% short timeout, this call is expected to work
    gproc:await({Class,Scope,Name}, 10000).

await_new(#key{class=Class,scope=Scope,name=Name}) ->
    spawn(
      fun() ->
              Res = (catch gproc:await({Class,Scope,Name})),
              receive
                  {From, send_result} ->
                      From ! {result, Res},
                      timer:sleep(1000)
              end
      end).

check_waiters(Pid, Key, Value, Waiters) ->
    case [W || {K, W} <- Waiters,
               K == Key] of
        [] ->
            true;
        WPids ->
            lists:all(fun(WPid) ->
                              check_waiter(WPid, Pid, Key, Value)
                      end, WPids)
    end.

check_waiter(WPid, Pid, _Key, Value) ->   
    MRef = erlang:monitor(process, WPid),
    WPid ! {self(), send_result},
    receive
        {result, Res} ->
            {Pid,Value} == Res;
        {'DOWN', MRef, _, _, R} ->
            erlang:error(R)
    after 1000 ->
            erlang:error(timeout)
    end.