Permalink
Browse files

Cleaned up PropEr statem tests

  • Loading branch information...
1 parent 018c4be commit 67921243af70649f7a9a2ee3f5bf2356a2c8c683 @ferd committed Apr 1, 2012
Showing with 21 additions and 18 deletions.
  1. +0 −1 README.markdown
  2. +21 −17 test/dispcount_prop.erl
View
@@ -198,7 +198,6 @@ The error you see is likely `{start_spec,{invalid_shutdown,infinity}}`. This is
## What's left to do? ##
-- More complete testing suite.
- Adding a function call to allow the transfer of ownership from a process to another one to avoid messing with monitoring in the callback module.
- Testing to make sure the callback modules can be updated with OTP relups and appups. This is so far untested.
- Allowing dynamic resizing of pools.
View
@@ -11,7 +11,7 @@
-define(NAME, prop_dispatch).
-define(INFO, {call, erlang, element, [2,{call, dispcount, dispatcher_info, [?NAME]}]}).
--record(state, {resource=[]}).
+-record(state, {resource=[], last}).
initial_state() ->
#state{}.
@@ -22,36 +22,36 @@ command(#state{resource=R}) ->
[{call, ?MODULE, checkin, [?INFO, hd(R)]} || R =/= []]).
next_state(S=#state{resource=L}, V, {call, _, checkout, _}) ->
- S#state{resource=[V|L]};
+ S#state{resource=[V|L], last=checkout};
next_state(S=#state{resource=[_|L]}, _V, {call, _, checkin, _}) ->
- S#state{resource=L}.
+ S#state{resource=L, last=checkin}.
-%% 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.
+%% when we have a resource checked in or out, we can either try to
+%% check it in or out again
precondition(#state{resource=R}, {call,_,checkin,_}) when R =/= [] -> true;
precondition(#state{resource=R}, {call,_,checkout,_}) when R =/= [] -> true;
+%% Without a resource, we can only check stuff out.
precondition(#state{resource=[]}, {call,_,checkout,_}) -> true;
-precondition(A, B) -> io:format("PRE: ~p~n",[{A,B}]), false.
+precondition(_, _) -> 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;
+%% In case of a fast checkin following checkout on a similar resource might end up busy.
+postcondition(#state{resource=[],last=checkin}, {call, _, checkout, _}, {error,busy}) -> true;
+%% Gotta make sure we didn't manage to checkout the same resource twice
+postcondition(#state{resource=L=[_|_]}, {call, _, checkout, _}, {ok,_Ref,Res}) ->
+ case lists:keyfind(Res,3,L) of
+ false -> true;
+ {ok,_,Res} -> false
+ end;
postcondition(_, _, _) -> false.
prop_nocrash() ->
@@ -68,13 +68,17 @@ prop_nocrash() ->
{?NAME, [Tid]},
[{restart,permanent},{shutdown,4000},
{maxr,10},{maxt,60},{resources,10}]),
- {H,_S,_R} = run_commands(?MODULE, Cmds),
+ {H,S,R} = run_commands(?MODULE, Cmds),
ets:delete(Tid),
?WHENFAIL(io:format("History: ~p~n",[{Cmds,H}]),
- true)
+ aggregate(command_names(Cmds),
+ R =:= ok))
end).
%% Simple wrapper to work around limitations of statem stuff.
+%% busy_checkin is basically a hack to circumvent the idea that the
+%% previous result was a busy thing and we discard it through this function
checkin(_Info, {error,busy}) -> busy_checkin;
+%% unpack & call the right checkin
checkin(Info, {ok, Ref, Res}) -> ?SERVER:checkin(Info, Ref, Res).

0 comments on commit 6792124

Please sign in to comment.