Statem test #3
3 changed files with 56 additions and 6 deletions
2
Makefile
2
Makefile
|
@ -18,7 +18,7 @@ eunit: compile clean-test-btrees
|
||||||
@$(REBAR) eunit skip_deps=true
|
@$(REBAR) eunit skip_deps=true
|
||||||
|
|
||||||
clean-test-btrees:
|
clean-test-btrees:
|
||||||
rm -fr .eunit/Btree_*
|
rm -fr .eunit/Btree_* .eunit/simple
|
||||||
|
|
||||||
plt: compile
|
plt: compile
|
||||||
$(DIALYZER) --build_plt --output_plt .fractal_btree.plt \
|
$(DIALYZER) --build_plt --output_plt .fractal_btree.plt \
|
||||||
|
|
|
@ -6,7 +6,9 @@
|
||||||
%% API
|
%% API
|
||||||
-export([start_link/0]).
|
-export([start_link/0]).
|
||||||
|
|
||||||
-export([open/1,
|
-export([
|
||||||
|
lookup_exist/2,
|
||||||
|
open/1,
|
||||||
put/3,
|
put/3,
|
||||||
stop/0]).
|
stop/0]).
|
||||||
|
|
||||||
|
@ -27,6 +29,9 @@ start_link() ->
|
||||||
call(X) ->
|
call(X) ->
|
||||||
gen_server:call(?SERVER, X, infinity).
|
gen_server:call(?SERVER, X, infinity).
|
||||||
|
|
||||||
|
lookup_exist(N, K) ->
|
||||||
|
call({lookup_exist, N, K}).
|
||||||
|
|
||||||
open(N) ->
|
open(N) ->
|
||||||
call({open, N}).
|
call({open, N}).
|
||||||
|
|
||||||
|
@ -56,7 +61,12 @@ handle_call({put, N, K, V}, _, #state { btrees = D} = State) ->
|
||||||
Other ->
|
Other ->
|
||||||
{reply, {error, Other}, State}
|
{reply, {error, Other}, State}
|
||||||
end;
|
end;
|
||||||
|
handle_call({lookup_exist, N, K}, _, #state { btrees = D} = State) ->
|
||||||
|
Tree = dict:fetch(N, D),
|
||||||
|
Reply = fractal_btree:lookup(Tree, K),
|
||||||
|
{reply, Reply, State};
|
||||||
handle_call(stop, _, State) ->
|
handle_call(stop, _, State) ->
|
||||||
|
cleanup_trees(State),
|
||||||
{stop, normal, ok, State};
|
{stop, normal, ok, State};
|
||||||
handle_call(_Request, _From, State) ->
|
handle_call(_Request, _From, State) ->
|
||||||
Reply = ok,
|
Reply = ok,
|
||||||
|
@ -68,8 +78,7 @@ handle_cast(_Msg, State) ->
|
||||||
handle_info(_Info, State) ->
|
handle_info(_Info, State) ->
|
||||||
{noreply, State}.
|
{noreply, State}.
|
||||||
|
|
||||||
terminate(_Reason, State) ->
|
terminate(_Reason, _State) ->
|
||||||
cleanup_trees(State),
|
|
||||||
ok.
|
ok.
|
||||||
|
|
||||||
code_change(_OldVsn, State, _Extra) ->
|
code_change(_OldVsn, State, _Extra) ->
|
||||||
|
|
|
@ -23,9 +23,10 @@ full_test_() ->
|
||||||
fun () -> ok end,
|
fun () -> ok end,
|
||||||
fun (_) -> ok end,
|
fun (_) -> ok end,
|
||||||
[{timeout, 120, ?_test(test_proper())},
|
[{timeout, 120, ?_test(test_proper())},
|
||||||
|
?_test(test_tree_simple_1()),
|
||||||
?_test(test_tree())]}.
|
?_test(test_tree())]}.
|
||||||
|
|
||||||
qc_opts() -> [{numtests, 400}].
|
qc_opts() -> [{numtests, 800}].
|
||||||
|
|
||||||
test_proper() ->
|
test_proper() ->
|
||||||
[?assertEqual([], proper:module(?MODULE, qc_opts()))].
|
[?assertEqual([], proper:module(?MODULE, qc_opts()))].
|
||||||
|
@ -46,17 +47,39 @@ cmd_put_args(#state { open = Open }) ->
|
||||||
{oneof(dict:fetch_keys(Open)), binary(), binary()},
|
{oneof(dict:fetch_keys(Open)), binary(), binary()},
|
||||||
[Name, Key, Value]).
|
[Name, Key, Value]).
|
||||||
|
|
||||||
|
non_empty_btree(Open) ->
|
||||||
|
?SUCHTHAT(Name, union(dict:fetch_keys(Open)),
|
||||||
|
dict:size(dict:fetch(Name, Open)) > 0).
|
||||||
|
|
||||||
|
cmd_lookup_args(#state { open = Open}) ->
|
||||||
|
?LET(Name, non_empty_btree(Open),
|
||||||
|
?LET(Key, oneof(dict:fetch_keys(dict:fetch(Name, Open))),
|
||||||
|
[Name, Key])).
|
||||||
|
|
||||||
|
count_dicts(Open) ->
|
||||||
|
Dicts = [ V || {_, V} <- dict:to_list(Open)],
|
||||||
|
lists:sum([dict:size(D) || D <- Dicts]).
|
||||||
|
|
||||||
command(#state { open = Open} = S) ->
|
command(#state { open = Open} = S) ->
|
||||||
frequency(
|
frequency(
|
||||||
[ {100, {call, ?SERVER, open, [g_btree_name()]}} ] ++
|
[ {100, {call, ?SERVER, open, [g_btree_name()]}} ] ++
|
||||||
[ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|
[ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|
||||||
|| dict:size(Open) > 0]).
|
|| dict:size(Open) > 0] ++
|
||||||
|
[ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
|
||||||
|
|| dict:size(Open) > 0, count_dicts(Open) > 0]).
|
||||||
|
|
||||||
|
precondition(#state { open = _Open }, {call, ?SERVER, lookup_exist,
|
||||||
|
[_Name, _K]}) ->
|
||||||
|
%% No need to quantify since we limit this to validity in the
|
||||||
|
%% command/1 generator
|
||||||
|
true;
|
||||||
precondition(#state { open = Open }, {call, ?SERVER, put, [Name, K, V]}) ->
|
precondition(#state { open = Open }, {call, ?SERVER, put, [Name, K, V]}) ->
|
||||||
dict:is_key(Name, Open);
|
dict:is_key(Name, Open);
|
||||||
precondition(#state { open = Open }, {call, ?SERVER, open, [Name]}) ->
|
precondition(#state { open = Open }, {call, ?SERVER, open, [Name]}) ->
|
||||||
not (dict:is_key(Name, Open)).
|
not (dict:is_key(Name, Open)).
|
||||||
|
|
||||||
|
next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
|
||||||
|
S;
|
||||||
next_state(#state { open = Open} = S, _Res,
|
next_state(#state { open = Open} = S, _Res,
|
||||||
{call, ?SERVER, put, [Name, Key, Value]}) ->
|
{call, ?SERVER, put, [Name, Key, Value]}) ->
|
||||||
S#state { open = dict:update(Name,
|
S#state { open = dict:update(Name,
|
||||||
|
@ -67,6 +90,11 @@ next_state(#state { open = Open} = S, _Res,
|
||||||
next_state(#state { open = Open} = S, _Res, {call, ?SERVER, open, [Name]}) ->
|
next_state(#state { open = Open} = S, _Res, {call, ?SERVER, open, [Name]}) ->
|
||||||
S#state { open = dict:store(Name, dict:new(), Open) }.
|
S#state { open = dict:store(Name, dict:new(), Open) }.
|
||||||
|
|
||||||
|
postcondition(#state { open = Open },
|
||||||
|
{call, ?SERVER, lookup_exist, [Name, Key]}, {ok, Value}) ->
|
||||||
|
V = dict:fetch(Key, dict:fetch(Name, Open)),
|
||||||
|
io:format("~p == ~p~n", [V, Value]),
|
||||||
|
V == Value;
|
||||||
postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
|
postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
|
||||||
true;
|
true;
|
||||||
postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
|
postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
|
||||||
|
@ -74,6 +102,13 @@ postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
|
||||||
postcondition(_, _, _) ->
|
postcondition(_, _, _) ->
|
||||||
false.
|
false.
|
||||||
|
|
||||||
|
cleanup_test_trees(#state { open = Open}) ->
|
||||||
|
[cleanup_tree(N) || N <- dict:fetch_keys(Open)].
|
||||||
|
|
||||||
|
cleanup_tree(Tree) ->
|
||||||
|
{ok, FileNames} = file:list_dir(Tree),
|
||||||
|
[ok = file:delete(filename:join([Tree, Fname])) || Fname <- FileNames],
|
||||||
|
file:del_dir(Tree).
|
||||||
|
|
||||||
prop_dict_agree() ->
|
prop_dict_agree() ->
|
||||||
?FORALL(Cmds, commands(?MODULE),
|
?FORALL(Cmds, commands(?MODULE),
|
||||||
|
@ -82,6 +117,7 @@ prop_dict_agree() ->
|
||||||
fractal_btree_drv:start_link(),
|
fractal_btree_drv:start_link(),
|
||||||
{History,State,Result} = run_commands(?MODULE, Cmds),
|
{History,State,Result} = run_commands(?MODULE, Cmds),
|
||||||
fractal_btree_drv:stop(),
|
fractal_btree_drv:stop(),
|
||||||
|
cleanup_test_trees(State),
|
||||||
?WHENFAIL(io:format("History: ~w\nState: ~w\nResult: ~w\n",
|
?WHENFAIL(io:format("History: ~w\nState: ~w\nResult: ~w\n",
|
||||||
[History,State,Result]),
|
[History,State,Result]),
|
||||||
aggregate(command_names(Cmds), Result =:= ok))
|
aggregate(command_names(Cmds), Result =:= ok))
|
||||||
|
@ -93,6 +129,11 @@ prop_dict_agree() ->
|
||||||
|
|
||||||
%% UNIT TESTS -----------------------------------------------------------------
|
%% UNIT TESTS -----------------------------------------------------------------
|
||||||
|
|
||||||
|
test_tree_simple_1() ->
|
||||||
|
{ok, Tree} = fractal_btree:open("simple"),
|
||||||
|
ok = fractal_btree:put(Tree, <<>>, <<"data", 77:128>>),
|
||||||
|
{ok, <<"data", 77:128>>} = fractal_btree:lookup(Tree, <<>>).
|
||||||
|
|
||||||
|
|
||||||
test_tree() ->
|
test_tree() ->
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue