Crash test for proper-testing#224

test/parallel_crash_tests.erl

@@ -0,0 +1,123 @@
+-module(parallel_crash_tests).
+
+-include_lib("proper/include/proper.hrl").
+
+-include_lib("eunit/include/eunit.hrl").
+
+
+%%------------------------------------------------------------------------------
+%% Helper macros
+%%------------------------------------------------------------------------------
+
+%% NOTE: Never add long_result to Opts for these macros.
+
+state_is_clean() ->
+    get() =:= [].
+
+assertEqualsOneOf(_X, none) ->
+    ok;
+assertEqualsOneOf(X, List) ->
+    ?assert(lists:any(fun(Y) -> Y =:= X end, List)).
+
+-define(_passes(Test),
+	?_passes(Test, [])).
+
+-define(_passes(Test, Opts),
+	?_assertRun(true, Test, Opts, true)).
+
+-define(_errorsOut(ExpReason, Test),
+	?_errorsOut(ExpReason, Test, [])).
+
+-define(_errorsOut(ExpReason, Test, Opts),
+	?_assertRun({error,ExpReason}, Test, Opts, true)).
+
+-define(_assertRun(ExpResult, Test, Opts, AlsoLongResult),
+	?_test(begin
+	    ?assertMatch(ExpResult, proper:quickcheck(Test,Opts)),
+	    proper:clean_garbage(),
+	    ?assert(state_is_clean()),
+	    case AlsoLongResult of
+		true ->
+		    ?assertMatch(ExpResult,
+				 proper:quickcheck(Test,[long_result|Opts])),
+		    proper:clean_garbage(),
+		    ?assert(state_is_clean());
+		false ->
+		    ok
+	    end
+	end)).
+
+-define(_assertCheck(ExpShortResult, CExm, Test),
+	?_assertCheck(ExpShortResult, CExm, Test, [])).
+
+-define(_assertCheck(ExpShortResult, CExm, Test, Opts),
+	?_test(?assertCheck(ExpShortResult, CExm, Test, Opts))).
+
+-define(assertCheck(ExpShortResult, CExm, Test, Opts),
+	begin
+	    ?assertMatch(ExpShortResult, proper:check(Test,CExm,Opts)),
+	    ?assert(state_is_clean())
+	end).
+
+-define(_fails(Test),
+	?_fails(Test, [])).
+
+-define(_fails(Test, Opts),
+	?_failsWith(_, Test, Opts)).
+
+-define(_failsWith(ExpCExm, Test),
+	?_failsWith(ExpCExm, Test, [])).
+
+-define(_failsWith(ExpCExm, Test, Opts),
+	?_assertFailRun(ExpCExm, none, Test, Opts)).
+
+-define(_failsWithOneOf(AllCExms, Test),
+	?_failsWithOneOf(AllCExms, Test, [])).
+
+-define(_failsWithOneOf(AllCExms, Test, Opts),
+	?_assertFailRun(_, AllCExms, Test, Opts)).
+
+-define(SHRINK_TEST_OPTS, [{start_size,10},{max_shrinks,10000}]).
+
+-define(_shrinksTo(ExpShrunk, Type),
+	?_assertFailRun([ExpShrunk], none, ?FORALL(_X,Type,false),
+			?SHRINK_TEST_OPTS)).
+
+-define(_shrinksToOneOf(AllShrunk, Type),
+	?_assertFailRun(_, [[X] || X <- AllShrunk], ?FORALL(_X,Type,false),
+			?SHRINK_TEST_OPTS)).
+
+-define(_nativeShrinksTo(ExpShrunk, TypeStr),
+	?_assertFailRun([ExpShrunk], none,
+			?FORALL(_X,assert_can_translate(?MODULE,TypeStr),false),
+			?SHRINK_TEST_OPTS)).
+
+-define(_nativeShrinksToOneOf(AllShrunk, TypeStr),
+	?_assertFailRun(_, [[X] || X <- AllShrunk],
+			?FORALL(_X,assert_can_translate(?MODULE,TypeStr),false),
+			?SHRINK_TEST_OPTS)).
+
+-define(_assertFailRun(ExpCExm, AllCExms, Test, Opts),
+	?_test(begin
+		   ShortResult = proper:quickcheck(Test, Opts),
+		   CExm1 = get_cexm(),
+		   ?checkCExm(CExm1, ExpCExm, AllCExms, Test, Opts),
+		   ?assertEqual(false, ShortResult),
+		   LongResult = proper:quickcheck(Test, [long_result|Opts]),
+		   CExm2 = get_cexm(),
+		   ?checkCExm(CExm2, ExpCExm, AllCExms, Test, Opts),
+		   ?checkCExm(LongResult, ExpCExm, AllCExms, Test, Opts)
+	       end)).
+
+
+simple_test_() ->
+    [
+     ?_passes(symb_statem:prop_simple())
+    ].
+
+
+parallel_simple_test_() ->
+    [
+     %% {timeout, 20, ?_passes(symb_statem:prop_parallel_simple())}
+     ?_passes(symb_statem:prop_parallel_simple())
+    ].

test/symb_statem.erl

@@ -28,62 +28,81 @@
 -module(symb_statem).
 
 -export([command/1,
-	 initial_state/0, next_state/3,
-	 precondition/2, postcondition/3]).
--export([foo/1, bar/1]).
+         initial_state/0, next_state/3,
+         precondition/2, postcondition/3]).
+-export([foo/1, bar/1, croak/0]).
 -export([prop_simple/0, prop_parallel_simple/0]).
 
 -include_lib("proper/include/proper.hrl").
 
 -record(state, {foo = [] :: list(),
-		bar = [] :: list()}).
+                bar = [] :: list()
+               }).
 -type state() :: #state{}.
 
 -spec initial_state() -> state().
 initial_state() ->
-    #state{}.
+  #state{}.
 
 command(_S) ->
-    oneof([{call,?MODULE,foo,[integer()]},
-	   {call,?MODULE,bar,[integer()]}]).
+  oneof([{call,?MODULE,foo,[integer()]},
+         {call,?MODULE,croak,[]},
+         {call,?MODULE,bar,[integer()]}]).
 
 precondition(_, _) ->
-    true.
+  true.
 
+next_state(S, _V, {call,_,croak,[]}) ->
+  S;
 next_state(S = #state{foo=Foo}, V, {call,_,foo,[_Arg]}) ->
-    V1 = {call,erlang,element,[1,V]},
-    S#state{foo = [V1|Foo]};
+  V1 = {call,erlang,element,[1,V]},
+  S#state{foo = [V1|Foo]};
 next_state(S = #state{bar=Bar}, V, {call,_,bar,[_Arg]}) ->
-    V1 = {call,erlang,hd,[V]},
-    S#state{bar = [V1|Bar]}.
+  V1 = {call,erlang,hd,[V]},
+  S#state{bar = [V1|Bar]}.
 
 postcondition(S, {call,_,foo,[_Arg]}, Res) when is_tuple(Res) ->
-    lists:all(fun is_integer/1, S#state.foo);
+  lists:all(fun is_integer/1, S#state.foo);
 postcondition(S, {call,_,bar,[_Arg]}, Res) when is_list(Res) ->
-    lists:all(fun is_integer/1, S#state.bar);
+  lists:all(fun is_integer/1, S#state.bar);
+postcondition(_, {call,_,croak,[]}, _) ->
+  true;
 postcondition(_, _, _) ->
-    false.
+  false.
 
 foo(I) when is_integer(I) ->
-    erlang:make_tuple(3, I).
+  io:format(user, "foo\n", []),
+  erlang:make_tuple(3, I).
 
 bar(I) when is_integer(I) ->
-    lists:duplicate(3, I).
+  lists:duplicate(3, I).
+
+croak() ->
+  io:format(user, "croaking now\n", []),
+  1/0.
 
 prop_simple() ->
-    ?FORALL(Cmds, commands(?MODULE),
-	    begin
-		{H,S,Res} = run_commands(?MODULE, Cmds),
-		?WHENFAIL(
-		   io:format("H: ~w\nState: ~w\n:Res: ~w\n", [H,S,Res]),
-		   Res =:= ok)
-	    end).
+  ?FORALL(Cmds, commands(?MODULE),
+          begin
+            {H,S,Res} = run_commands(?MODULE, Cmds),
+            ?WHENFAIL(
+               io:format("H: ~w\nState: ~w\n:Res: ~w\n", [H,S,Res]),
+               Res =:= ok)
+          end).
+
+croaking_commands() ->
+  exactly({
+           [{set,{var,1},{call,symb_statem,foo,[1]}}],   % seq
+           [
+            [{set,{var,2},{call,symb_statem,croak,[]}}], % proc 1
+            []                                           % proc 2
+           ]}).
 
 prop_parallel_simple() ->
-    ?FORALL(Cmds, parallel_commands(?MODULE),
-	    begin
-		{S,P,Res} = run_parallel_commands(?MODULE, Cmds),
-		?WHENFAIL(
-		   io:format("Seq: ~w\nParallel: ~w\n:Res: ~w\n", [S,P,Res]),
-		   Res =:= ok)
-	    end).
+  ?FORALL(Cmds, croaking_commands(),
+          begin
+            {S,P,Res} = run_parallel_commands(?MODULE, Cmds),
+            ?WHENFAIL(
+               io:format(user, "Seq: ~w\nParallel: ~w\n:Res: ~w\n", [S,P,Res]),
+               Res =:= ok)
+          end).