|
| 1 | +%%% -*- coding: utf-8 -*- |
| 2 | +%%% -*- erlang-indent-level: 2 -*- |
| 3 | +%%% ------------------------------------------------------------------- |
| 4 | +%%% From X4lldux |
| 5 | +%%% |
| 6 | +%%% When there was a crash in sequential phase of `run_parallel_commands` |
| 7 | +%%% the returned result was `{exception,_,_,_}` tuple, but when a crash |
| 8 | +%%% occurred in the parallel phase, then the `run_parallel_commands` |
| 9 | +%%% also crashed. |
| 10 | +%%% |
| 11 | +%%% ------------------------------------------------------------------- |
| 12 | + |
| 13 | +-module(parallel_statem). |
| 14 | + |
| 15 | +%% -compile(export_all). |
| 16 | +-export([initial_state/0, next_state/3, precondition/2, postcondition/3]). |
| 17 | +-export([foo/1, crash/0]). |
| 18 | +-export([prop_parallel_crash/0, prop_sequential_crash/0]). |
| 19 | + |
| 20 | +-include_lib("proper/include/proper.hrl"). |
| 21 | + |
| 22 | + |
| 23 | +initial_state() -> |
| 24 | + []. |
| 25 | + |
| 26 | +precondition(_, _) -> |
| 27 | + true. |
| 28 | + |
| 29 | +next_state(S, _V, {call,_,_,[_Arg]}) -> |
| 30 | + S. |
| 31 | + |
| 32 | +postcondition(_, _, _) -> |
| 33 | + true. |
| 34 | + |
| 35 | +foo(_) -> |
| 36 | + ok. |
| 37 | + |
| 38 | +crash() -> |
| 39 | + erlang:error(boom). |
| 40 | + |
| 41 | + |
| 42 | +parallel_crash_commands() -> |
| 43 | + exactly( |
| 44 | + { |
| 45 | + [{set,{var,1},{call,?MODULE,foo,[1]}}], % seq |
| 46 | + [ |
| 47 | + [{set,{var,2},{call,?MODULE,crash,[]}}], % proc 1 |
| 48 | + [] % proc 2 |
| 49 | + ] |
| 50 | + }). |
| 51 | + |
| 52 | +sequential_crash_commands() -> |
| 53 | + exactly( |
| 54 | + { |
| 55 | + [{set,{var,1},{call,?MODULE,crash,[]}}], % seq |
| 56 | + [ |
| 57 | + [{set,{var,2},{call,?MODULE,foo,[1]}}], % proc 1 |
| 58 | + [] % proc 2 |
| 59 | + ] |
| 60 | + }). |
| 61 | + |
| 62 | +prop_parallel_crash() -> |
| 63 | + ?FORALL(Cmds, parallel_crash_commands(), |
| 64 | + begin |
| 65 | + {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds), |
| 66 | + assert_exception(Res) |
| 67 | + end). |
| 68 | + |
| 69 | +prop_sequential_crash() -> |
| 70 | + ?FORALL(Cmds, sequential_crash_commands(), |
| 71 | + begin |
| 72 | + {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds), |
| 73 | + assert_exception(Res) |
| 74 | + end). |
| 75 | + |
| 76 | +assert_exception({exception, error, boom, _}) -> true; |
| 77 | +assert_exception(_) -> false. |
0 commit comments