Permalink
Browse files

Basic statem property-based tests added

These tests are for now incomplete but provide a base
on which to build a more complete suite to make sure
dispcount is hopefully rock-solid.
  • Loading branch information...
ferd committed Apr 1, 2012
1 parent bb96186 commit d3379f11902dfa5fa9a674394ed91c31efdf2e43
Showing with 138 additions and 1 deletion.
  1. +1 −0 .gitignore
  2. +24 −0 Makefile
  3. +4 −1 rebar.config
  4. +80 −0 test/dispcount_prop.erl
  5. +29 −0 test/prop_dispatch.erl
View
@@ -4,3 +4,4 @@
*.COVER.*
logs/*
ebin/*
+deps/*
View
@@ -0,0 +1,24 @@
+REBAR=./rebar
+
+all:
+ @$(REBAR) get-deps compile
+
+get-deps:
+ @$(REBAR) get-deps
+
+edoc:
+ @$(REBAR) doc
+
+test:
+ @rm -rf .eunit
+ @mkdir -p .eunit
+ @$(REBAR) skip_deps=true eunit
+
+clean:
+ @rm -rf deps/ ebin/ logs/
+
+build_plt:
+ @$(REBAR) build-plt
+
+dialyzer:
+ @$(REBAR) dialyze
View
@@ -28,4 +28,7 @@
%% name as an atom, eg. mochiweb, a name and a version (from the .app file), or
%% an application name, a version and the SCM details on how to fetch it (SCM
%% type, location and revision). Rebar currently supports git, hg, bzr and svn.
-{deps, []}.
+{deps, [
+ {proper, "1.0", {git, "https://github.com/manopapad/proper.git", "master"}},
+ {meck, "0.7.1", {git, "https://github.com/eproxus/meck.git", "master"}}
+]}.
View
@@ -0,0 +1,80 @@
+%%% Basic sequential statem based tests for dispcount.
+-module(dispcount_prop).
+-include_lib("proper/include/proper.hrl").
+-behaviour(proper_statem).
+
+-export([command/1, initial_state/0, next_state/3, postcondition/3,
+ precondition/2]).
+-export([checkin/2]).
+
+-define(SERVER, dispcount).
+-define(NAME, prop_dispatch).
+-define(INFO, {call, erlang, element, [2,{call, dispcount, dispatcher_info, [?NAME]}]}).
+
+-record(state, {resource=[]}).
+
+initial_state() ->
+ #state{}.
+
+%% Checking in and checking out is always valid
+command(#state{resource=R}) ->
+ oneof([{call, ?SERVER, checkout, [?INFO]}] ++
+ [{call, ?MODULE, checkin, [?INFO, hd(R)]} || R =/= []]).
+
+next_state(S=#state{resource=L}, V, {call, _, checkout, _}) ->
+ S#state{resource=[V|L]};
+next_state(S=#state{resource=[_|L]}, _V, {call, _, checkin, _}) ->
+ S#state{resource=L}.
+
+%% These preconditions might need a little rework. They were added
+%% when the tests only worked with one resource, but since then, the
+%% rules about empty lists no longer holds with 10 resources. The
+%% tests still pass, but this should be cleaned up.
+precondition(#state{resource=R}, {call,_,checkin,_}) when R =/= [] -> true;
+precondition(#state{resource=R}, {call,_,checkout,_}) when R =/= [] -> true;
+precondition(#state{resource=[]}, {call,_,checkout,_}) -> true;
+precondition(A, B) -> io:format("PRE: ~p~n",[{A,B}]), false.
+
+%% The postconditions are a little bit more complex.
+%% The following rules are for resources that we managed to check out.
+postcondition(#state{resource=[{ok,_Ref,_Res}|_]}, {call, _, checkin, _}, ok) -> true;
+postcondition(#state{resource=[{ok,_Ref,_Res}|_]}, {call, _, checkout, _}, {error,busy}) -> true;
+postcondition(#state{resource=L}, {call, _, checkout, _}, {ok,_Ref,Res}) ->
+ %% Gotta make sure we didn't manage to checkout the same resource twice
+ case lists:keyfind(Res,3,L) of
+ false -> true;
+ {ok,_,Res} -> false
+ end;
+%% These postconditions check for what happens when we were busy beforehand
+%% This state pretty much allows anything to go
+postcondition(#state{resource=[{error,busy}|_]}, {call, _, checkout, _}, {error,busy}) -> true;
+postcondition(#state{resource=[{error,busy}|_]}, {call, _, checkout, _}, {ok,_Ref,_Res}) -> true;
+postcondition(#state{resource=[{error,busy}|_]}, {call, _, checkin, _}, busy_checkin) -> true;
+%% Checking out is always fine when we had no resource checked out beforehand
+postcondition(#state{resource=[]}, {call, _, checkout, _}, {ok,_Ref,_Res}) -> true;
+postcondition(_, _, _) -> false.
+
+prop_nocrash() ->
+ ?FORALL(Cmds, commands(?MODULE, #state{}),
+ begin
+ %% the ETS table works with the dispcount dispatcher
+ %% in this test to assign increasing IDs to each dispatch_watcher
+ %% instance.
+ Tid = ets:new(ids, [public,set]),
+ ets:insert(Tid, {id,0}),
+ application:stop(dispcount),
+ application:start(dispcount),
+ ok = ?SERVER:start_dispatch(?NAME,
+ {?NAME, [Tid]},
+ [{restart,permanent},{shutdown,4000},
+ {maxr,10},{maxt,60},{resources,10}]),
+ {H,_S,_R} = run_commands(?MODULE, Cmds),
+ ets:delete(Tid),
+ ?WHENFAIL(io:format("History: ~p~n",[{Cmds,H}]),
+ true)
+ end).
+
+%% Simple wrapper to work around limitations of statem stuff.
+checkin(_Info, {error,busy}) -> busy_checkin;
+checkin(Info, {ok, Ref, Res}) -> ?SERVER:checkin(Info, Ref, Res).
+
View
@@ -0,0 +1,29 @@
+-module(prop_dispatch).
+-behaviour(dispcount).
+-export([init/1, checkout/2, checkin/2, handle_info/2, dead/1,
+ terminate/2, code_change/3]).
+
+init([Tid]) ->
+ Id = ets:update_counter(Tid, id, 1),
+ {ok, Id}.
+
+checkout(_From, Id) ->
+ {ok, Id, Id}.
+
+checkin(Id, undefined) ->
+ {ok, Id};
+checkin(_SomeId, Id) ->
+ {ignore, Id}.
+
+dead(Id) ->
+ {ok, Id}.
+
+handle_info(_Msg, State) ->
+ {ok, State}.
+
+terminate(_Reason, _State) ->
+ ok.
+
+code_change(_OldVsn, State, _Extra) ->
+ {ok, State}.
+

0 comments on commit d3379f1

Please sign in to comment.