237 lines
7.1 KiB
Erlang
237 lines
7.1 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_statemc_lets).
|
|
|
|
-ifdef(QC).
|
|
-ifdef(EQC).
|
|
|
|
%% 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([commands_setup/1, commands_teardown/1, commands_teardown/2]).
|
|
|
|
%% @NOTE For boilerplate exports, see "qc_statem.hrl"
|
|
-include_lib("eqc/include/eqc_c.hrl").
|
|
-include_lib("qc/include/qc_statem.hrl").
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% defines, types, records
|
|
%%%----------------------------------------------------------------------
|
|
|
|
-define(IMPL, qc_leveldb).
|
|
|
|
-record(obj, {key :: binary(), val :: binary()}).
|
|
|
|
-type obj() :: #obj{}.
|
|
|
|
-record(state, {
|
|
parallel=false :: boolean(),
|
|
exists=false :: boolean(),
|
|
db=undefined :: undefined | term(),
|
|
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{db=undefined, exists=false}) ->
|
|
{call,?IMPL,open,[]};
|
|
serial_command_gen(_Mod,#state{db=undefined, exists=true}) ->
|
|
{call,?IMPL,reopen,[]};
|
|
serial_command_gen(_Mod,#state{db=Db}=S) ->
|
|
oneof([{call,?IMPL,close,[Db]},
|
|
{call,?IMPL,put,[Db,gen_obj(S)]},
|
|
{call,?IMPL,delete,[Db,gen_key(S)]},
|
|
{call,?IMPL,get,[Db,gen_key(S)]},
|
|
{call,?IMPL,first,[Db]},
|
|
{call,?IMPL,last,[Db]},
|
|
{call,?IMPL,next,[Db,gen_key(S)]}
|
|
]).
|
|
|
|
parallel_command_gen(_Mod,#state{db=undefined}) ->
|
|
{call,?IMPL,open,[]};
|
|
parallel_command_gen(_Mod,#state{db=Db}=S) ->
|
|
oneof([{call,?IMPL,put,[Db,gen_obj(S)]},
|
|
{call,?IMPL,delete,[Db,gen_key(S)]},
|
|
{call,?IMPL,get,[Db,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{db=undefined, exists=false}=S, V, {call,_,open,[]}) ->
|
|
S#state{db=V, exists=true};
|
|
next_state(#state{db=undefined, exists=true}=S, V, {call,_,reopen,[]}) ->
|
|
S#state{db=V, exists=true};
|
|
next_state(#state{db=Db}=S, _V, {call,_,close,[Db]}) when Db /= undefined ->
|
|
S#state{db=undefined};
|
|
next_state(S, _V, {call,_,put,[_Db,Obj]}) ->
|
|
insert_obj(S, Obj);
|
|
next_state(S, _V, {call,_,delete,[_Db,Key]}) ->
|
|
delete_obj(S, Key);
|
|
next_state(S, _V, {call,_,_,_}) ->
|
|
S.
|
|
|
|
-spec precondition(#state{}, tuple()) -> boolean().
|
|
precondition(#state{exists=true}, {call,_,open,[]}) ->
|
|
false;
|
|
precondition(#state{exists=false}, {call,_,reopen,[]}) ->
|
|
false;
|
|
precondition(#state{db=Db}, {call,_,open,[]}) when Db /= undefined->
|
|
false;
|
|
precondition(#state{db=Db}, {call,_,reopen,[]}) when Db /= undefined->
|
|
false;
|
|
precondition(_S, {call,_,_,_}) ->
|
|
true.
|
|
|
|
-spec postcondition(#state{}, tuple(), term()) -> boolean().
|
|
postcondition(#state{exists=false}, {call,_,open,[]}, Res) ->
|
|
?IMPL:is_db(Res);
|
|
postcondition(#state{exists=true}, {call,_,reopen,[]}, Res) ->
|
|
?IMPL:is_db(Res);
|
|
postcondition(#state{db=Db}, {call,_,close,[_Db]}, Res) ->
|
|
Res andalso Db /= undefined;
|
|
postcondition(_S, {call,_,put,[_Db,_]}, Res) ->
|
|
Res;
|
|
postcondition(_S, {call,_,delete,[_Db,_]}, Res) ->
|
|
Res;
|
|
postcondition(S, {call,_,get,[_Db,Key]}, Res) ->
|
|
Res =:= get_val(S, Key);
|
|
postcondition(#state{objs=[]}, {call,_,first,[_Db]}, Res) ->
|
|
Res;
|
|
postcondition(S, {call,_,first,[_Db]}, Res) ->
|
|
#obj{key=K} = hd(sort_objs(S)),
|
|
Res =:= K;
|
|
postcondition(#state{objs=[]}, {call,_,last,[_Db]}, Res) ->
|
|
Res;
|
|
postcondition(S, {call,_,last,[_Db]}, Res) ->
|
|
#obj{key=K} = hd(lists:reverse(sort_objs(S))),
|
|
Res =:= K;
|
|
postcondition(S, {call,_,next,[_Db,Key]}, Res) ->
|
|
case lists:dropwhile(fun(#obj{key=X}) -> X =< Key end, sort_objs(S)) of
|
|
[] ->
|
|
Res;
|
|
[#obj{key=K}|_] ->
|
|
Res =:= K
|
|
end;
|
|
postcondition(_S, {call,_,_,_}, _Res) ->
|
|
false.
|
|
|
|
-spec commands_setup(boolean()) -> {ok, term()}.
|
|
commands_setup(_Hard) ->
|
|
?IMPL:setup(),
|
|
teardown(),
|
|
{ok, unused}.
|
|
|
|
-spec commands_teardown(term()) -> ok.
|
|
commands_teardown(unused) ->
|
|
teardown(),
|
|
ok.
|
|
|
|
-spec commands_teardown(term(), #state{}) -> ok.
|
|
commands_teardown(Ref, _State) ->
|
|
commands_teardown(Ref).
|
|
|
|
|
|
%%%----------------------------------------------------------------------
|
|
%%% Internal
|
|
%%%----------------------------------------------------------------------
|
|
|
|
teardown() ->
|
|
?IMPL:teardown().
|
|
|
|
gen_bytes() ->
|
|
?LET(B, list(choose(0,127)), list_to_binary(B)).
|
|
|
|
gen_key() ->
|
|
gen_bytes().
|
|
|
|
gen_val() ->
|
|
gen_bytes().
|
|
|
|
gen_obj() ->
|
|
#obj{key=gen_key(), val=gen_val()}.
|
|
|
|
gen_key(#state{objs=[]}) ->
|
|
gen_key();
|
|
gen_key(#state{objs=Objs}) ->
|
|
oneof([?LET(Obj, oneof(Objs), Obj#obj.key), gen_key()]).
|
|
|
|
gen_obj(#state{objs=[]}) ->
|
|
gen_obj();
|
|
gen_obj(#state{objs=Objs}) ->
|
|
oneof([oneof(Objs), gen_obj()]).
|
|
|
|
insert_obj(S, #obj{key=K}=Obj) ->
|
|
case keymember(K, S) of
|
|
false ->
|
|
S#state{objs=[Obj|S#state.objs]};
|
|
true ->
|
|
S#state{objs=keyreplace(K, Obj, S)}
|
|
end.
|
|
|
|
delete_obj(S, K) ->
|
|
S#state{objs=keydelete(K, S)}.
|
|
|
|
get_val(S, K) ->
|
|
case keyfind(K, S) of
|
|
[] ->
|
|
true;
|
|
[#obj{val=Val}] ->
|
|
Val
|
|
end.
|
|
|
|
sort_objs(#state{objs=Objs}) ->
|
|
lists:sort(Objs).
|
|
|
|
keydelete(X, #state{objs=L}) ->
|
|
lists:filter(fun(#obj{key=K}) -> K =/= X end, L).
|
|
|
|
keyreplace(X, Y, #state{objs=L}) ->
|
|
lists:map(fun(Z=#obj{key=K}) -> case K =:= X of true -> Y; false -> Z end end, L).
|
|
|
|
keyfind(X, #state{objs=L}) ->
|
|
lists:filter(fun(#obj{key=K}) -> K =:= X end, L).
|
|
|
|
keymember(X, S) ->
|
|
[] /= keyfind(X, S).
|
|
|
|
-endif. %% -ifdef(EQC).
|
|
-endif. %% -ifdef(QC).
|