hashmap_eqc.erl

-module(hashmap_eqc).

%% include some quickcheck headers
-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

%% include the eqc-c generated header
-include("hashmap.hrl").

%% function to initialize the model state
-export([initial_state/0]).

%% command functions

-export([hashmap_create_pre/1,
         hashmap_create_args/1,
         hashmap_create/1,
         hashmap_create_next/3]).

%% the property
-export([prop_correct/0]).


-record(state, {hashmap=undefined,
                size,
                map=[]}).

prop_correct() ->
    %% call setup() if we don't have the 'hashmap' module loaded
    case code:which(hashmap) of
        non_existing ->
            setup();
        _ ->
            ok
    end,
    ?FORALL(Cmds,
            noshrink(commands(?MODULE)),
            begin
                Env = [],
                %% run the commands
                {H, S, Res} = run_commands(?MODULE, Cmds, Env),
                case S#state.hashmap of
                    undefined ->
                        %% we didn't actually generate anything, so nothing to cleanup
                        ok;
                    HM ->
                        %% cleanup the hashmap
                        hashmap:hashmap_free(HM),
                        eqc_c:free(HM)
                end,
                %% print out how many times we ran each command as a percentage
                pretty_commands(?MODULE, Cmds, {H, S, Res},
                                aggregate(command_names(Cmds),
                                          eqc:equals(Res, ok)))
            end).

setup() ->
    %% compile and load the C code as an erlang module
    eqc_c:start(hashmap, [{c_src, "hashmap.c"}, {cppflags, "-I ../../include/ -std=c99"},{cflags,"-lm"}, {additional_files, ["iterator.c"]}]).

-spec initial_state() -> eqc_statem:symbolic_state().
initial_state() ->
    #state{}.

%% commands

hashmap_create_pre(S) ->
    S#state.hashmap == undefined.

hashmap_create_args(_S) ->
    [eqc_gen:choose(4,10)].

hashmap_create(Size) ->
    HM = eqc_c:alloc({struct, hashmap_t}),
    hashmap:hashmap_create(HM, Size),
    HM.

hashmap_create_next(S, R, [_Size]) ->
    S#state{hashmap=R}.