seed: introduce seed user option

src/proper.erl

@@ -242,6 +242,8 @@
 %%% <dd>This is equivalent to the {@link numtests/1} property wrapper. Any
 %%%   {@link numtests/1} wrappers in the actual property will overwrite this
 %%%   user option.</dd>
+%%% <dt>`{seed, {<Non_negative_integer>,<Non_negative_integer>,<Non_negative_integer>}}'</dt>
+%%% <dd>Pass a seed to the RNG so that random results can be reproduced.</dd>
 %%% <dt>`{start_size, <Size>}'</dt>
 %%% <dd>Specifies the initial value of the `size' parameter (default is 1), see
 %%%   the documentation of the {@link proper_types} module for details.</dd>
@@ -521,6 +523,7 @@
 		  | {'on_output',output_fun()}
 		  | {'search_steps',pos_integer()}
 		  | {'search_strategy',proper_target:strategy()}
+		  | {'seed',proper_gen:seed()}
 		  | {'skip_mfas',[mfa()]}
 		  | {'spec_timeout',timeout()}
 		  | {'start_size',proper_gen:size()}
@@ -982,6 +985,8 @@ parse_opt(UserOpt, Opts) ->
 	    ?VALIDATE_OPT(?POS_INTEGER(N), Opts#opts{search_steps = N});
 	{search_strategy,S} ->
 	    ?VALIDATE_OPT(is_atom(S), Opts#opts{search_strategy = S});
+	{seed,Seed} ->
+	    ?VALIDATE_OPT(((is_tuple(Seed) andalso tuple_size(Seed) == 3) andalso ?POS_INTEGER(element(1,Seed)) andalso ?POS_INTEGER(element(2,Seed)) andalso ?POS_INTEGER(element(3,Seed))), Opts#opts{seed = Seed});
 	{skip_mfas,L} ->
 	    IsMFA = fun ({M,F,A}) when is_atom(M), is_atom(F),
 				       is_integer(A), 0 =< A, A =< 255 -> true;

src/proper_arith.erl

@@ -33,7 +33,7 @@
 	 safe_any/2, safe_zip/2, tuple_map/2, cut_improper_tail/1,
 	 head_length/1, find_first/2, filter/2, partition/2, insert/3,%remove/2,
 	 unflatten/2]).
--export([rand_start/1, rand_restart/1, rand_reseed/0, rand_stop/0,
+-export([rand_start/1, rand_restart/1, rand_make_seed/0, rand_reseed/0, rand_stop/0,
 	 rand_int/1, rand_int/2, smart_rand_int/3, rand_non_neg_int/1,
 	 rand_float/1, rand_float/2, rand_non_neg_float/1,
 	 distribute/2, jumble/1, rand_choose/1, freq_choose/1]).
@@ -239,6 +239,16 @@ rand_restart(Seed) ->
             ok
     end.
 
+%% @doc Derives a 3-tuple seed from current PRNG instance.
+%% Throws if there is no such instance.
+-spec rand_make_seed() -> proper_gen:seed().
+rand_make_seed() ->
+    {_,_} = get(?SEED_NAME),
+    A = rand_int(0, ?SEED_RANGE -1),
+    B = rand_int(0, ?SEED_RANGE -1),
+    C = rand_int(0, ?SEED_RANGE -1),
+    {A,B,C}.
+
 -spec rand_reseed() -> 'ok'.
 rand_reseed() ->
     _ = rand:seed(exsplus, os:timestamp()),

src/proper_target.erl

@@ -137,7 +137,8 @@ init_strategy(#{search_steps := Steps, search_strategy := Strat}) ->
   Strategy = strategy(Strat),
   proper_gen_next:init(),
   Data = Strategy:init_strategy(Steps),
-  Args = [{Strategy, Data}],
+  Seed = proper_arith:rand_make_seed(),
+  Args = [{Strategy, Data, Seed}],
   {ok, TargetserverPid} = gen_server:start_link(?MODULE, Args, []),
   put('$targetserver_pid', TargetserverPid),
   update_pdict(),
@@ -274,8 +275,9 @@ strategy(Strat) ->
 %% -----------------------------------------------------------------------------
 
 %% @private
--spec init(Args :: [{strategy(), strategy_data()}]) -> {ok, state()}.
-init([{Strategy, Data}]) ->
+-spec init(Args :: [{strategy(), strategy_data(), proper_gen:seed()}]) -> {ok, state()}.
+init([{Strategy, Data, Seed}]) ->
+  proper_arith:rand_start(Seed),
   {ok, #state{strategy = Strategy, data = Data}}.
 
 %% @private

test/proper_tests.erl

@@ -1172,6 +1172,54 @@ options_test_() ->
 print_in_magenta(S, L) ->
    io:format("\033[1;35m"++S++"\033[0m", L).
 
+seeded_test_() ->
+   Seed = os:timestamp(),
+   BaseOpts = [noshrink, {start_size,65536}, quiet],
+   Seeded = fun (Prop) ->
+                R = proper:counterexample(Prop, [{seed,Seed}|BaseOpts]),
+                proper:clean_garbage(),
+                R
+            end,
+   NoSeed = fun (Prop) ->
+                R = proper:counterexample(Prop, BaseOpts),
+                proper:clean_garbage(),
+                R
+            end,
+   ReSeeded = fun (Prop) ->
+                  OtherSeed = os:timestamp(),
+                  R = proper:counterexample(Prop, [{seed,OtherSeed}|BaseOpts]),
+                  proper:clean_garbage(),
+                  R
+              end,
+   [[?_assert(state_is_clean()),
+     ?_assertMatch({Name,{_,Equals}} when Equals > 6, {Name,equaltimes(Seeded,Prop,Check,10)}),
+     ?_assert(state_is_clean()),
+     ?_assertMatch({Name,{_,Equals}} when Equals < 4, {Name,equaltimes(NoSeed,Prop,Check,10)}),
+     ?_assert(state_is_clean()),
+     ?_assertMatch({Name,{_,Equals}} when Equals < 4, {Name,equaltimes(ReSeeded,Prop,Check,10)}),
+     ?_assert(state_is_clean())]
+    %% For each of these properties...
+    || {Name,Prop} <- [{forall,?FORALL(_, integer(), false)},
+                       {trapexit,?FORALL(_, integer(), ?TRAPEXIT(false))},
+                       {targeted,?FORALL_TARGETED(I, integer(), begin ?MAXIMIZE(I),false end)}],
+       %% Ensure that, using a large enough size and at least 60% of the time:
+       %% * provided a seed, another run gives the same counterexample;
+       %% * when not provided a seed: run gives out differing results to the seeded one;
+       %% * and similarly when given a different seed.
+       Check <- [Seeded(Prop)]].
+
+equaltimes(Runner, Prop, Expected, Max) ->
+    equaltimes(Runner, Prop, Expected, Max, Max, []).
+equaltimes(_, _, _, Max, 0, Unexpecteds) ->
+    {Unexpecteds, Max - length(Unexpecteds)};
+equaltimes(Runner, Prop, Expected, Max, N, Acc) ->
+    case Runner(Prop) of
+        Expected ->
+            equaltimes(Runner, Prop, Expected, Max, N-1, Acc);
+        Got ->
+            equaltimes(Runner, Prop, Expected, Max, N-1, [Got|Acc])
+    end.
+
 setup_prop() ->
     ?SETUP(fun () ->
 		   put(setup_token, true),