EQC Cluster example

client_eqc.erl

-module(client_eqc).
-compile(export_all).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").

api_spec() ->
    #api_spec {
      language = erlang,
      modules = [
        #api_module {
          name = xmaps,
          functions = [
            #api_fun { name = new, arity = 0, classify = xmaps_eqc},
            #api_fun { name = get, arity = 2, classify = xmaps_eqc},
            #api_fun { name = put, arity = 3, classify = xmaps_eqc}
        ]} ]}.

-record(state, {
	init = false
}).

initial_state() -> #state{}.

new() -> {x, xmaps:new()}.
	
new_pre(S) -> not initialized(S).

new_args(_S) -> [].

new_callouts(_S, []) ->
	?CALLOUT(xmaps, new, [], 'MAP'),
	?RET({x, 'MAP'}).

new_next(S, _, _) -> S#state { init = true }.

%% Use a common postcondition for all commands, so we can utilize the valid return
%% of each command.
postcondition_common(S, Call, Res) ->
    eq(Res, return_value(S, Call)).

%% Main property, just verify that the commands are in sync with reality.
prop_component_correct() ->
    ?SETUP(fun() ->
        eqc_mocking:start_mocking(api_spec()),
        fun() -> ok end
    end,
    ?FORALL(Cmds, commands(?MODULE),
      begin
        {H,S,R} = run_commands(?MODULE, Cmds),
        pretty_commands(?MODULE, Cmds, {H,S,R},
            aggregate(with_title('Commands'), command_names(Cmds),
            aggregate(with_title('Features'), eqc_statem:call_features(H),
            features(eqc_statem:call_features(H),
                R == ok))))
      end)).

%% Helper for showing states of the output:
t() -> t(5).

t(Secs) ->
    eqc:quickcheck(eqc:testing_time(Secs, eqc_statem:show_states(prop_component_correct()))).

initialized(#state { init = I }) -> I.

cluster.erl

-module(cluster).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_cluster.hrl").
-compile(export_all).

components() -> [
	xmaps_eqc, client_eqc
].

api_spec() -> api_spec(?MODULE).

prop_cluster_correct() ->
    ?SETUP(fun() ->
        eqc_mocking:start_mocking(api_spec()),
        fun() -> ok end
    end,
    ?FORALL(Cmds, eqc_cluster:commands(?MODULE),
      begin
        {H,S,R} = run_commands(?MODULE, Cmds),
        pretty_commands(?MODULE, Cmds, {H,S,R},
          aggregate(command_names(Cmds),
            R == ok))
      end)).
    
t() -> t(15).

t(Secs) ->
    eqc:quickcheck(eqc:testing_time(Secs, eqc_statem:show_states(prop_cluster_correct()))).

cmds() ->
    eqc_gen:sample(eqc_cluster:commands(?MODULE)).

xmaps_eqc.erl

-module(xmaps_eqc).
-compile(export_all).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_component.hrl").

api_spec() ->
    #api_spec {
      language = erlang,
      modules = []}.

-record(state, {
	initialized = false,
	m :: maps:map(integer(), integer()),
	contents = [] :: list({integer(), integer()})
}).

initial_state() -> #state{}.

ensure_started_pre(S) -> initialized(S).

new() ->maps:new().
	
new_pre(S) -> not initialized(S).
new_args(_S) -> [].

new_return(#state { contents = Contents }, _R) ->
    maps:from_list(Contents).

new_next(S, Res, _) -> S#state { m = Res, initialized = true }.

new_callers() -> [client_eqc].

put(K, V, Map) -> maps:put(K, V, Map).
put_pre(S) -> initialized(S).
put_args(#state { m = Map }) -> [int(), int(), Map].

put_next(#state { contents = Contents } = S, Res, [K, V, _]) ->
    S#state { contents = lists:keystore(K,1,Contents, {K, V}), m = Res }.
    
put_return(#state { contents = Contents }, [K, V, _M]) ->
    maps:from_list(lists:keystore(K, 1, Contents, {K, V})).

get(K, M) -> maps:get(K, M).
get_pre(S) -> initialized(S) andalso has_pairs(S).
get_args(#state { m = Map } = S) -> [elements(keys(S)), Map].
get_return(#state { contents = Cs }, [K, _]) ->
    {_, V} = lists:keyfind(K, 1, Cs),
    V.

%% Property
%% ----------------------------------

%% Use a common postcondition for all commands, so we can utilize the valid return
%% of each command.
postcondition_common(S, Call, Res) ->
    eq(Res, return_value(S, Call)).

%% Main property, just verify that the commands are in sync with reality.
prop_component_correct() ->
    ?SETUP(fun() ->
        eqc_mocking:start_mocking(api_spec()),
        fun() -> ok end
    end,
    ?FORALL(Cmds, commands(?MODULE),
      begin
        {H,S,R} = run_commands(?MODULE, Cmds),
        pretty_commands(?MODULE, Cmds, {H,S,R},
            aggregate(with_title('Commands'), command_names(Cmds),
            aggregate(with_title('Features'), eqc_statem:call_features(H),
            features(eqc_statem:call_features(H),
                R == ok))))
      end)).

%% Helper for showing states of the output:
t() -> t(5).

t(Secs) ->
    eqc:quickcheck(eqc:testing_time(Secs, eqc_statem:show_states(prop_component_correct()))).

%% ----------------------------------
initialized(#state { initialized = I }) -> I.
has_pairs(#state { contents = Contents }) -> Contents /= [].
keys(#state { contents = Cs }) -> [K || {K, _} <- Cs].