% Licensed under the Apache License, Version 2.0 (the "License"); you may not
% use this file except in compliance with the License. You may obtain a copy of
% the License at
%
%   http://www.apache.org/licenses/LICENSE-2.0
%
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
% WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
% License for the specific language governing permissions and limitations under
% the License.

-module(ioq_kv_tests).
-ifdef(WITH_PROPER).
-behaviour(proper_statem).

-include_lib("proper/include/proper.hrl").
-include_lib("eunit/include/eunit.hrl").


-export([
    initial_state/0,
    command/1,
    precondition/2,
    postcondition/3,
    next_state/3,
    random_key/1
]).

-record(st, {kvs}).

proper_test_() ->
    PropErOpts = [
        {to_file, user},
        {max_size, 5},
        {numtests, 1000}
    ],
    {timeout, 3600, ?_assertEqual([], proper:module(?MODULE, PropErOpts))}.


prop_ioq_kvs_almost_any() ->
    ?FORALL({K, V}, kvs(), begin
        case (catch ioq_kv:put(K, V)) of
            ok -> ioq_kv:get(K) == V;
            {'EXIT', {invalid_term, _}} -> true;
            _ -> false
        end
    end).


prop_ioq_kvs() ->
    ?FORALL(Cmds, commands(?MODULE),
        begin
            cleanup(),
            {H, S, R} = run_commands(?MODULE, Cmds),
            ?WHENFAIL(
                io:format("History: ~p\nState: ~p\nRes: ~p\n", [H,S,R]),
                R =:= ok
            )
        end
    ).

initial_state() ->
    #st{kvs=dict:new()}.


command(S) ->
    Key = {call, ioq_kv_tests, random_key, [S]},
    frequency([
        {1, {call, ioq_kv, init, []}},
        {9, {call, ioq_kv, get, [Key]}},
        {1, {call, ioq_kv, get, [key()]}},
        {9, {call, ioq_kv, put, [Key, val()]}},
        {1, {call, ioq_kv, put, [key(), val()]}},
        {2, {call, ioq_kv, delete, [Key]}},
        {1, {call, ioq_kv, delete, [key()]}}
    ]).


precondition(_, _) ->
    true.


postcondition(_S, {call, _, init, []}, ok) ->
    true;
postcondition(S, {call, _, get, [Key]}, Val) ->
    case dict:is_key(Key, S#st.kvs) of
        true ->
            case dict:find(Key, S#st.kvs) of
                {ok, Val} -> true;
                _ -> false
            end;
        false ->
            case Val of
                undefined -> true;
                _ -> false
            end
    end;
postcondition(_S, {call, _, put, [_Key, _Val]}, ok) ->
    true;
postcondition(_S, {call, _, delete, [_Key]}, ok) ->
    true;
postcondition(_S, _, _) ->
    false.


next_state(S, _V, {call, _, init, []}) ->
    S;
next_state(S, _V, {call, _, get, [_Key]}) ->
    S;
next_state(S, _V, {call, _, put, [Key, Val]}) ->
    S#st{
        kvs={call, dict, store, [Key, Val, S#st.kvs]}
    };
next_state(S, _V, {call, _, delete, [Key]}) ->
    S#st{
        kvs={call, dict, erase, [Key, S#st.kvs]}
    }.


random_key(#st{kvs=KVs}) ->
    Keys0 = dict:fetch_keys(KVs),
    Keys = lists:append(Keys0, [foo]),
    NumKeys = erlang:length(Keys),
    KeyPos = random:uniform(NumKeys),
    lists:nth(KeyPos, Keys).

cleanup() ->
    code:purge(ioq_kv_dyn),
    code:delete(ioq_kv_dyn).


% Generators

key() -> almost_any().
val() -> almost_any().
kvs() -> {any(), any()}.

% ioq_kv can't handle storing bitstrings that don't have
% a length divisible by 8. Instead of being clever I
% just define an almost any.
almost_any() ->
    oneof([
        integer(),
        float(),
        atom(),
        binary(),
        ?LAZY(loose_tuple(almost_any())),
        ?LAZY(list(almost_any()))
    ]).
-endif.