%%% 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([commands_setup/1, commands_teardown/1, commands_teardown/2]).

%% @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]).

-record(obj, {key :: integer() | float() | binary(), val :: integer() | float() | binary()}).

-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) ->
    {call,?IMPL,new,[undefined,?TAB,gen_options(new,S)]};
serial_command_gen(_Mod,#state{tab=Tab, type=Type}=S) ->
    %% @TODO insert/3, insert_new/3, delete/3, delete_all_objs/2 write_gen_options
    %% @TODO lookup/3 read_gen_options
    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]
          %% @TODO ++ [{call,?IMPL,delete,[Tab]}]
          ++ [{call,?IMPL,delete,[Tab,gen_key(S)]}]
          ++ [{call,?IMPL,delete_all_objs,[Tab]} || Type == ets]
          ++ [{call,?IMPL,lookup,[Tab,gen_key(S)]}]
          ++ [{call,?IMPL,first,[Tab]}]
          ++ [{call,?IMPL,next,[Tab,gen_key(S)]}]
          %% @TODO info
          ++ [{call,?IMPL,tab2list,[Tab]}]
         ).

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 insert/3, insert_new/3, delete_all_objs/2 write_gen_options
    %% @TODO lookup/3 read_gen_options
    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,delete_all_objs,[Tab]} || Type == ets]
          ++ [{call,?IMPL,lookup,[Tab,gen_key(S)]}]
          ++ [{call,?IMPL,first,[Tab]}]
          ++ [{call,?IMPL,next,[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_objs,[_Tab]}) ->
    S#state{objs=[]};
next_state(S, _V, {call,_,delete_all_objs,[_Tab]}) ->
    S;
next_state(S, _V, {call,_,_,_}) ->
    S.

-spec precondition(#state{}, tuple()) -> boolean().
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,new,[?TAB,Options]}) ->
    L = proplists:get_value(db, Options, []),
    proplists:get_bool(create_if_missing, L) andalso proplists:get_bool(error_if_exists, L);
precondition(#state{tab=undefined, type=undefined, impl=undefined}, {call,_,new,[_Tab,?TAB,Options]}) ->
    L = proplists:get_value(db, Options, []),
    proplists:get_bool(create_if_missing, L) andalso proplists:get_bool(error_if_exists, L);
precondition(#state{tab=Tab}, {call,_,new,[?TAB,_Options]}) when Tab /= undefined ->
    false;
precondition(#state{tab=Tab}, {call,_,new,[_Tab,?TAB,_Options]}) when Tab /= undefined ->
    false;
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_objs,[_Tab]}, Res) ->
    Res =:= true;
postcondition(_S, {call,_,delete_all_objs,[_Tab]}, {'EXIT',{badarg,_}}) ->
    true;
postcondition(S, {call,_,lookup,[_Tab,Key]}, Res) ->
    Res =:= keyfind(Key, 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{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, objs=[]}, {call,_,next,[_Tab, _Key]}, Res) ->
    Res =:= '$end_of_table';
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{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(_S, {call,_,_,_}, _Res) ->
    false.

-spec commands_setup(boolean()) -> {ok, term()}.
commands_setup(_Hard) ->
    ?IMPL:teardown(?TAB),
    {ok, unused}.

-spec commands_teardown(term()) -> ok.
commands_teardown(unused) ->
    ?IMPL:teardown(?TAB),
    ok.

-spec commands_teardown(term(), #state{}) -> ok.
commands_teardown(Ref, _State) ->
    commands_teardown(Ref).


%%%----------------------------------------------------------------------
%%% Internal
%%%----------------------------------------------------------------------

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}, Impl]
        ++ gen_leveldb_options(Op,S);
gen_options(Op,#state{type=Type, impl=nif=Impl}=S) ->
    [Type, public, named_table, {keypos,#obj.key}, Impl]
        ++ gen_leveldb_options(Op,S);
gen_options(_Op,#state{type=Type, impl=ets=Impl}) ->
    [Type, public, named_table, {keypos,#obj.key}, 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,
    ?LET(Options, ulist(gen_db_options()), {db, Options ++ ExistsOptions});
gen_db_options(_Op,_S) ->
    ?LET(Options, ulist(gen_db_options()), {db, Options}).

gen_db_read_options(_Op,_S) ->
    ?LET(Options, ulist(gen_db_read_options()), {db_read, Options}).

gen_db_write_options(_Op,_S) ->
    ?LET(Options, ulist(gen_db_write_options()), {db_write, Options}).

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() ->
    nat().

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))}]).

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).

keyfind(X, #state{objs=L}=S) ->
    lists:filter(fun(#obj{key=K}) -> eq(X, K, S) end, L).

keymember(X, S) ->
    [] /= keyfind(X, S).

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).

sort(#state{impl=ets, objs=L}) ->
    lists:sort(L);
sort(#state{objs=L}) ->
    [ sext:decode(X) || X <- lists:sort([ sext:encode(Y) || Y <- L ]) ].

-endif. %% -ifdef(QC).