code_mesh/registry.erl at master · rjmh/code_mesh · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
-module(registry).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").
-compile(export_all).

-record(state,{pids=[],regs=[]}).

initial_state() ->
  #state{}.

%% spawn

spawn_args(_) ->
  [].

spawn() ->
  erlang:spawn(timer,sleep,[5000]).

spawn_next(S,Pid,[]) ->
  S#state{pids=S#state.pids++[Pid]}.

%% register

register_args(S) ->
  [name(),pid(S)].

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

name() ->
  elements(?names).

pid(S) ->
  elements(S#state.pids).

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

register_pre(S) ->
  S#state.pids /= [].

register_pre(S,[Name,Pid]) ->
  not lists:keymember(Name,1,S#state.regs) andalso
  not lists:keymember(Pid, 2,S#state.regs).

register_next(S,_,[Name,Pid]) ->
  S#state{regs=S#state.regs++[{Name,Pid}]}.

%% whereis

whereis_args(_) ->
  [name()].

whereis(Name) ->
  erlang:whereis(Name).

whereis_post(S,[Name],Res) ->
  eq(Res,proplists:get_value(Name,S#state.regs)).

prop_registry() ->
  ?FORALL(Cmds, commands(?MODULE),
          begin
            [catch unregister(Name) || Name <- ?names],
            {H, S, Res} = run_commands(?MODULE,Cmds),
            pretty_commands(?MODULE, Cmds, {H, S, Res},
                            aggregate(command_names(Cmds),
                                      Res == ok))
          end).