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

Add close to shame tests

Browse source
This commit is contained in:
Kresten Krab Thorup 2012-01-07 15:16:57 +01:00
parent 99a6985eed
commit 03350aa096
2 changed files with 45 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
test/fractal_btree_drv.erl
View file

@ -9,7 +9,7 @@
-export([
delete_exist/2,
lookup_exist/2,
open/1,
open/1, close/1,
put/3,
stop/0]).
@ -39,6 +39,9 @@ delete_exist(N, K) ->
open(N) ->
call({open, N}).
close(N) ->
call({close, N}).
put(N, K, V) ->
call({put, N, K, V}).
@ -57,6 +60,14 @@ handle_call({open, N}, _, #state { btrees = D} = State) ->
Otherwise ->
{reply, {error, Otherwise}, State}
end;
handle_call({close, N}, _, #state { btrees = D} = State) ->
Tree = dict:fetch(N, D),
case fractal_btree:close(Tree) of
ok ->
{reply, ok, State#state { btrees = dict:erase(N, D)}};
Otherwise ->
{reply, {error, Otherwise}, State}
end;
handle_call({put, N, K, V}, _, #state { btrees = D} = State) ->
Tree = dict:fetch(N, D),
case fractal_btree:put(Tree, K, V) of

42
test/fractal_btree_tests.erl
View file

@ -37,25 +37,40 @@ test_proper() ->
%% Generators
%% ----------------------------------------------------------------------
-define(NUM_TREES, 10).
%% Generate a name for a btree
g_btree_name() ->
?LET(I, integer(1,10),
"Btree_" ++ integer_to_list(I)).
?LET(I, integer(1,?NUM_TREES),
btree_name(I)).
%% Pick a name of a non-empty Btree
non_empty_btree(Open) ->
?SUCHTHAT(Name, union(dict:fetch_keys(Open)),
dict:size(dict:fetch(Name, Open)) > 0).
btree_name(I) ->
"Btree_" ++ integer_to_list(I).
%% Statem test
%% ----------------------------------------------------------------------
initial_state() ->
#state { }.
ClosedBTrees = lists:foldl(fun(N, Closed) ->
dict:store(btree_name(N),
dict:new(),
Closed)
end,
dict:new(),
lists:seq(1,?NUM_TREES)),
#state { closed=ClosedBTrees }.
command(#state { open = Open} = S) ->
command(#state { open = Open, closed = Closed } = S) ->
frequency(
[ {20, {call, ?SERVER, open, [g_btree_name()]}} ] ++
[ {20, {call, ?SERVER, open, [oneof(dict:fetch_keys(Closed))]}}
|| dict:size(Closed) > 0] ++
[ {20, {call, ?SERVER, close, [oneof(dict:fetch_keys(Open))]}}
|| dict:size(Open) > 0] ++
[ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
|| dict:size(Open) > 0] ++
[ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
@ -74,8 +89,11 @@ precondition(#state { open = _Open }, {call, ?SERVER, lookup_exist,
true;
precondition(#state { open = Open }, {call, ?SERVER, put, [Name, _K, _V]}) ->
dict:is_key(Name, Open);
precondition(#state { open = Open }, {call, ?SERVER, open, [Name]}) ->
not (dict:is_key(Name, Open)).
precondition(#state { open = Open, closed = Closed }, {call, ?SERVER, open, [Name]}) ->
(not (dict:is_key(Name, Open))) and (dict:is_key(Name, Closed));
precondition(#state { open = Open, closed = Closed }, {call, ?SERVER, close, [Name]}) ->
(dict:is_key(Name, Open)) and (not dict:is_key(Name, Closed)).
%% Next state manipulation (abstract / concrete)
next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
@ -94,8 +112,12 @@ next_state(#state { open = Open} = S, _Res,
dict:store(Key, Value, Dict)
end,
Open)};
next_state(#state { open = Open} = S, _Res, {call, ?SERVER, open, [Name]}) ->
S#state { open = dict:store(Name, dict:new(), Open) }.
next_state(#state { open = Open, closed=Closed} = S, _Res, {call, ?SERVER, open, [Name]}) ->
S#state { open = dict:store(Name, dict:fetch(Name, Closed) , Open),
closed = dict:erase(Name, Closed) };
next_state(#state { open = Open, closed=Closed} = S, _Res, {call, ?SERVER, close, [Name]}) ->
S#state { closed = dict:store(Name, dict:fetch(Name, Open) , Closed),
open = dict:erase(Name, Open) }.
%% Postcondition check (concrete)
postcondition(#state { open = Open },
@ -107,6 +129,8 @@ postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
true;
postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
true;
postcondition(_S, {call, ?SERVER, close, [_Name]}, ok) ->
true;
postcondition(_, _, _) ->
false.