updated quickcheck test model

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

src/gproc_eqc.erl

@@ -70,38 +70,37 @@ command(S) ->
       ++ [ {call,?MODULE,n_reg,[name(),elements(S#state.pids)]}
            || S#state.pids/=[] ]
       %% name - unregister
-      ++ [ {call,?MODULE,n_unreg,[elements(S#state.n_regs)]}
-           || S#state.n_regs/=[] ]
+      ++ [ {call,?MODULE,n_unreg,[name(),elements(S#state.pids)]}
+           || S#state.pids/=[] ]
       %% counter - register
       ++ [ {call,?MODULE,c_reg,[counter(),elements(S#state.pids),int()]}
            || S#state.pids/=[] ]
       %% counter - unregister
-      ++ [ {call,?MODULE,c_unreg,[elements(S#state.c_regs)]}
-           || S#state.c_regs/=[] ]
+      ++ [ {call,?MODULE,c_unreg,[counter(),elements(S#state.pids)]}
+           || S#state.pids/=[] ]
       %% aggr counter - register
       ++ [ {call,?MODULE,a_reg,[aggr_counter(),elements(S#state.pids)]}
            || S#state.pids/=[] ]
       %% aggr counter - unregister
-      ++ [ {call,?MODULE,a_unreg,[elements(S#state.a_regs)]}
-           || S#state.a_regs/=[] ]
+      ++ [ {call,?MODULE,a_unreg,[aggr_counter(),elements(S#state.pids)]}
+           || S#state.pids/=[] ]
 
       %% counter - set_value
-      ++ [ {call,?MODULE,set_value,[elements(S#state.c_regs),int()]}
-           || S#state.c_regs/=[] ]
+      ++ [ {call,?MODULE,c_set_value,[counter(),elements(S#state.pids),int()]}
+           || S#state.pids/=[] ]
 
       %% aggr counter - get_value
-      ++ [{call,?MODULE,get_value,[elements(S#state.c_regs)]}
-          || S#state.c_regs/=[] ]
-      ++ [{call,?MODULE,get_value,[elements(S#state.a_regs)]}
-          || S#state.a_regs/=[] ]
+      ++ [ {call,?MODULE,a_get_value,[aggr_counter(),elements(S#state.pids)]}
+           || S#state.pids/=[] ]
 
       %% name - where
       ++ [{call,gproc,where,[{n,l,name()}]}]
       %% aggr counter - where
       ++ [{call,gproc,where,[{a,l,aggr_counter()}]}]
-      %% counter - lookup_pids
-      ++ [ {call,gproc,lookup_pids,[{c,l,counter()}]}
-           || S#state.c_regs/=[] ]
+
+      %% TODO: postcondition fails ... need to investigate ?
+      %% %% counter - lookup_pids
+      %% ++ [ {call,gproc,lookup_pids,[{c,l,counter()}]} ]
 
      ).
 
@@ -137,51 +136,99 @@ next_state(S,_V,{call,_,kill,[Pid]}) ->
             , a_regs=[ X || #a_reg{pid=Pid1}=X <- S#state.a_regs, Pid/=Pid1 ]
            };
 %% n_reg
-next_state(S,_V,{call,_,n_reg,[Name,Pid]}) ->
-    case is_n_register_ok(S,Name,Pid) of
+next_state(S,_V,{call,_,n_reg,[Key,Pid]}) ->
+    case is_n_register_ok(S,Key,Pid) of
         false ->
             S;
         true ->
-            S#state{n_regs=[#n_reg{key=Name,pid=Pid}|S#state.n_regs]}
+            S#state{n_regs=[#n_reg{key=Key,pid=Pid}|S#state.n_regs]}
     end;
 %% n_unreg
-next_state(S,_V,{call,_,n_unreg,[#n_reg{key=Name}]}) ->
-    S#state{n_regs=[ X || #n_reg{key=Name1}=X <- S#state.n_regs
-                              , Name/=Name1 ]};
+next_state(S,_V,{call,_,n_unreg,[Key,Pid]}) ->
+    case is_n_unregister_ok(S,Key,Pid) of
+        false ->
+            S;
+        true ->
+            FunN = fun(#n_reg{key=Key1,pid=Pid1}) -> (Key==Key1 andalso Pid==Pid1) end,
+            case lists:partition(FunN, S#state.n_regs) of
+                {[_], NOthers} ->
+                    S#state{n_regs=NOthers}
+            end
+    end;
 %% c_reg
-next_state(S,_V,{call,_,c_reg,[Counter,Pid,Value]}) ->
-    case is_c_register_ok(S,Counter,Pid) of
+next_state(S,_V,{call,_,c_reg,[Key,Pid,Value]}) ->
+    case is_c_register_ok(S,Key,Pid) of
         false ->
             S;
         true ->
-            S#state{c_regs=[#c_reg{key=Counter,pid=Pid,value=Value}|S#state.c_regs]}
+            S1 = S#state{c_regs=[#c_reg{key=Key,pid=Pid,value=Value}|S#state.c_regs]},
+            %% aggr counter update
+            FunA = fun(#a_reg{key=Key1}) -> Key==Key1 end,
+            case lists:partition(FunA, S#state.a_regs) of
+                {[], _AOthers} ->
+                    S1;
+                {[AReg], AOthers} ->
+                    S1#state{a_regs=[AReg#a_reg{value=AReg#a_reg.value+Value}|AOthers]}
+            end
     end;
 %% c_unreg
-next_state(S,_V,{call,_,c_unreg,[#c_reg{key=Counter,pid=Pid}]}) ->
-    S#state{c_regs=[ X || #c_reg{key=Counter1,pid=Pid1}=X <- S#state.c_regs
-                              , Counter/=Counter1 andalso Pid/=Pid1 ]};
+next_state(S,_V,{call,_,c_unreg,[Key,Pid]}) ->
+    case is_c_unregister_ok(S,Key,Pid) of
+        false ->
+            S;
+        true ->
+            FunC = fun(#c_reg{key=Key1,pid=Pid1}) -> (Key==Key1 andalso Pid==Pid1) end,
+            case lists:partition(FunC, S#state.c_regs) of
+                {[#c_reg{value=Value}], COthers} ->
+                    S1 = S#state{c_regs=COthers},
+                    %% aggr counter update
+                    FunA = fun(#a_reg{key=Key1}) -> Key==Key1 end,
+                    case lists:partition(FunA, S#state.a_regs) of
+                        {[], _AOthers} ->
+                            S1;
+                        {[AReg], AOthers} ->
+                            S1#state{a_regs=[AReg#a_reg{value=AReg#a_reg.value-Value}|AOthers]}
+                    end
+            end
+    end;
 %% a_reg
-next_state(S,_V,{call,_,a_reg,[AggrCounter,Pid]}) ->
-    case is_a_register_ok(S,AggrCounter,Pid) of
+next_state(S,_V,{call,_,a_reg,[Key,Pid]}) ->
+    case is_a_register_ok(S,Key,Pid) of
         false ->
             S;
         true ->
-            S#state{a_regs=[#a_reg{key=AggrCounter,pid=Pid,value=0}|S#state.a_regs]}
+            S#state{a_regs=[#a_reg{key=Key,pid=Pid,value=0}|S#state.a_regs]}
     end;
 %% a_unreg
-next_state(S,_V,{call,_,a_unreg,[#a_reg{key=AggrCounter}]}) ->
-    S#state{a_regs=[ X || #a_reg{key=AggrCounter1}=X <- S#state.a_regs
-                              , AggrCounter/=AggrCounter1 ]};
+next_state(S,_V,{call,_,a_unreg,[Key,Pid]}) ->
+    case is_a_unregister_ok(S,Key,Pid) of
+        false ->
+            S;
+        true ->
+            FunA = fun(#a_reg{key=Key1,pid=Pid1}) -> (Key==Key1 andalso Pid==Pid1) end,
+            case lists:partition(FunA, S#state.a_regs) of
+                {[_], AOthers} ->
+                    S#state{a_regs=AOthers}
+            end
+    end;
 %% set_value
-next_state(S,_V,{call,_,set_value,[#c_reg{key=Counter,pid=Pid},Value]}) ->
-    case is_c_registered_and_alive(S,Counter,Pid) of
+next_state(S,_V,{call,_,c_set_value,[Key,Pid,Value]}) ->
+    case is_c_registered_and_alive(S,Key,Pid) of
         false ->
             S;
         true ->
-            Fun = fun(#c_reg{key=Counter1,pid=Pid1}) -> Counter==Counter1 andalso Pid==Pid1 end,
-            case lists:splitwith(Fun, S#state.c_regs) of
-                {[#c_reg{key=Counter,pid=Pid,value=_OldValue}], Others} ->
-                    S#state{c_regs=[#c_reg{key=Counter,pid=Pid,value=Value}|Others]}
+            FunC = fun(#c_reg{key=Key1,pid=Pid1}) -> (Key==Key1 andalso Pid==Pid1) end,
+            case lists:partition(FunC, S#state.c_regs) of
+                {[#c_reg{value=OldValue}=CReg], COthers} ->
+                    S1 = S#state{c_regs=[CReg#c_reg{value=Value}|COthers]},
+                    %% aggr counter update
+                    FunA = fun(#a_reg{key=Key1}) -> Key==Key1 end,
+                    case lists:partition(FunA, S#state.a_regs) of
+                        {[], _AOthers} ->
+                            S1;
+                        {[AReg], AOthers} ->
+                            S1#state{a_regs=[AReg#a_reg{value=AReg#a_reg.value-OldValue+Value}|AOthers]}
+                    end
             end
     end;
 %% otherwise
@@ -205,98 +252,89 @@ postcondition(_S,{call,_,spawn,_},_Res) ->
 postcondition(_S,{call,_,kill,_},_Res) ->
     true;
 %% n_reg
-postcondition(S,{call,_,n_reg,[Name,Pid]},Res) ->
+postcondition(S,{call,_,n_reg,[Key,Pid]},Res) ->
     case Res of
         true ->
-            is_n_register_ok(S,Name,Pid);
+            is_n_register_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_n_register_ok(S,Name,Pid)
+            not is_n_register_ok(S,Key,Pid)
     end;
 %% n_unreg
-postcondition(S,{call,_,n_unreg,[#n_reg{key=Name,pid=Pid}]},Res) ->
+postcondition(S,{call,_,n_unreg,[Key,Pid]},Res) ->
     case Res of
         true ->
-            is_n_unregister_ok(S,Name,Pid);
+            is_n_unregister_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_n_unregister_ok(S,Name,Pid)
+            not is_n_unregister_ok(S,Key,Pid)
     end;
 %% c_reg
-postcondition(S,{call,_,c_reg,[Counter,Pid,_Value]},Res) ->
+postcondition(S,{call,_,c_reg,[Key,Pid,_Value]},Res) ->
     case Res of
         true ->
-            is_c_register_ok(S,Counter,Pid);
+            is_c_register_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_c_register_ok(S,Counter,Pid)
+            not is_c_register_ok(S,Key,Pid)
     end;
 %% c_unreg
-postcondition(S,{call,_,c_unreg,[#c_reg{key=Counter,pid=Pid}]},Res) ->
+postcondition(S,{call,_,c_unreg,[Key,Pid]},Res) ->
     case Res of
         true ->
-            is_c_unregister_ok(S,Counter,Pid);
+            is_c_unregister_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_c_unregister_ok(S,Counter,Pid)
+            not is_c_unregister_ok(S,Key,Pid)
     end;
 %% a_reg
-postcondition(S,{call,_,a_reg,[AggrCounter,Pid]},Res) ->
+postcondition(S,{call,_,a_reg,[Key,Pid]},Res) ->
     case Res of
         true ->
-            is_a_register_ok(S,AggrCounter,Pid);
+            is_a_register_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_a_register_ok(S,AggrCounter,Pid)
+            not is_a_register_ok(S,Key,Pid)
     end;
 %% a_unreg
-postcondition(S,{call,_,a_unreg,[#a_reg{key=AggrCounter,pid=Pid}]},Res) ->
+postcondition(S,{call,_,a_unreg,[Key,Pid]},Res) ->
     case Res of
         true ->
-            is_a_unregister_ok(S,AggrCounter,Pid);
+            is_a_unregister_ok(S,Key,Pid);
         {'EXIT',_} ->
-            not is_a_unregister_ok(S,AggrCounter,Pid)
+            not is_a_unregister_ok(S,Key,Pid)
     end;
 %% set_value
-postcondition(S,{call,_,set_value,[#c_reg{key=Counter,pid=Pid},_Value]},Res) ->
+postcondition(S,{call,_,c_set_value,[Key,Pid,_Value]},Res) ->
     case Res of
         true ->
-            is_c_registered_and_alive(S,Counter,Pid);
+            is_c_registered_and_alive(S,Key,Pid);
         {'EXIT',_} ->
-            not is_c_registered_and_alive(S,Counter,Pid)
-    end;
-%% get_value
-postcondition(S,{call,_,get_value,[#c_reg{key=Counter,pid=Pid}]},Res) ->
-    case [ Value1 || #c_reg{key=Counter1,pid=Pid1,value=Value1} <- S#state.c_regs
-                         , Counter==Counter1 andalso Pid==Pid1 ] of
-        [] ->
-            case Res of {'EXIT',_} -> true; _ -> false end;
-        [Value] ->
-            Res == Value
+            not is_c_registered_and_alive(S,Key,Pid)
     end;
 %% get_value
-postcondition(S,{call,_,get_value,[#a_reg{key=AggrCounter,pid=Pid}]},Res) ->
-    case [ Value1 || #a_reg{key=AggrCounter1,pid=Pid1,value=Value1} <- S#state.a_regs
-                         , AggrCounter==AggrCounter1 andalso Pid==Pid1 ] of
+postcondition(S,{call,_,a_get_value,[Key,Pid]},Res) ->
+    case [ Value || #a_reg{key=Key1,pid=Pid1,value=Value} <- S#state.a_regs
+                        , (Key==Key1 andalso Pid==Pid1) ] of
         [] ->
             case Res of {'EXIT',_} -> true; _ -> false end;
         [Value] ->
             Res == Value
     end;
 %% where
-postcondition(S,{call,_,where,[{n,l,Name}]},Res) ->
-    case lists:keysearch(Name,#n_reg.key,S#state.n_regs) of
+postcondition(S,{call,_,where,[{n,l,Key}]},Res) ->
+    case lists:keysearch(Key,#n_reg.key,S#state.n_regs) of
         {value, #n_reg{pid=Pid}} ->
             Res == Pid;
         false ->
             Res == undefined
     end;
-postcondition(S,{call,_,where,[{a,l,AggrCounter}]},Res) ->
-    case lists:keysearch(AggrCounter,#a_reg.key,S#state.a_regs) of
+postcondition(S,{call,_,where,[{a,l,Key}]},Res) ->
+    case lists:keysearch(Key,#a_reg.key,S#state.a_regs) of
         {value, #a_reg{pid=Pid}} ->
             Res == Pid;
         false ->
             Res == undefined
     end;
 %% lookup_pids
-postcondition(S,{call,_,lookup_pids,[{c,l,Counter}]},Res) ->
-    lists:usort(Res) ==
-        [ Pid || #c_reg{key=Counter1,pid=Pid} <- S#state.c_regs, Counter==Counter1 ];
+postcondition(S,{call,_,lookup_pids,[{c,l,Key}]},Res) ->
+    lists:sort(Res) ==
+        lists:sort([ Pid || #c_reg{key=Key1,pid=Pid} <- S#state.c_regs, Key==Key1 ]);
 %% otherwise
 postcondition(_S,{call,_,_,_},_Res) ->
     false.
@@ -310,8 +348,26 @@ prop_gproc() ->
                    {H,S,Res} = run_commands(?MODULE,Cmds),
                    kill_all_pids({H,S}),
                    ok = stop_app(),
+
+                   %% whenfail
                    ?WHENFAIL(
-                      io:format("History: ~p\nState: ~p\nRes: ~p\n",[H,S,Res]),
+                      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)).
 
@@ -348,26 +404,32 @@ kill_all_pids(_) ->
 
 
 %% helpers
-is_n_register_ok(S,Name,Pid) ->
-    not is_n_unregister_ok(S,Name,Pid).
+is_n_register_ok(S,Key,_Pid) ->
+    [] == [ Pid1 || #n_reg{key=Key1,pid=Pid1}
+                        <- S#state.n_regs, (Key==Key1) ].
 
-is_n_unregister_ok(S,Name,_Pid) ->
-    lists:keymember(Name,#n_reg.key,S#state.n_regs).
+is_n_unregister_ok(S,Key,Pid) ->
+    [] /= [ Pid1 || #n_reg{key=Key1,pid=Pid1}
+                        <- S#state.n_regs, (Key==Key1 andalso Pid==Pid1) ].
 
-is_c_register_ok(S,Counter,Pid) ->
-    not is_c_unregister_ok(S,Counter,Pid).
+is_c_register_ok(S,Key,Pid) ->
+    [] == [ Pid1 || #c_reg{key=Key1,pid=Pid1}
+                        <- S#state.c_regs, (Key==Key1 andalso Pid==Pid1) ].
 
-is_c_unregister_ok(S,Counter,_Pid) ->
-    [] /= [ Pid1 || #c_reg{key=Counter1,pid=Pid1} <- S#state.c_regs, Counter==Counter1 ].
+is_c_unregister_ok(S,Key,Pid) ->
+    [] /= [ Pid1 || #c_reg{key=Key1,pid=Pid1}
+                        <- S#state.c_regs, (Key==Key1 andalso Pid==Pid1) ].
 
-is_a_register_ok(S,AggrCounter,Pid) ->
-    not is_a_unregister_ok(S,AggrCounter,Pid).
+is_a_register_ok(S,Key,_Pid) ->
+    [] == [ Pid1 || #a_reg{key=Key1,pid=Pid1}
+                        <- S#state.a_regs, (Key==Key1) ].
 
-is_a_unregister_ok(S,AggrCounter,_Pid) ->
-    lists:keymember(AggrCounter,#a_reg.key,S#state.a_regs).
+is_a_unregister_ok(S,Key,Pid) ->
+    [] /= [ Pid1 || #a_reg{key=Key1,pid=Pid1}
+                        <- S#state.a_regs, (Key==Key1 andalso Pid==Pid1) ].
 
-is_c_registered_and_alive(S,Counter,Pid) ->
-    [Pid] == [ Pid1 || #c_reg{key=Counter1,pid=Pid1} <- S#state.c_regs, Counter==Counter1 ]
+is_c_registered_and_alive(S,Key,Pid) ->
+    is_c_unregister_ok(S,Key,Pid)
         andalso lists:member(Pid,S#state.pids)
         andalso not lists:member(Pid,S#state.killed).
 
@@ -391,64 +453,59 @@ kill(Pid) ->
     timer:sleep(10).
 
 %% n_reg
-n_reg(Name,Pid) ->
+n_reg(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:reg({n,l,Name},Pid)
+               catch gproc:reg({n,l,Key},Pid)
        end).
 
 %% n_unreg
-n_unreg(#n_reg{key=Name,pid=Pid}) ->
+n_unreg(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:unreg({n,l,Name})
+               catch gproc:unreg({n,l,Key})
        end).
 
 %% c_reg
-c_reg(Counter,Pid,Value) ->
+c_reg(Key,Pid,Value) ->
     do(Pid,
        fun() ->
-               catch gproc:reg({c,l,Counter},Value)
+               catch gproc:reg({c,l,Key},Value)
        end).
 
 %% c_unreg
-c_unreg(#c_reg{key=Counter,pid=Pid}) ->
+c_unreg(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:unreg({c,l,Counter})
+               catch gproc:unreg({c,l,Key})
        end).
 
 %% a_reg
-a_reg(AggrCounter,Pid) ->
+a_reg(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:reg({a,l,AggrCounter},Pid)
+               catch gproc:reg({a,l,Key},Pid)
        end).
 
 %% a_unreg
-a_unreg(#a_reg{key=AggrCounter,pid=Pid}) ->
+a_unreg(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:unreg({a,l,AggrCounter})
+               catch gproc:unreg({a,l,Key})
        end).
 
-%% set_value
-set_value(#c_reg{key=Counter,pid=Pid},Value) ->
+%% c_set_value
+c_set_value(Key,Pid,Value) ->
     do(Pid,
        fun() ->
-               catch gproc:set_value({c,l,Counter},Value)
+               catch gproc:set_value({c,l,Key},Value)
        end).
 
-%% get_value
-get_value(#c_reg{key=Counter,pid=Pid}) ->
-    do(Pid,
-       fun() ->
-               catch gproc:get_value({c,l,Counter})
-       end);
-get_value(#a_reg{key=AggrCounter,pid=Pid}) ->
+%% a_get_value
+a_get_value(Key,Pid) ->
     do(Pid,
        fun() ->
-               catch gproc:get_value({a,l,AggrCounter})
+               catch gproc:get_value({a,l,Key})
        end).