<commit_before><commit_msg>Add a quickcheck test for the lock free queue<commit_after>-module(erl_lfq_eqc).
-compile([export_all]).

-ifdef(TEST).
-ifdef(EQC).
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

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

lfq_eqc_test_() ->
    {timeout, 20,
        fun() ->
                ?assert(eqc:quickcheck(eqc:testing_time(4,
                            erl_lfq_eqc:prop_sequential())))
        end
    }.

-record(state, {
        model = [],
        pid,
        queue
        }).

initial_state() ->
    #state{}.

producer_loop(Q) ->
    receive
        {in, Ref, Pid, Bin} ->
            erl_lfq:in(Q, Bin),
            Pid ! {Ref, ok}
    end,
    producer_loop(Q).

command(S) ->
    oneof(
            [{call, ?MODULE, new, []} || S#state.pid == undefined] ++
            [{call, ?MODULE, in, [S#state.pid, binary()]} || S#state.pid /= undefined] ++
            [{call, ?MODULE, out, [S#state.queue]} || S#state.pid /= undefined]
    ).

new() ->
    {ok, Q} = erl_lfq:new(),
    Pid = spawn_link(?MODULE, producer_loop, [Q]),
    {Q, Pid}.

in(Pid, Bin) ->
    Ref = make_ref(),
    Pid ! {in, Ref, self(), Bin},
    receive
        {Ref, ok} ->
            ok
    end.

out(Queue) ->
    erl_lfq:out(Queue).

invariant(#state{queue=Q, model=M}) when Q /= undefined ->
    QLen = length(M),
    QSize = lists:foldl(fun(E, Acc) ->
                    byte_size(E) + Acc
            end, 0, M),
    case erl_lfq:byte_size(Q) == QSize of
        true ->
            case erl_lfq:len(Q) == QLen of
                true ->
                    true;
                false ->
                    {bad_length, erl_lfq:len(Q), QLen}
            end;
        false ->
            {bad_byte_size, erl_lfq:byte_size(Q), QSize}
    end;
invariant(_) ->
    true.

precondition(_S,{call,_,_,_}) ->
    true.

postcondition(_S,{call,_,new,[]},_R) ->
    true;
postcondition(_S,{call,_,in,[_,_Bin]},_R) ->
    true;
postcondition(S,{call,_,out,[_]},R) ->
    case R of
        {empty, _} ->
            case S#state.model == [] of
                true ->
                    true;
                false ->
                    {unexpected_empty, S#state.model}
            end;
        {{value, Val}, _} ->
            case S#state.model == [] of
                true ->
                    {unexpected_non_empty, Val};
                false ->
                    case Val == hd(S#state.model) of
                        true ->
                            true;
                        false ->
                            {unexpected_value, Val, hd(S#state.model)}
                    end
            end
    end.


next_state(S,V,{call, _, new, []}) ->
    S#state{queue={call, erlang, element, [1, V]}, pid={call, erlang, element, [2, V]}};
next_state(S,_V,{call, _, in, [_, Bin]}) ->
    S#state{model=S#state.model ++ [Bin]};
next_state(S,_V,{call, _, out, [_]}) ->
    case S#state.model == [] of
        true ->
            %% still empty
            S#state{model=[]};
        false ->
            S#state{model=tl(S#state.model)}
    end.

prop_sequential() ->
    ?FORALL(Cmds,commands(?MODULE),
            ?TRAPEXIT(
            aggregate(command_names(Cmds),
                      begin
                    {H,S,Res} = run_commands(?MODULE,Cmds),
                    catch(unlink(S#state.pid)),
                    catch(exit(S#state.pid, kill)),
                    ?WHENFAIL(io:format("History: ~p\nState: ~p\nRes: ~p\n~p\n",
                                        [H,S,Res, zip(Cmds, [Y || {_, Y} <- H])]),
                              Res == ok)
                end))).
-endif.
-endif.

{'fraction_non_alphanumeric': 0.17002724795640328, 'fraction_numerical': 0.0016348773841961854, 'mean_word_length': 1.488813559322034, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 38, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7018110', 'n_tokens_mistral': 1292, 'n_tokens_neox': 1238, 'n_words': 220}