gistfile1.hrl

-module(reg_eqc).

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

-compile(export_all).

% Model of states

-define(names,[a,b,c,d]).

-record(state,{pids,	% list of spawned pids
	       regs}).	% list of registered names and pids

initial_state() ->
    #state{pids=[], regs=[]}.

% State transitions

next_state(S,V,{call,?MODULE,spawn,[]}) ->
    S#state{pids=[V | S#state.pids]};
next_state(S,V,{call,?MODULE,register,[Name,Pid]}) ->
    case register_ok(S, Name, Pid) of
        true -> S#state{regs=[{Name,Pid} | S#state.regs]};
        false -> S
    end;
next_state(S,V,{call,?MODULE,unregister,[Name]}) ->
    S#state{regs = lists:keydelete(Name,1,S#state.regs)};
next_state(S,V,{call,erlang,whereis,[Name]}) ->
    S.

% Command generator

command(S) ->
    oneof(
      [{call,?MODULE,register, [name(),elements(S#state.pids)]} 
       || S#state.pids/=[]] ++
	  [{call,?MODULE,unregister,[name()]},
	   {call,?MODULE,spawn,[]},
	   {call,erlang,whereis,[name()]}]
     ).

name() -> 
    elements(?names).

% Preconditions

precondition(S=#state{regs=Regs},{call,?MODULE,unregister,[Name]}) ->
    lists:keymember(Name, 1, Regs);
precondition(S=#state{regs=Regs, pids=Pids},{call,?MODULE,register,[Name,Pid]}) ->
    not lists:keymember(Name, 1, Regs) andalso not lists:member(Pid, Pids);
precondition(S,_) -> true.


% Postconditions

postcondition(S,{call,erlang,whereis,[Name]},V) ->
    case lists:keysearch(Name, 1, S#state.regs) of
        {value, {Name, Pid}} -> V==Pid;
        false -> V==undefined
    end;

postcondition(S, {call,?MODULE,unregister,[Name]},V) -> 
    case V of
        {'EXIT', _} ->
            not lists:keymember(Name, 1, S#state.regs);
        _ -> lists:keymember(Name, 1, S#state.regs)
    end;
postcondition(S, {call,_,_,_},V) -> true.


register(Name, Pid) ->            
    catch erlang:register(Name, Pid).

unregister(Name) ->
    catch erlang:unregister(Name).

is_exit({'EXIT',_}) -> true;
is_exit(_) -> false.

register_ok(S, Name, Pid) ->    
    lists:member({Name, Pid}, S#state.regs).
            

% Correctness property

prop_registration() ->
    ?FORALL(Cmds,commands(?MODULE),
	    begin
		{H,S,Res} = run_commands(?MODULE,Cmds),
                [catch ?MODULE:unregister(N) || N<-?names],
                ?WHENFAIL(io:format("~p~n~p~n~p~n", [H,S,Res]),
                          Res==ok)
	    end).

spawn() -> 
    spawn(fun() -> loop() end).
loop() -> 
    receive _ -> loop() end.