%%% 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}) ->
    oneof([{call,?IMPL,reopen,[]}
           %% @TODO {call,?IMPL,destroy,[]},
           %% @TODO {call,?IMPL,repair,[]}
          ]);
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=undefined, exists=true}=S, V, {call,_,destroy,[]}) ->
    S#state{db=V, exists=false, objs=[]};
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{exists=false}, {call,_,destroy,[]}) ->
    false;
precondition(#state{exists=false}, {call,_,repair,[]}) ->
    false;
precondition(#state{db=Db}, {call,_,open,[]}) when Db /= undefined->
    false;
precondition(#state{db=Db}, {call,_,reopen,[]}) when Db /= undefined->
    false;
precondition(#state{db=Db}, {call,_,destroy,[]}) when Db /= undefined->
    false;
precondition(#state{db=Db}, {call,_,repair,[]}) 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{exists=true}, {call,_,destroy,[]}, Res) ->
    Res;
postcondition(#state{exists=true}, {call,_,repair,[]}, Res) ->
    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).