eqc suite works for await()

.gitignore

@@ -0,0 +1,2 @@
+*.beam
+current_counterexample.eqc

src/Unit-Quick-Files/gproc_eqc.erl

@@ -1,553 +1,586 @@
-%%% 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()]
-         , waiters=[]   %% [{key(),pid()}]
-        }).
-
-
-%% 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()]} ]
-
-      ++ [ {call,?MODULE,await_new, [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,?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([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()}]).
-
-
-%% 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_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,_,await_new,[Key]}) ->
-    not lists:keymember(Key,#reg.key,S#state.regs);
-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;
-%% 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,_,await_new,[#key{}=Key]}, Pid) ->
-    is_pid(Pid);
-%% 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.
-
-
-await_existing(#key{class=Class,scope=Scope,name=Name}) ->
-    %% short timeout, this call is expected to work
-    gproc:await({Class,Scope,Name}, 1000).
-
-await_new(#key{class=Class,scope=Scope,name=Name} = Key) ->
-    spawn_link(
-      fun() ->
-              Res = (catch gproc:await({Class,Scope,Name}, infinity)),
-              receive
-                  {From, send_result} ->
-                      From ! {result, Key, Res}
-              end
-      end).
-
-check_waiters(Pid, Key, Value, Waiters) ->
-    case [W || {Key, W} <- Waiters] of
-        [] ->
-            true;
-        WPids ->
-            lists:all(fun(WPid) ->
-                              check_waiter(WPid, Key, Value)
-                      end, WPids)
-    end.
-
-check_waiter(Pid, Key, Value) ->   
-    MRef = erlang:monitor(process, Pid),
-    Pid ! {self(), send_result},
-    receive
-        {result, Res} ->
-            Res == {Key, {Pid, Value}};
-        {'DOWN', MRef, _, _, R} ->
-            erlang:error(R)
-    after 1000 ->
-            erlang:error(timeout)
-    end.
+%%% 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()]
+         , waiters=[]   %% [{key(),pid()}]
+        }).
+
+
+%% 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()]} ]
+
+      ++ [ {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,           [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([x,y,z,w]).
+
+%% generator key
+key() -> #key{class=class(), scope=scope(), name=name()}.
+
+name_key() -> #key{class=n, 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) ->
+    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_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],
+                            waiters = [W || {K,_} = W <- S#state.waiters,
+                                            K =/= Key]}
+            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, 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.
+
+
+%% Precondition, checked before command is added to the command
+%% sequence
+precondition(S, {call,_,await_new,[#key{class=C}=Key]}) ->
+    C == n andalso
+        not lists:keymember(Key,#reg.key,S#state.regs);
+precondition(S, {call,_,await_existing,[#reg{key=#key{class=C}}]}) ->
+    C == n;
+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;
+%% 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{}=Key]}, Pid) ->
+    is_pid(Pid);
+postcondition(S,{call,_,await_existing,[#reg{key=Key,value=V}]}, {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() ->
+    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.
+
+
+await_existing(#reg{key = #key{class=Class,scope=Scope,name=Name}}) ->
+    %% short timeout, this call is expected to work
+    gproc:await({Class,Scope,Name}, 1000).
+
+await_new(#key{class=Class,scope=Scope,name=Name} = Key) ->
+    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.

src/gproc.erl

@@ -44,7 +44,7 @@
          set_value/2,
          get_value/1,
          where/1,
-         await/2,
+         await/1, await/2,
          nb_wait/1,
          cancel_wait/2,
          lookup_pid/1,
@@ -278,6 +278,9 @@ default(_) -> undefined.
 %% registered (the difference: await/2 also returns the value).
 %% @end
 %%
+await(Key) ->
+    await(Key, infinity).
+
 await({n,l,_} = Key, Timeout) ->
     case ets:lookup(?TAB, {Key, n}) of
         [{_, Pid, Value}] ->