797 lines
29 KiB
Erlang
797 lines
29 KiB
Erlang
%%% The MIT License
|
|
%%%
|
|
%%% Copyright (C) 2011 by Joseph Wayne Norton <norton@alum.mit.edu>
|
|
%%%
|
|
%%% Permission is hereby granted, free of charge, to any person obtaining a copy
|
|
%%% of this software and associated documentation files (the "Software"), to deal
|
|
%%% in the Software without restriction, including without limitation the rights
|
|
%%% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
|
%%% copies of the Software, and to permit persons to whom the Software is
|
|
%%% furnished to do so, subject to the following conditions:
|
|
%%%
|
|
%%% The above copyright notice and this permission notice shall be included in
|
|
%%% all copies or substantial portions of the Software.
|
|
%%%
|
|
%%% THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
|
%%% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
|
%%% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
|
%%% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
|
%%% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
|
%%% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
|
%%% THE SOFTWARE.
|
|
|
|
-module(qc_statem_lets).
|
|
|
|
-ifdef(QC).
|
|
|
|
%% qc_statem Callbacks
|
|
-behaviour(qc_statem).
|
|
-export([command_gen/2]).
|
|
-export([initial_state/0, state_is_sane/1, next_state/3, precondition/2, postcondition/3]).
|
|
-export([setup/1, teardown/1, teardown/2, aggregate/1]).
|
|
|
|
%% @TODO remove at time of db, db_read, db_write options testing
|
|
%% DEBUG
|
|
-compile(export_all).
|
|
%% Implementation
|
|
-export([match31/3, match_object31/3, select31/3, select_reverse31/3]).
|
|
|
|
%% @NOTE For boilerplate exports, see "qc_statem.hrl"
|
|
-include_lib("qc/include/qc_statem.hrl").
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% defines, types, records
|
|
%%%----------------------------------------------------------------------
|
|
|
|
%%-define(IMPL, qc_lets_raw).
|
|
%%-define(IMPL, qc_lets_proxy).
|
|
-define(IMPL, qc_lets_slave_proxy).
|
|
|
|
-define(TAB, ?MODULE).
|
|
-define(INT_KEYS, lists:seq(0,10)).
|
|
-define(FLOAT_KEYS, [float(Key) || Key <- ?INT_KEYS]).
|
|
-define(BINARY_KEYS, [term_to_binary(Key) || Key <- ?INT_KEYS]).
|
|
|
|
-type key() :: integer() | float() | binary() | atom().
|
|
-type val() :: integer() | float() | binary() | atom().
|
|
|
|
-record(obj, {
|
|
key :: key(),
|
|
val :: val()
|
|
}).
|
|
|
|
-type obj() :: #obj{}.
|
|
-type ets_type() :: set | ordered_set. %% default is set
|
|
-type ets_impl() :: drv | nif | ets. %% default is drv
|
|
|
|
-record(state, {
|
|
parallel=false :: boolean(),
|
|
type=undefined :: undefined | ets_type(),
|
|
impl=undefined :: undefined | ets_impl(),
|
|
exists=false :: boolean(),
|
|
tab=undefined :: undefined | tuple(),
|
|
objs=[] :: [obj()]
|
|
}).
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% qc_statem Callbacks
|
|
%%%----------------------------------------------------------------------
|
|
|
|
command_gen(Mod,#state{parallel=false}=S) ->
|
|
serial_command_gen(Mod,S);
|
|
command_gen(Mod,#state{parallel=true}=S) ->
|
|
parallel_command_gen(Mod,S).
|
|
|
|
serial_command_gen(_Mod,#state{tab=undefined, type=undefined, impl=undefined}=S) ->
|
|
{call,?IMPL,new,[?TAB,gen_options(new,S)]};
|
|
serial_command_gen(_Mod,#state{tab=undefined}=S) ->
|
|
oneof([{call,?IMPL,new,[undefined,?TAB,gen_options(new,S)]}]
|
|
%% @TODO ++ [{call,?IMPL,destroy,[undefined,?TAB,gen_options(destroy,S)]}]
|
|
%% @TODO ++ [{call,?IMPL,repair,[undefined,?TAB,gen_options(repair,S)]}]
|
|
);
|
|
serial_command_gen(_Mod,#state{tab=Tab, type=Type, impl=Impl}=S) ->
|
|
%% @TODO gen_db_write_options/2
|
|
%% @TODO gen_db_read_options/2
|
|
%% @TODO info/1, info/2
|
|
oneof([{call,?IMPL,insert,[Tab,oneof([gen_obj(S),gen_objs(S)])]}]
|
|
++ [{call,?IMPL,insert_new,[Tab,oneof([gen_obj(S),gen_objs(S)])]} || Impl =:= ets]
|
|
++ [{call,?IMPL,delete,[Tab]}]
|
|
++ [{call,?IMPL,delete,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,delete_all_objects,[Tab]} || Type =:= ets]
|
|
++ [{call,?IMPL,member,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,lookup,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,lookup_element,[Tab,gen_key(S),choose(1,record_info(size,obj))]}]
|
|
++ [{call,?IMPL,first,[Tab]}]
|
|
++ [{call,?IMPL,last,[Tab]}]
|
|
++ [{call,?IMPL,next,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,prev,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,foldl,[fun(X,Acc) -> [X|Acc] end, [], Tab]}]
|
|
++ [{call,?IMPL,foldr,[fun(X,Acc) -> [X|Acc] end, [], Tab]}]
|
|
++ [{call,?IMPL,tab2list,[Tab]}]
|
|
++ [{call,?IMPL,match,[Tab, gen_pattern(S)]}]
|
|
%%++ [{call,?MODULE,match31,[Tab, gen_pattern(S), gen_pos_integer()]}]
|
|
++ [{call,?IMPL,match_delete,[Tab, gen_pattern(S)]}]
|
|
++ [{call,?IMPL,match_object,[Tab, gen_pattern(S)]}]
|
|
%%++ [{call,?MODULE,match_object31,[Tab, gen_pattern(S), gen_pos_integer()]}]
|
|
++ [{call,?IMPL,select,[Tab, gen_spec(S)]}]
|
|
++ [{call,?MODULE,select31,[Tab, gen_spec(S), gen_pos_integer()]}]
|
|
++ [{call,?IMPL,select_count,[Tab, gen_spec_true(S)]}]
|
|
++ [{call,?IMPL,select_delete,[Tab, gen_spec_true(S)]}]
|
|
++ [{call,?IMPL,select_reverse,[Tab, gen_spec(S)]}]
|
|
%%++ [{call,?MODULE,select_reverse31,[Tab, gen_spec(S), gen_pos_integer()]}]
|
|
).
|
|
|
|
parallel_command_gen(_Mod,#state{tab=undefined, type=undefined, impl=undefined}=S) ->
|
|
{call,?IMPL,new,[?TAB,gen_options(new,S)]};
|
|
parallel_command_gen(_Mod,#state{tab=Tab, type=Type}=S) ->
|
|
%% @TODO gen_db_write_options/2
|
|
%% @TODO gen_db_read_options/2
|
|
oneof([{call,?IMPL,insert,[Tab,oneof([gen_obj(S),gen_objs(S)])]}]
|
|
++ [{call,?IMPL,insert_new,[Tab,oneof([gen_obj(S),gen_objs(S)])]} || Type =:= ets]
|
|
++ [{call,?IMPL,delete,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,member,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,lookup,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,lookup_element,[Tab,gen_key(S),choose(1,record_info(size,obj))]}]
|
|
++ [{call,?IMPL,first,[Tab]}]
|
|
++ [{call,?IMPL,last,[Tab]}]
|
|
++ [{call,?IMPL,next,[Tab,gen_key(S)]}]
|
|
++ [{call,?IMPL,prev,[Tab,gen_key(S)]}]
|
|
).
|
|
|
|
-spec initial_state() -> #state{}.
|
|
initial_state() ->
|
|
?LET(Parallel,parameter(parallel,false),
|
|
#state{parallel=Parallel}).
|
|
|
|
-spec state_is_sane(#state{}) -> boolean().
|
|
state_is_sane(_S) ->
|
|
%% @TODO
|
|
true.
|
|
|
|
-spec next_state(#state{}, term(), tuple()) -> #state{}.
|
|
next_state(#state{tab=undefined, type=undefined, impl=undefined}=S, V, {call,_,new,[?TAB,Options]}) ->
|
|
%% @TODO Options
|
|
case [proplists:get_bool(X, Options) || X <- [set, ordered_set]] of
|
|
[_, false] ->
|
|
Type = set;
|
|
[false, true] ->
|
|
Type = ordered_set
|
|
end,
|
|
case [proplists:get_bool(X, Options) || X <- [drv, nif, ets]] of
|
|
[_, false, false] ->
|
|
Impl = drv;
|
|
[false, true, _] ->
|
|
Impl = nif;
|
|
[false, false, true] ->
|
|
Impl = ets
|
|
end,
|
|
S#state{type=Type, impl=Impl, exists=true, tab=V};
|
|
next_state(#state{tab=undefined}=S, V, {call,_,new,[_Tab,?TAB,Options]}) ->
|
|
%% @TODO Options
|
|
case [proplists:get_bool(X, Options) || X <- [set, ordered_set]] of
|
|
[_, false] ->
|
|
Type = set;
|
|
[false, true] ->
|
|
Type = ordered_set
|
|
end,
|
|
case [proplists:get_bool(X, Options) || X <- [drv, nif, ets]] of
|
|
[_, false, false] ->
|
|
Impl = drv;
|
|
[false, true, _] ->
|
|
Impl = nif;
|
|
[false, false, true] ->
|
|
Impl = ets
|
|
end,
|
|
S#state{type=Type, impl=Impl, exists=true, tab=V};
|
|
next_state(#state{impl=Impl}=S, _V, {call,_,destroy,[_Tab,?TAB,_Options]})
|
|
when Impl =/= ets ->
|
|
S#state{tab=undefined, exists=false, objs=[]};
|
|
next_state(S, _V, {call,_,insert,[_Tab,Objs]}) when is_list(Objs) ->
|
|
insert_objs(S, Objs);
|
|
next_state(S, _V, {call,_,insert,[_Tab,Obj]}) ->
|
|
insert_objs(S, [Obj]);
|
|
next_state(#state{impl=ets}=S, _V, {call,_,insert_new,[_Tab,Objs]}) when is_list(Objs) ->
|
|
insert_new_objs(S, Objs);
|
|
next_state(#state{impl=ets}=S, _V, {call,_,insert_new,[_Tab,Obj]}) ->
|
|
insert_new_objs(S, [Obj]);
|
|
next_state(S, _V, {call,_,insert_new,[_Tab,_ObjOrObjs]}) ->
|
|
S;
|
|
next_state(#state{impl=ets}=S, _V, {call,_,delete,[_Tab]}) ->
|
|
S#state{tab=undefined, exists=false, objs=[]};
|
|
next_state(#state{exists=Exists}=S, _V, {call,_,delete,[_Tab]}) ->
|
|
S#state{tab=undefined, exists=Exists};
|
|
next_state(S, _V, {call,_,delete,[_Tab,Key]}) ->
|
|
S#state{objs=keydelete(Key, S)};
|
|
next_state(#state{impl=ets}=S, _V, {call,_,delete_all_objects,[_Tab]}) ->
|
|
S#state{objs=[]};
|
|
next_state(S, _V, {call,_,delete_all_objects,[_Tab]}) ->
|
|
S;
|
|
next_state(S, _V, {call,_,match_delete,[_Tab,Pattern]}) ->
|
|
match_delete(S, Pattern);
|
|
next_state(S, _V, {call,_,select_delete,[_Tab,Spec]}) ->
|
|
select_delete(S, Spec);
|
|
next_state(S, _V, {call,_,_,_}) ->
|
|
S.
|
|
|
|
-spec precondition(#state{}, tuple()) -> boolean().
|
|
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,new,[?TAB,Options]}) ->
|
|
Drv = proplists:get_bool(drv, Options),
|
|
Nif = proplists:get_bool(nif, Options),
|
|
if Drv orelse Nif ->
|
|
L = proplists:get_value(db, Options, []),
|
|
proplists:get_bool(create_if_missing, L) andalso proplists:get_bool(error_if_exists, L);
|
|
true ->
|
|
true
|
|
end;
|
|
precondition(#state{tab=_Tab}, {call,_,new,[?TAB,_Options]}) ->
|
|
false;
|
|
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,new,[_Tab,?TAB,_Options]}) ->
|
|
false;
|
|
precondition(#state{tab=Tab}, {call,_,new,[_Tab,?TAB,_Options]}) ->
|
|
Tab =:= undefined;
|
|
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,destroy,[_Tab,?TAB,_Options]}) ->
|
|
false;
|
|
precondition(#state{tab=Tab}, {call,_,destroy,[_Tab,?TAB,_Options]}) ->
|
|
Tab =:= undefined;
|
|
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,repair,[_Tab,?TAB,_Options]}) ->
|
|
false;
|
|
precondition(#state{tab=Tab}, {call,_,repair,[_Tab,?TAB,_Options]}) ->
|
|
Tab =:= undefined;
|
|
precondition(_S, {call,_,_,_}) ->
|
|
true.
|
|
|
|
-spec postcondition(#state{}, tuple(), term()) -> boolean().
|
|
postcondition(#state{tab=undefined}, {call,_,new,[?TAB,_Options]}, Res) ->
|
|
?IMPL:is_table(Res);
|
|
postcondition(_S, {call,_,new,[?TAB,_Options]}, Res) ->
|
|
case Res of
|
|
{'EXIT', {badarg, _}} ->
|
|
true;
|
|
_ ->
|
|
false
|
|
end;
|
|
postcondition(#state{tab=undefined}, {call,_,new,[_Tab,?TAB,_Options]}, Res) ->
|
|
?IMPL:is_table(Res);
|
|
postcondition(_S, {call,_,destroy,[_Tab,?TAB,_Options]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(_S, {call,_,repair,[_Tab,?TAB,_Options]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(_S, {call,_,insert,[_Tab,_ObjOrObjs]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(#state{impl=ets}=S, {call,_,insert_new,[_Tab,Objs]}, Res) when is_list(Objs) ->
|
|
Res =:= has_insert_new_objs(S, Objs);
|
|
postcondition(#state{impl=ets}=S, {call,_,insert_new,[_Tab,Obj]}, Res) ->
|
|
Res =:= has_insert_new_objs(S, [Obj]);
|
|
postcondition(_S, {call,_,insert_new,[_Tab,_ObjOrObjs]}, {'EXIT',{badarg,_}}) ->
|
|
true;
|
|
postcondition(_S, {call,_,delete,[_Tab]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(_S, {call,_,delete,[_Tab,_Key]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(#state{impl=ets}=_S, {call,_,delete_all_objects,[_Tab]}, Res) ->
|
|
Res =:= true;
|
|
postcondition(_S, {call,_,delete_all_objects,[_Tab]}, {'EXIT',{badarg,_}}) ->
|
|
true;
|
|
postcondition(S, {call,_,member,[_Tab,Key]}, Res) ->
|
|
Res =:= keymember(Key, S);
|
|
postcondition(S, {call,_,lookup,[_Tab,Key]}, Res) ->
|
|
Res =:= keyfind(Key, S);
|
|
postcondition(S, {call,_,lookup_element,[_Tab,Key,_Pos]}, {'EXIT',{badarg,_}}) ->
|
|
not keymember(Key, S);
|
|
postcondition(S, {call,_,lookup_element,[_Tab,Key,Pos]}, Res) ->
|
|
[Res] =:= keyposfind(Key, Pos, S);
|
|
postcondition(#state{objs=[]}, {call,_,first,[_Tab]}, Res) ->
|
|
Res =:= '$end_of_table';
|
|
postcondition(#state{type=set}=S, {call,_,first,[_Tab]}, Res) ->
|
|
keymember(Res, S);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,first,[_Tab]}, Res) ->
|
|
#obj{key=K} = hd(sort(S)),
|
|
Res =:= K;
|
|
postcondition(#state{objs=[]}, {call,_,last,[_Tab]}, Res) ->
|
|
Res =:= '$end_of_table';
|
|
postcondition(#state{type=set}=S, {call,_,last,[_Tab]}, Res) ->
|
|
keymember(Res, S);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,last,[_Tab]}, Res) ->
|
|
#obj{key=K} = hd(rsort(S)),
|
|
Res =:= K;
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,next,[_Tab, Key]}, {'EXIT',{badarg,_}}) ->
|
|
not keymember(Key, S);
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,next,[_Tab, Key]}, '$end_of_table') ->
|
|
keymember(Key, S);
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,next,[_Tab, Key]}, Res) ->
|
|
keymember(Key, S) andalso keymember(Res, S);
|
|
postcondition(#state{type=set}, {call,_,next,[_Tab, _Key]}, '$end_of_table') ->
|
|
true;
|
|
postcondition(#state{type=set}=S, {call,_,next,[_Tab, _Key]}, Res) ->
|
|
keymember(Res, S);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,next,[_Tab, Key]}, Res) ->
|
|
case lists:dropwhile(fun(#obj{key=X}) -> lteq(X, Key, S) end, sort(S)) of
|
|
[] ->
|
|
Res =:= '$end_of_table';
|
|
[#obj{key=K}|_] ->
|
|
Res =:= K
|
|
end;
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,prev,[_Tab, Key]}, {'EXIT',{badarg,_}}) ->
|
|
not keymember(Key, S);
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,prev,[_Tab, Key]}, '$end_of_table') ->
|
|
keymember(Key, S);
|
|
postcondition(#state{impl=ets, type=set}=S, {call,_,prev,[_Tab, Key]}, Res) ->
|
|
keymember(Key, S) andalso keymember(Res, S);
|
|
postcondition(#state{type=set}, {call,_,prev,[_Tab, _Key]}, '$end_of_table') ->
|
|
true;
|
|
postcondition(#state{type=set}=S, {call,_,prev,[_Tab, _Key]}, Res) ->
|
|
keymember(Res, S);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,prev,[_Tab, Key]}, Res) ->
|
|
case lists:dropwhile(fun(#obj{key=X}) -> gteq(X, Key, S) end, rsort(S)) of
|
|
[] ->
|
|
Res =:= '$end_of_table';
|
|
[#obj{key=K}|_] ->
|
|
Res =:= K
|
|
end;
|
|
postcondition(#state{type=set}=S, {call,_,foldl,[_Function,_Acc0,_Tab]}, Res) ->
|
|
[] =:= (S#state.objs -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,foldl,[_Function,_Acc0,_Tab]}, Res) ->
|
|
rsort(S) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,foldr,[_Function,_Acc0,_Tab]}, Res) ->
|
|
[] =:= (S#state.objs -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,foldr,[_Function,_Acc0,_Tab]}, Res) ->
|
|
sort(S) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,tab2list,[_Tab]}, Res) ->
|
|
[] =:= (S#state.objs -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,tab2list,[_Tab]}, Res) ->
|
|
sort(S) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,match,[_Tab,Pattern]}, Res) ->
|
|
[] =:= (match(S, Pattern) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,match,[_Tab,Pattern]}, Res) ->
|
|
match(S, Pattern) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,match31,[_Tab,Pattern,_Limit]}, Res) ->
|
|
[] =:= (match(S, Pattern) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,match31,[_Tab,Pattern,_Limit]}, Res) ->
|
|
match(S, Pattern) =:= Res;
|
|
postcondition(_S, {call,_,match_delete,[_Tab,_Pattern]}, Res) ->
|
|
Res;
|
|
postcondition(#state{type=set}=S, {call,_,match_object,[_Tab,Pattern]}, Res) ->
|
|
[] =:= (match_object(S, Pattern) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,match_object,[_Tab,Pattern]}, Res) ->
|
|
match_object(S, Pattern) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,match_object31,[_Tab,Pattern,_Limit]}, Res) ->
|
|
[] =:= (match_object(S, Pattern) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,match_object31,[_Tab,Pattern,_Limit]}, Res) ->
|
|
match_object(S, Pattern) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,select,[_Tab,Spec]}, Res) ->
|
|
[] =:= (select(S, Spec) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,select,[_Tab,Spec]}, Res) ->
|
|
select(S, Spec) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,select31,[_Tab,Spec,_Limit]}, Res) ->
|
|
[] =:= (select(S, Spec) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,select31,[_Tab,Spec,_Limit]}, Res) ->
|
|
select(S, Spec) =:= Res;
|
|
postcondition(S, {call,_,select_count,[_Tab,Spec]}, Res) ->
|
|
select_count(S, Spec) =:= Res;
|
|
postcondition(S, {call,_,select_delete,[_Tab,Spec]}, Res) ->
|
|
select_count(S, Spec) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,select_reverse,[_Tab,Spec]}, Res) ->
|
|
[] =:= (select_reverse(S, Spec) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,select_reverse,[_Tab,Spec]}, Res) ->
|
|
select_reverse(S, Spec) =:= Res;
|
|
postcondition(#state{type=set}=S, {call,_,select_reverse31,[_Tab,Spec,_Limit]}, Res) ->
|
|
[] =:= (select_reverse(S, Spec) -- Res);
|
|
postcondition(#state{type=ordered_set}=S, {call,_,select_reverse31,[_Tab,Spec,_Limit]}, Res) ->
|
|
select_reverse(S, Spec) =:= Res;
|
|
postcondition(_S, {call,_,_,_}, _Res) ->
|
|
false.
|
|
|
|
-spec setup(boolean()) -> {ok, term()}.
|
|
setup(_Hard) ->
|
|
?IMPL:teardown(?TAB),
|
|
{ok, unused}.
|
|
|
|
-spec teardown(term()) -> ok.
|
|
teardown(unused) ->
|
|
?IMPL:teardown(?TAB),
|
|
ok.
|
|
|
|
-spec teardown(term(), #state{}) -> ok.
|
|
teardown(Ref, _State) ->
|
|
teardown(Ref).
|
|
|
|
-spec aggregate([{integer(), term(), term(), #state{}}])
|
|
-> [{atom(), atom(), integer() | term()}].
|
|
aggregate(L) ->
|
|
[ {Cmd,filter_reply(Reply)} || {_N,{set,_,{call,_,Cmd,_}},Reply,_State} <- L ].
|
|
|
|
filter_reply({'EXIT',{Err,_}}) ->
|
|
{error,Err};
|
|
filter_reply(_) ->
|
|
ok.
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% Internal - Generators
|
|
%%%----------------------------------------------------------------------
|
|
|
|
gen_options(Op,#state{tab=undefined, type=undefined, impl=undefined}=S) ->
|
|
?LET({Type,Impl}, {gen_ets_type(), gen_ets_impl()},
|
|
gen_options(Op,S#state{type=Type, impl=Impl}));
|
|
gen_options(Op,#state{type=Type, impl=drv=Impl}=S) ->
|
|
[Type, public, named_table, {keypos,#obj.key},
|
|
{compressed, gen_boolean()}, {async, gen_boolean()}, Impl]
|
|
++ gen_leveldb_options(Op,S);
|
|
gen_options(Op,#state{type=Type, impl=nif=Impl}=S) ->
|
|
[Type, public, named_table, {keypos,#obj.key},
|
|
{compressed, gen_boolean()}, {async, gen_boolean()}, Impl]
|
|
++ gen_leveldb_options(Op,S);
|
|
gen_options(_Op,#state{type=Type, impl=ets=Impl}) ->
|
|
[Type, public, named_table, {keypos,#obj.key},
|
|
{compressed, gen_boolean()}, Impl].
|
|
|
|
gen_leveldb_options(Op,S) ->
|
|
[gen_db_options(Op,S), gen_db_read_options(Op,S), gen_db_write_options(Op,S)].
|
|
|
|
gen_db_options(new,#state{exists=Exists}) ->
|
|
ExistsOptions = if Exists -> []; true -> [create_if_missing, error_if_exists] end,
|
|
%% @TODO ?LET(Options, ulist(gen_db_options()), {db, Options ++ ExistsOptions});
|
|
{db, ExistsOptions};
|
|
gen_db_options(_Op,_S) ->
|
|
%% @TODO ?LET(Options, ulist(gen_db_options()), {db, Options}).
|
|
{db, []} .
|
|
|
|
gen_db_read_options(_Op,_S) ->
|
|
%% @TODO ?LET(Options, ulist(gen_db_read_options()), {db_read, Options}).
|
|
{db_read, []}.
|
|
|
|
gen_db_write_options(_Op,_S) ->
|
|
%% @TODO ?LET(Options, ulist(gen_db_write_options()), {db_write, Options}).
|
|
{db_write, []}.
|
|
|
|
gen_db_options() ->
|
|
oneof([paranoid_checks, {paranoid_checks,gen_boolean()}, {write_buffer_size,gen_pos_integer()}, {max_open_files,gen_pos_integer()}, {block_cache_size,gen_pos_integer()}, {block_size,gen_pos_integer()}, {block_restart_interval,gen_pos_integer()}]).
|
|
|
|
gen_db_read_options() ->
|
|
oneof([verify_checksums, {verify_checksums,gen_boolean()}, fill_cache, {fill_cache,gen_boolean()}]).
|
|
|
|
gen_db_write_options() ->
|
|
oneof([sync, {sync,gen_boolean()}]).
|
|
|
|
gen_boolean() ->
|
|
oneof([true, false]).
|
|
|
|
gen_pos_integer() ->
|
|
?LET(N, nat(), N+1).
|
|
|
|
gen_ets_type() ->
|
|
noshrink(oneof([set, ordered_set])).
|
|
|
|
gen_ets_impl() ->
|
|
%% @NOTE Remove one or two of these to restrict to a particular
|
|
%% implementation.
|
|
noshrink(oneof([drv,nif,ets])).
|
|
|
|
gen_integer_key() ->
|
|
oneof(?INT_KEYS).
|
|
|
|
gen_float_key() ->
|
|
oneof(?FLOAT_KEYS).
|
|
|
|
gen_binary_key() ->
|
|
oneof(?BINARY_KEYS).
|
|
|
|
gen_key() ->
|
|
frequency([{5, gen_integer_key()}, {1, gen_float_key()}, {1, gen_binary_key()}]).
|
|
|
|
gen_key(#state{objs=[]}) ->
|
|
gen_key();
|
|
gen_key(#state{objs=Objs}) ->
|
|
oneof([?LET(Obj, oneof(Objs), Obj#obj.key), gen_key()]).
|
|
|
|
gen_int_or_float_or_bin() ->
|
|
frequency([{5, int()}, {1, real()}, {1, binary()}]).
|
|
|
|
gen_val() ->
|
|
gen_int_or_float_or_bin().
|
|
|
|
gen_obj() ->
|
|
#obj{key=gen_key(), val=gen_val()}.
|
|
|
|
gen_obj(#state{objs=[]}) ->
|
|
gen_obj();
|
|
gen_obj(#state{objs=Objs}) ->
|
|
oneof([oneof(Objs), gen_obj()]).
|
|
|
|
gen_objs(S) ->
|
|
frequency([{9, non_empty(list(gen_obj(S)))}, {1, list(gen_obj(S))}]).
|
|
|
|
gen_pattern(S) ->
|
|
oneof([{'$1', '$2', '$3'}
|
|
, #obj{key=oneof(['_',gen_key(S)]), val='$1'}
|
|
, #obj{key='$1', val=oneof(['_',gen_val()])}
|
|
]).
|
|
|
|
gen_spec(S) ->
|
|
[{gen_pattern(S), [], [oneof(['$$', '$_'])]}].
|
|
|
|
gen_spec_true(S) ->
|
|
[{gen_pattern(S), [], [true]}].
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% Internal - Model
|
|
%%%----------------------------------------------------------------------
|
|
|
|
insert_objs(S, []) ->
|
|
S;
|
|
insert_objs(S, [#obj{key=K}=Obj|T]) ->
|
|
case keymember(K, S) of
|
|
false ->
|
|
insert_objs(S#state{objs=[Obj|S#state.objs]}, T);
|
|
true ->
|
|
insert_objs(S#state{objs=keyreplace(K, Obj, S)}, T)
|
|
end.
|
|
|
|
insert_new_objs(S, L) ->
|
|
insert_new_objs(S, lists:reverse(L), S).
|
|
|
|
insert_new_objs(S, [], _S0) ->
|
|
S;
|
|
insert_new_objs(S, [#obj{key=K}=Obj|T], S0) ->
|
|
case keymember(K, S) of
|
|
false ->
|
|
NewT = keydelete(K, T, S),
|
|
insert_new_objs(S#state{objs=[Obj|S#state.objs]}, NewT, S0);
|
|
true ->
|
|
S0
|
|
end.
|
|
|
|
has_insert_new_objs(S, L) ->
|
|
has_insert_new_objs(S, lists:reverse(L), true).
|
|
|
|
has_insert_new_objs(_S, [], Bool) ->
|
|
Bool;
|
|
has_insert_new_objs(S, [#obj{key=K}=Obj|T], _Bool) ->
|
|
case keymember(K, S) of
|
|
false ->
|
|
NewT = keydelete(K, T, S),
|
|
has_insert_new_objs(S#state{objs=[Obj|S#state.objs]}, NewT, true);
|
|
true ->
|
|
false
|
|
end.
|
|
|
|
keydelete(X, #state{objs=L}=S) ->
|
|
keydelete(X, L, S).
|
|
|
|
keydelete(X, L, S) ->
|
|
lists:filter(fun(#obj{key=K}) -> neq(X, K, S) end, L).
|
|
|
|
keyreplace(X, Y, #state{objs=L}=S) ->
|
|
lists:map(fun(Z=#obj{key=K}) -> case eq(X, K, S) of true -> Y; false -> Z end end, L).
|
|
|
|
keymember(X, S) ->
|
|
[] =/= keyfind(X, S).
|
|
|
|
keyfind(X, #state{objs=L}=S) ->
|
|
lists:filter(fun(#obj{key=K}) -> eq(X, K, S) end, L).
|
|
|
|
keyposfind(X, Pos, S) ->
|
|
[ element(Pos, Obj) || Obj <- keyfind(X, S) ].
|
|
|
|
match(S, Pattern) ->
|
|
select(S, [{Pattern, [], ['$$']}]).
|
|
|
|
match(S, Pattern, Limit) ->
|
|
select(S, [{Pattern, [], ['$$']}], Limit).
|
|
|
|
match_cont(S, Pattern, Limit, StartKey) ->
|
|
ContObjs = lists:dropwhile(fun(#obj{key=X}) -> lteq(X, StartKey, S) end, sort(S)),
|
|
match(S#state{objs=ContObjs}, Pattern, Limit).
|
|
|
|
match_delete(#state{objs=L}=S, Pattern) ->
|
|
S#state{objs=L -- match_object(S, Pattern)}.
|
|
|
|
match_object(S, Pattern) ->
|
|
match_object(S, Pattern, undefined).
|
|
|
|
match_object(S, Pattern, Limit) ->
|
|
select(S, [{Pattern, [], ['$_']}], Limit).
|
|
|
|
match_object_cont(S, Pattern, Limit, StartKey) ->
|
|
ContObjs = lists:dropwhile(fun(#obj{key=X}) -> lteq(X, StartKey, S) end, sort(S)),
|
|
match_object(S#state{objs=ContObjs}, Pattern, Limit).
|
|
|
|
match_object_reverse(S, Pattern) ->
|
|
match_object_reverse(S, Pattern, undefined).
|
|
|
|
match_object_reverse(S, Pattern, Limit) ->
|
|
select_reverse(S, [{Pattern, [], ['$_']}], Limit).
|
|
|
|
match_object_reverse_cont(S, Pattern, Limit, StartKey) ->
|
|
ContObjs = lists:dropwhile(fun(#obj{key=X}) -> gteq(X, StartKey, S) end, rsort(S)),
|
|
match_object_reverse(S#state{objs=ContObjs}, Pattern, Limit).
|
|
|
|
select(S, Spec) ->
|
|
select(S, Spec, undefined).
|
|
|
|
select(S, Spec, Limit) ->
|
|
case select1(S, sort(S), Spec) of
|
|
[] ->
|
|
[];
|
|
Match when Limit =:= undefined ->
|
|
Match;
|
|
Match ->
|
|
lists:sublist(Match, Limit)
|
|
end.
|
|
|
|
select_cont(S, Spec, Limit, StartKey) ->
|
|
ContObjs = lists:dropwhile(fun(#obj{key=X}) -> lteq(X, StartKey, S) end, sort(S)),
|
|
select(S#state{objs=ContObjs}, Spec, Limit).
|
|
|
|
select_count(S, Spec) ->
|
|
select1(S, sort(S), Spec).
|
|
|
|
select_delete(#state{objs=L}=S, [{Pattern, [], [true]}]) ->
|
|
S#state{objs=L -- match_object(S, Pattern)}.
|
|
|
|
select_reverse(S, Spec) ->
|
|
select_reverse(S, Spec, undefined).
|
|
|
|
select_reverse(S, Spec, Limit) ->
|
|
case select1(S, rsort(S), Spec) of
|
|
[] ->
|
|
[];
|
|
Match when Limit =:= undefined ->
|
|
Match;
|
|
Match ->
|
|
lists:sublist(Match, Limit)
|
|
end.
|
|
|
|
select_reverse_cont(S, Spec, Limit, StartKey) ->
|
|
ContObjs = lists:dropwhile(fun(#obj{key=X}) -> gteq(X, StartKey, S) end, rsort(S)),
|
|
select_reverse(S#state{objs=ContObjs}, Spec, Limit).
|
|
|
|
select1(#state{impl=ets}=S, L, Spec) ->
|
|
select2(S#state{type=set}, L, Spec);
|
|
select1(S, L, Spec) ->
|
|
select2(S, L, Spec).
|
|
|
|
%% simple and limited select implementation
|
|
select2(S, L, [{Pattern, [], [Result]}]) ->
|
|
case Pattern of
|
|
{'$1', '$2', '$3'} ->
|
|
case Result of
|
|
'$$' ->
|
|
[ [obj, X, Y] || #obj{key=X,val=Y} <- L ];
|
|
'$_' ->
|
|
[ X || X <- L ];
|
|
true ->
|
|
length(L)
|
|
end;
|
|
#obj{key='_', val='$1'} ->
|
|
case Result of
|
|
'$$' ->
|
|
[ [X] || #obj{val=X} <- L ];
|
|
'$_' ->
|
|
[ X || X <- L ];
|
|
true ->
|
|
length(L)
|
|
end;
|
|
#obj{key='$1', val='_'} ->
|
|
case Result of
|
|
'$$' ->
|
|
[ [X] || #obj{key=X} <- L ];
|
|
'$_' ->
|
|
[ X || X <- L ];
|
|
true ->
|
|
length(L)
|
|
end;
|
|
#obj{key=P, val='$1'} ->
|
|
case Result of
|
|
'$$' ->
|
|
[ [X] || #obj{key=Y, val=X} <- L, eq(Y, P, S) ];
|
|
'$_' ->
|
|
[ X || #obj{key=Y}=X <- L, eq(Y, P, S) ];
|
|
true ->
|
|
length([ X || #obj{key=Y}=X <- L, eq(Y, P, S) ])
|
|
end;
|
|
#obj{key='$1', val=P} ->
|
|
case Result of
|
|
'$$' ->
|
|
[ [X] || #obj{key=X, val=Y} <- L, eq(Y, P, S) ];
|
|
'$_' ->
|
|
[ X || #obj{val=Y}=X <- L, eq(Y, P, S) ];
|
|
true ->
|
|
length([ X || #obj{val=Y}=X <- L, eq(Y, P, S) ])
|
|
end
|
|
end.
|
|
|
|
eq(X, Y, #state{type=set, impl=ets}) ->
|
|
X =:= Y;
|
|
eq(X, Y, #state{type=ordered_set, impl=ets}) ->
|
|
X == Y;
|
|
eq(X, Y, #state{type=set}) ->
|
|
term_to_binary(X) == term_to_binary(Y);
|
|
eq(X, Y, #state{type=ordered_set}) ->
|
|
sext:encode(X) == sext:encode(Y).
|
|
|
|
neq(X, Y, #state{type=set, impl=ets}) ->
|
|
X =/= Y;
|
|
neq(X, Y, #state{type=ordered_set, impl=ets}) ->
|
|
X /= Y;
|
|
neq(X, Y, #state{type=set}) ->
|
|
term_to_binary(X) /= term_to_binary(Y);
|
|
neq(X, Y, #state{type=ordered_set}) ->
|
|
sext:encode(X) /= sext:encode(Y).
|
|
|
|
lteq(X, Y, #state{impl=ets}) ->
|
|
X =< Y;
|
|
lteq(X, Y, #state{type=set}) ->
|
|
term_to_binary(X) =< term_to_binary(Y);
|
|
lteq(X, Y, #state{type=ordered_set}) ->
|
|
sext:encode(X) =< sext:encode(Y).
|
|
|
|
gteq(X, Y, #state{impl=ets}) ->
|
|
X >= Y;
|
|
gteq(X, Y, #state{type=set}) ->
|
|
term_to_binary(X) >= term_to_binary(Y);
|
|
gteq(X, Y, #state{type=ordered_set}) ->
|
|
sext:encode(X) >= sext:encode(Y).
|
|
|
|
sort(#state{impl=ets, objs=L}) ->
|
|
lists:sort(L);
|
|
sort(#state{objs=L}) ->
|
|
[ sext:decode(X) || X <- lists:sort([ sext:encode(Y) || Y <- L ]) ].
|
|
|
|
rsort(S) ->
|
|
lists:reverse(sort(S)).
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% Internal - Implementation
|
|
%%%----------------------------------------------------------------------
|
|
|
|
%% @NOTE simplify test model by combining match/3 and match/1 into
|
|
%% single match31/3 command
|
|
|
|
match31(Tab, Pattern, Limit) ->
|
|
catch match31(?IMPL:match(Tab, Pattern, Limit), Pattern, Limit, []).
|
|
|
|
match31('$end_of_table', _Pattern, _Limit, Acc) ->
|
|
Acc;
|
|
match31({Match, Cont}, Pattern, Limit, Acc) when length(Match) =< Limit ->
|
|
match31(?IMPL:match(Cont), Pattern, Limit, Acc ++ Match).
|
|
|
|
%% @NOTE simplify test model by combining match_object/3 and
|
|
%% match_object/1 into single match_object31/3 command
|
|
|
|
match_object31(Tab, Pattern, Limit) ->
|
|
catch match_object31(?IMPL:match_object(Tab, Pattern, Limit), Pattern, Limit, []).
|
|
|
|
match_object31('$end_of_table', _Pattern, _Limit, Acc) ->
|
|
Acc;
|
|
match_object31({Match, Cont}, Pattern, Limit, Acc) when length(Match) =< Limit ->
|
|
match_object31(?IMPL:match_object(Cont), Pattern, Limit, Acc ++ Match).
|
|
|
|
%% @NOTE simplify test model by combining select/3 and select/1 into
|
|
%% single select31/3 command
|
|
|
|
select31(Tab, Spec, Limit) ->
|
|
catch select31(?IMPL:select(Tab, Spec, Limit), Spec, Limit, []).
|
|
|
|
select31('$end_of_table', _Spec, _Limit, Acc) ->
|
|
Acc;
|
|
select31({Match, Cont}, Spec, Limit, Acc) when length(Match) =< Limit ->
|
|
select31(?IMPL:select(Cont), Spec, Limit, Acc ++ Match).
|
|
|
|
%% @NOTE simplify test model by combining select_reverse/3 and
|
|
%% select_reverse/1 into single select_reverse31/3 command
|
|
|
|
select_reverse31(Tab, Spec, Limit) ->
|
|
catch select_reverse31(?IMPL:select_reverse(Tab, Spec, Limit), Spec, Limit, []).
|
|
|
|
select_reverse31('$end_of_table', _Spec, _Limit, Acc) ->
|
|
Acc;
|
|
select_reverse31({Match, Cont}, Spec, Limit, Acc) when length(Match) =< Limit ->
|
|
select_reverse31(?IMPL:select_reverse(Cont), Spec, Limit, Acc ++ Match).
|
|
|
|
|
|
-endif. %% -ifdef(QC).
|