diff --git a/test/parallel_crash_tests.erl b/test/parallel_crash_tests.erl new file mode 100644 index 00000000..fb8b6696 --- /dev/null +++ b/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()) + ]. diff --git a/test/symb_statem.erl b/test/symb_statem.erl index 71eadb13..39815b8b 100644 --- a/test/symb_statem.erl +++ b/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).