greg/hanoidb
1
0
Fork 0
Code Issues 10 Pull requests 3 Projects Releases Packages Wiki Activity

Work on failing keys. Optimize generator.

Browse source 
To make failing keys work we must be able to produce a key in fewer
failures then currently. So encode the picker for non-empty trees
directly so it is much faster and doesn't try to do it by generating a
case and then asking "is this one good enough?". A simple
dict:filter/2 does it.
This commit is contained in:
Jesper Louis Andersen 2012-01-07 22:58:38 +01:00
parent 6b8683bb08
commit c8b9a6183f
1 changed files with 61 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

73
test/lsm_btree_tests.erl
View file

@ -55,10 +55,32 @@ g_btree_name() ->
?LET(I, choose(1,?NUM_TREES),
btree_name(I)).
%% Generate a key for the Tree
g_key() ->
binary().
%% Generate a value for the Tree
g_value() ->
binary().
g_fail_key() ->
?LET(T, choose(1,999999999999),
term_to_binary(T)).
%% Pick a name of a non-empty Btree
non_empty_btree(Open) ->
?SUCHTHAT(Name, oneof(dict:fetch_keys(Open)),
dict:size(dict:fetch(Name, Open)) > 0).
TreesWithKeys = dict:filter(fun(_K, D) -> dict:size(D) > 0 end, Open),
oneof(dict:fetch_keys(TreesWithKeys)).
g_existing_key(Name, Open) ->
oneof(dict:fetch_keys(dict:fetch(Name, Open))).
g_non_existing_key(Name, Open) ->
?SUCHTHAT(Key, g_fail_key(),
begin
D = dict:fetch(Name, Open),
not dict:is_key(Key, D)
end).
btree_name(I) ->
"Btree_" ++ integer_to_list(I).
@ -79,21 +101,27 @@ initial_state() ->
command(#state { open = Open, closed = Closed } = S) ->
frequency(
[ {20, {call, ?SERVER, open, [oneof(dict:fetch_keys(Closed))]}}
|| dict:size(Closed) > 0] ++
|| closed_dicts(S)] ++
[ {20, {call, ?SERVER, close, [oneof(dict:fetch_keys(Open))]}}
|| dict:size(Open) > 0] ++
|| open_dicts(S)] ++
[ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|| dict:size(Open) > 0] ++
|| open_dicts(S)] ++
%% [ {1500, {call, ?SERVER, lookup_fail, cmd_lookup_fail_args(S)}}
%% || open_dicts(S)] ++
[ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
|| dict:size(Open) > 0, count_dicts(Open) > 0] ++
|| open_dicts(S), open_dicts_with_keys(S)] ++
[ {500, {call, ?SERVER, delete_exist, cmd_delete_args(S)}}
|| dict:size(Open) > 0, count_dicts(Open) > 0 ]).
|| open_dicts(S), open_dicts_with_keys(S)]).
%% Precondition (abstract)
precondition(#state { open = _Open}, {call, ?SERVER, delete_exist,
[_Name, _K]}) ->
%% No need to check since we limit this in the command/1 generator
true;
precondition(#state { open = _Open }, {call, ?SERVER, lookup_fail,
[_Name, _K]}) ->
%% We can always try to look up some non-existing key
true;
precondition(#state { open = _Open }, {call, ?SERVER, lookup_exist,
[_Name, _K]}) ->
%% No need to check since we limit this in the command/1 generator
@ -107,6 +135,8 @@ precondition(#state { open = Open, closed = Closed }, {call, ?SERVER, close, [Na
%% Next state manipulation (abstract / concrete)
next_state(S, _Res, {call, ?SERVER, lookup_fail, [_Name, _Key]}) ->
S;
next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
S;
next_state(#state { open = Open} = S, _Res,
@ -131,6 +161,9 @@ next_state(#state { open = Open, closed=Closed} = S, _Res, {call, ?SERVER, close
open = dict:erase(Name, Open) }.
%% Postcondition check (concrete)
postcondition(S,
{call, ?SERVER, lookup_fail, [_Name, _Key]}, notfound) ->
true;
postcondition(#state { open = Open },
{call, ?SERVER, lookup_exist, [Name, Key]}, {ok, Value}) ->
dict:fetch(Key, dict:fetch(Name, Open)) == Value;
@ -196,18 +229,23 @@ cmd_close_args(#state { open = Open }) ->
cmd_put_args(#state { open = Open }) ->
?LET({Name, Key, Value},
{oneof(dict:fetch_keys(Open)), binary(), binary()},
{oneof(dict:fetch_keys(Open)), g_key(), g_value()},
[Name, Key, Value]).
cmd_lookup_fail_args(#state { open = Open}) ->
?LET(Name, non_empty_btree(Open),
?LET(Key, g_non_existing_key(Name, Open),
[Name, Key])).
cmd_lookup_args(#state { open = Open}) ->
?LET(Name, non_empty_btree(Open),
?LET(Key, oneof(dict:fetch_keys(dict:fetch(Name, Open))),
?LET(Key, g_existing_key(Name, Open),
[Name, Key])).
cmd_delete_args(#state { open = Open}) ->
?LET(Name, non_empty_btree(Open),
?LET(Key, oneof(dict:fetch_keys(dict:fetch(Name, Open))),
?LET(Key, g_existing_key(Name, Open),
[Name, Key])).
@ -226,6 +264,17 @@ cleanup_tree(Tree) ->
%% @todo optimize this call. You can fast-exit as soon as you know
%% there is a non-empty dict.
count_dicts(Open) ->
Dicts = [ V || {_, V} <- dict:to_list(Open)],
open_dicts_with_keys(#state { open = Open}) ->
keysum_of_dicts(Open) > 0.
keysum_of_dicts(DictOfDict) ->
Dicts = [ V || {_, V} <- dict:to_list(DictOfDict)],
lists:sum([dict:size(D) || D <- Dicts]).
open_dicts(#state { open = Open}) ->
dict:size(Open) > 0.
closed_dicts(#state { closed = Closed}) ->
dict:size(Closed) > 0.