From 6c67c7d87ad2a53f2baad1d390f6903dc380dc7b Mon Sep 17 00:00:00 2001
From: X4lldux <x4lldux@vectron.io>
Date: Sun, 29 Mar 2020 13:18:21 +0200
Subject: [PATCH] Add tests for `run_parallel_commands`

---
 test/parallel_statem.erl | 79 ++++++++++++++++++++++++++++++++++++++++
 test/proper_tests.erl    |  4 ++
 2 files changed, 83 insertions(+)
 create mode 100644 test/parallel_statem.erl

diff --git a/test/parallel_statem.erl b/test/parallel_statem.erl
new file mode 100644
index 00000000..4a62a595
--- /dev/null
+++ b/test/parallel_statem.erl
@@ -0,0 +1,79 @@
+%%% -*- coding: utf-8 -*-
+%%% -*- erlang-indent-level: 2 -*-
+%%% -------------------------------------------------------------------
+%%% From X4lldux
+%%%
+%%% When there was a crash in sequential phase of `run_parallel_commands`
+%%% the returned result was `{exception,_,_,_}` tuple, but when a crash
+%%% occurred in the parallel phase, then the `run_parallel_commands`
+%%% also crashed.
+%%%
+%%% -------------------------------------------------------------------
+
+-module(parallel_statem).
+
+%% -compile(export_all).
+-export([initial_state/0, next_state/3, precondition/2, postcondition/3]).
+-export([foo/1, crash/0]).
+-export([prop_parallel_crash/0, prop_sequential_crash/0]).
+
+-include_lib("proper/include/proper.hrl").
+
+
+initial_state() ->
+    [].
+
+precondition(_, _) ->
+    true.
+
+next_state(S, _V, {call,_,_,[_Arg]}) ->
+    S.
+
+postcondition(_, _, _) ->
+    true.
+
+foo(_) ->
+    ok.
+
+crash() ->
+    erlang:error(boom).
+
+
+parallel_crash_commands() ->
+    exactly(
+      {
+       [{set,{var,1},{call,?MODULE,foo,[1]}}],       % seq
+       [
+        [{set,{var,2},{call,?MODULE,crash,[]}}],     % proc 1
+        []                                           % proc 2
+       ]
+      }).
+
+sequential_crash_commands() ->
+    exactly(
+      {
+       [{set,{var,1},{call,?MODULE,crash,[]}}],      % seq
+       [
+        [{set,{var,2},{call,?MODULE,foo,[1]}}],      % proc 1
+        []                                           % proc 2
+       ]
+      }).
+
+prop_parallel_crash() ->
+    ?FORALL(Cmds, parallel_crash_commands(),
+            begin
+                {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds),
+                io:format(user, "Res: ~w\n", [Res]),
+
+assert_exception(Res)
+            end).
+
+prop_sequential_crash() ->
+    ?FORALL(Cmds, sequential_crash_commands(),
+            begin
+                {_S,_P,Res} = run_parallel_commands(?MODULE, Cmds),
+                assert_exception(Res)
+            end).
+
+assert_exception({exception, error, boom, _}) -> true;
+assert_exception(_) -> false.
diff --git a/test/proper_tests.erl b/test/proper_tests.erl
index 44429f95..dfb136a9 100644
--- a/test/proper_tests.erl
+++ b/test/proper_tests.erl
@@ -898,6 +898,10 @@ native_type_props_test_() ->
 -record(untyped, {a, b = 12}).
 -type untyped() :: #untyped{}.
 
+%% parallel_statem_test_() ->
+%%     [?_passes(parallel_statem:prop_parallel_crash()),
+%%      ?_passes(parallel_statem:prop_sequential_crash())].
+
 true_props_test_() ->
     [?_passes(?FORALL(X,integer(),X < X + 1)),
      ?_passes(?FORALL(A,atom(),list_to_atom(atom_to_list(A)) =:= A)),