Skip to content

Instantly share code, notes, and snippets.

@jlouis
Created June 15, 2015 15:56
Show Gist options
  • Save jlouis/19e82dc0498de73ec713 to your computer and use it in GitHub Desktop.
Save jlouis/19e82dc0498de73ec713 to your computer and use it in GitHub Desktop.
EQC Cluster example
-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.
-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)).
-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].
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment