From 512b2b78aaad643a62655d3bc6369858e40fd08a Mon Sep 17 00:00:00 2001 From: Pierre Fenoll Date: Sun, 17 Jun 2018 21:16:21 +0200 Subject: [PATCH 1/3] introduce seed user option --- src/proper.erl | 5 +++++ test/proper_tests.erl | 48 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 53 insertions(+) diff --git a/src/proper.erl b/src/proper.erl index 84f044fd..a9fa6e5e 100644 --- a/src/proper.erl +++ b/src/proper.erl @@ -242,6 +242,8 @@ %%%
This is equivalent to the {@link numtests/1} property wrapper. Any %%% {@link numtests/1} wrappers in the actual property will overwrite this %%% user option.
+%%%
`{seed, {,,}}'
+%%%
Pass a seed to the RNG so that random results can be reproduced.
%%%
`{start_size, }'
%%%
Specifies the initial value of the `size' parameter (default is 1), see %%% the documentation of the {@link proper_types} module for details.
@@ -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; diff --git a/test/proper_tests.erl b/test/proper_tests.erl index 9619aa43..edd96f6b 100644 --- a/test/proper_tests.erl +++ b/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), From 6e2cf8f809a2dcb5beece3410da93fa7917f2327 Mon Sep 17 00:00:00 2001 From: Pierre Fenoll Date: Fri, 3 Apr 2020 18:52:44 +0200 Subject: [PATCH 2/3] deterministic TPBT Signed-off-by: Pierre Fenoll --- src/proper_arith.erl | 12 +++++++++++- src/proper_target.erl | 8 +++++--- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/proper_arith.erl b/src/proper_arith.erl index ce6404e8..26b1a991 100644 --- a/src/proper_arith.erl +++ b/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 = ?RANDOM_MOD:uniform(1000000), + B = ?RANDOM_MOD:uniform(1000000), + C = ?RANDOM_MOD:uniform(1000000), + {A,B,C}. + -spec rand_reseed() -> 'ok'. rand_reseed() -> _ = rand:seed(exsplus, os:timestamp()), diff --git a/src/proper_target.erl b/src/proper_target.erl index 7c3b04bc..d0e02fc5 100644 --- a/src/proper_target.erl +++ b/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 From fdc3f87fbe75846184e79e9a007764aadee2c605 Mon Sep 17 00:00:00 2001 From: Pierre Fenoll Date: Fri, 3 Apr 2020 20:10:36 +0200 Subject: [PATCH 3/3] derive seed with ?SEED_RANGE Signed-off-by: Pierre Fenoll --- src/proper_arith.erl | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/proper_arith.erl b/src/proper_arith.erl index 26b1a991..539f98fb 100644 --- a/src/proper_arith.erl +++ b/src/proper_arith.erl @@ -244,9 +244,9 @@ rand_restart(Seed) -> -spec rand_make_seed() -> proper_gen:seed(). rand_make_seed() -> {_,_} = get(?SEED_NAME), - A = ?RANDOM_MOD:uniform(1000000), - B = ?RANDOM_MOD:uniform(1000000), - C = ?RANDOM_MOD:uniform(1000000), + 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'.