fix bug in lookup_pids and update quickcheck test model

git-svn-id: http://svn.ulf.wiger.net/gproc/branches/experimental-0906/gproc@28 f3948e33-8234-0410-8a80-a07eae3b6c4d

src/Unit-Quick-Files/gproc_eqc.erl

@@ -24,7 +24,6 @@
 %%
 %%  - add non integer to value() generator
 %%  - implement mreg
-%%  - implement lookup_pid/lookup_pids
 %%
 
 %%
@@ -96,9 +95,9 @@ command(S) ->
                   %% get_value
                   , {call,?MODULE,get_value,      [elements(S#state.pids), key()]}
                   %% lookup_pid
-                  %%, {call,gproc,lookup_pid,     [key()]}
+                  , {call,?MODULE,lookup_pid,     [key()]}
                   %% lookup_pids
-                  %%, {call,gproc,lookup_pids,    [key()]}
+                  , {call,?MODULE,lookup_pids,    [key()]}
                  ])
            || S#state.pids/=[] ]
      ).
@@ -343,6 +342,26 @@ postcondition(S,{call,_,get_value,[Pid,Key]},Res) ->
         [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 ->
+    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.
@@ -456,6 +475,14 @@ update_counter(Pid, #key{class=Class,scope=Scope,name=Name},Incr) ->
 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),

src/gproc.erl

@@ -185,7 +185,7 @@ get_value(Key) ->
     get_value(Key, self()).
 
 get_value({T,_,_} = Key, Pid) when is_pid(Pid) ->
-    if T==n; T==a ->
+    if T==n orelse T==a ->
             case ets:lookup(?TAB, {Key, T}) of
                 [{_, P, Value}] when P == Pid -> Value;
                 _ -> erlang:error(badarg)
@@ -208,7 +208,7 @@ lookup_pid({_T,_,_} = Key) ->
 
 
 where({T,_,_}=Key) ->
-    if T==n; T==a ->
+    if T==n orelse T==a ->
             case ets:lookup(?TAB, {Key,T}) of
                 [] ->
                     undefined;
@@ -220,8 +220,10 @@ where({T,_,_}=Key) ->
     end.
 
 lookup_pids({T,_,_} = Key) ->
-    if T==n; T==a; T==c ->
+    if T==n orelse T==a ->
             ets:select(?TAB, [{{{Key,T}, '$1', '_'},[],['$1']}]);
+       T==c ->
+            ets:select(?TAB, [{{{Key,'_'}, '$1', '_'},[],['$1']}]);
        true ->
             erlang:error(badarg)
     end.
@@ -239,14 +241,14 @@ update_counter(_, _) ->
 
 
 send({T,C,_} = Key, Msg) when C==l; C==g ->
-    if T == n; T == a ->
+    if T == n orelse T == a ->
             case ets:lookup(?TAB, {Key, T}) of
                 [{_, Pid, _}] ->
                     Pid ! Msg;
                 [] ->
                     erlang:error(badarg)
             end;
-       T==p; T==c ->
+       T==p orelse T==c ->
             %% BUG - if the key part contains select wildcards, we may end up
             %% sending multiple messages to the same pid
             Head = {{Key,'$1'},'_'},
@@ -483,7 +485,7 @@ headpat(T, C, V1,V2,V3) ->
     Rf = fun(Pos) ->
                  {element,Pos,{element,1,{element,1,'$_'}}}
          end,
-    K2 = if T==n; T==a -> T;
+    K2 = if T==n orelse T==a -> T;
             true -> '_'
          end,
     {Kp,Vars} = case V1 of
@@ -644,7 +646,7 @@ qlc_lookup(Scope, 2, Pids) ->
                                                   [], ['$_']}]),
                           lists:flatmap(
                             fun({{_,{T,_,_}=K}}) ->
-                                    K2 = if T==n; T==a -> T;
+                                    K2 = if T==n orelse T==a -> T;
                                             true -> Pid
                                          end,
                                     case ets:lookup(?TAB, {K,K2}) of

src/gproc_eqc.erl

@@ -1,471 +0,0 @@
-%%% 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("eqc.hrl").
--include("eqc_statem.hrl").
-
--compile(export_all).
-
-%%
-%% QUESTIONS:
-%%
-%%  - does set_value for Class==a make sense?
-%%
-
-%%
-%% TODO Now:
-%%
-%%  - add non integer to value() generator
-%%  - implement mreg
-%%  - implement lookup_pid/lookup_pids
-%%
-
-%%
-%% TODO Later:
-%%
-%%  - 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,            [elements(S#state.pids), key(), value()]}
-                  %% 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,      [elements(S#state.pids), key(), value()]}
-                  %% 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,gproc,lookup_pid,     [key()]}
-                  %% lookup_pids
-                  %%, {call,gproc,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() -> int().
-
-
-%% helpers
-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)
-    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;
-%% 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() ->
-    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).
-
-%% 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.

src/gproc_lib.erl

@@ -112,7 +112,7 @@ remove_counter_1({c,C,N} = Key, Val, Pid) ->
     Res.
 
 do_set_value({T,_,_} = Key, Value, Pid) ->
-    K2 = if T==n; T==a -> T;
+    K2 = if T==n orelse T==a -> T;
             true -> Pid
          end,
     case (catch ets:lookup_element(?TAB, {Key,K2}, 2)) of