Restructure file, add deletion.

A refactoring run made the code more digestible. Also add the needed
clauses for handling random deletion.

test/fractal_btree_tests.erl

@@ -24,6 +24,7 @@ full_test_() ->
      fun (_) -> ok end,
      [{timeout, 120, ?_test(test_proper())},
       ?_test(test_tree_simple_1()),
+      ?_test(test_tree_simple_2()),
       ?_test(test_tree())]}.
 
 qc_opts() -> [{numtests, 800}].
@@ -31,34 +32,24 @@ qc_opts() -> [{numtests, 800}].
 test_proper() ->
     [?assertEqual([], proper:module(?MODULE, qc_opts()))].
 
+%% Generators
+%% ----------------------------------------------------------------------
 
-initial_state() ->
+%% Generate a name for a btree
-    #state { }.
-
 g_btree_name() ->
     ?LET(I, integer(1,10),
          "Btree_" ++ integer_to_list(I)).
 
-cmd_close_args(#state { open = Open }) ->
+%% Pick a name of a non-empty Btree
-    oneof(dict:fetch_keys(Open)).
-
-cmd_put_args(#state { open = Open }) ->
-    ?LET({Name, Key, Value},
-         {oneof(dict:fetch_keys(Open)), binary(), binary()},
-         [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}) ->
+%% Statem test
-    ?LET(Name, non_empty_btree(Open),
+%% ----------------------------------------------------------------------
-         ?LET(Key, oneof(dict:fetch_keys(dict:fetch(Name, Open))),
+initial_state() ->
-              [Name, Key])).
+    #state { }.
 
-count_dicts(Open) ->
-    Dicts = [ V || {_, V} <- dict:to_list(Open)],
-    lists:sum([dict:size(D) || D <- Dicts]).
 
 command(#state { open = Open} = S) ->
     frequency(
@@ -66,20 +57,34 @@ command(#state { open = Open} = S) ->
       [ {2000, {call, ?SERVER, put, cmd_put_args(S)}}
         || dict:size(Open) > 0] ++
       [ {1500, {call, ?SERVER, lookup_exist, cmd_lookup_args(S)}}
-        || dict:size(Open) > 0, count_dicts(Open) > 0]).
+        || dict:size(Open) > 0, count_dicts(Open) > 0] ++
+      [ {500, {call, ?SERVER, delete_exist, cmd_delete_args(S)}}
+        || dict:size(Open) > 0, count_dicts(Open) > 0 ]).
 
+%% 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_exist,
                                        [_Name, _K]}) ->
-    %% No need to quantify since we limit this to validity in the
+    %% No need to check since we limit this in the command/1 generator
-    %% 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);
 precondition(#state { open = Open }, {call, ?SERVER, open, [Name]}) ->
     not (dict:is_key(Name, Open)).
 
+%% Next state manipulation (abstract / concrete)
 next_state(S, _Res, {call, ?SERVER, lookup_exist, [_Name, _Key]}) ->
     S;
+next_state(#state { open = Open} = S, _Res,
+           {call, ?SERVER, delete_exist, [Name, Key]}) ->
+    S#state { open = dict:update(Name,
+                                 fun(Dict) ->
+                                         dict:erase(Key, Dict)
+                                 end,
+                                 Open)};
 next_state(#state { open = Open} = S, _Res,
            {call, ?SERVER, put, [Name, Key, Value]}) ->
     S#state { open = dict:update(Name,
@@ -90,11 +95,12 @@ next_state(#state { open = Open} = S, _Res,
 next_state(#state { open = Open} = S, _Res, {call, ?SERVER, open, [Name]}) ->
     S#state { open = dict:store(Name, dict:new(), Open) }.
 
+%% Postcondition check (concrete)
 postcondition(#state { open = Open },
               {call, ?SERVER, lookup_exist, [Name, Key]}, {ok, Value}) ->
-    V = dict:fetch(Key, dict:fetch(Name, Open)),
+    dict:fetch(Key, dict:fetch(Name, Open)) == Value;
-    io:format("~p == ~p~n", [V, Value]),
+postcondition(_S, {call, ?SERVER, delete_exist, [_Name, _Key]}, ok) ->
-    V == Value;
+    true;
 postcondition(_S, {call, ?SERVER, put, [_Name, _Key, _Value]}, ok) ->
     true;
 postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
@@ -102,14 +108,9 @@ postcondition(_S, {call, ?SERVER, open, [_Name]}, ok) ->
 postcondition(_, _, _) ->
     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).
 
+%% Main property. Running a random set of commands is in agreement
+%% with a dict.
 prop_dict_agree() ->
     ?FORALL(Cmds, commands(?MODULE),
             ?TRAPEXIT(
@@ -123,17 +124,17 @@ prop_dict_agree() ->
                               aggregate(command_names(Cmds), Result =:= ok))
                 end)).
 
+%% 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_simple_2() ->
+    {ok, Tree} = fractal_btree:open("simple"),
+    ok = fractal_btree:put(Tree, <<"ã">>, <<"µ">>),
+    ok = fractal_btree:delete(Tree, <<"ã">>).
 
 test_tree() ->
 
@@ -141,11 +142,51 @@ test_tree() ->
 
     {ok, Tree} = fractal_btree:open("simple"),
     lists:foldl(fun(N,_) ->
-                        ok = fractal_btree:put(Tree, <<N:128>>, <<"data",N:128>>)
+                        ok = fractal_btree:put(Tree,
+                                               <<N:128>>, <<"data",N:128>>)
                 end,
                 ok,
                 lists:seq(2,10000,1)),
 
     ok = fractal_btree:close(Tree).
 
+%% Command processing
+%% ----------------------------------------------------------------------
+cmd_close_args(#state { open = Open }) ->
+    oneof(dict:fetch_keys(Open)).
 
+cmd_put_args(#state { open = Open }) ->
+    ?LET({Name, Key, Value},
+         {oneof(dict:fetch_keys(Open)), binary(), binary()},
+         [Name, Key, Value]).
+
+
+cmd_lookup_args(#state { open = Open}) ->
+    ?LET(Name, non_empty_btree(Open),
+         ?LET(Key, oneof(dict:fetch_keys(dict:fetch(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))),
+              [Name, Key])).
+
+
+%% Context management
+%% ----------------------------------------------------------------------
+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).
+
+%% Various Helper routines
+%% ----------------------------------------------------------------------
+
+%% @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)],
+    lists:sum([dict:size(D) || D <- Dicts]).