Arguments shrinking is not working in stateful models.

[SylwBar]

Hi. I'm preparing new stateful model with Proper 1.4 and realized that shrinking is not applied in stateful models (or I don't know how to trigger it).

I prepared minimal program explaining problem:

-module(proper_test).

-include_lib("proper/include/proper.hrl").
-compile(export_all).

tested_f(Arg) when Arg > 50 -> false;
tested_f(_) -> true.

happy_f() -> true.

prop_test_f() -> ?FORALL(Num, choose(1, 100), tested_f(Num) == true).

test_f() -> proper:quickcheck(prop_test_f()).

test_f_statem() -> proper:quickcheck(prop_test_f_statem()).

initial_state() -> #{}.

command(_State) -> oneof([
    {call, ?MODULE, tested_f, [choose(1, 100)]},
    {call, ?MODULE, happy_f, []}
]).

precondition(_State, {call, _Mod, _Fun, _Args}) -> true.

postcondition(_State, {call, _Mod, _Fun, _Args}, Res) -> Res == true.

next_state(State, _Res, {call, _Mod, _Fun, _Args}) -> State.

prop_test_f_statem() ->
  ?FORALL(Cmds, commands(?MODULE),
    begin
        {History, State, Result} = run_commands(?MODULE, Cmds),
          ?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n",
            [History,State,Result]),
            aggregate(command_names(Cmds), Result =:= ok))
    end).

For state-less property shrinking is working fine:

> proper_test:test_f().
....!
Failed: After 5 test(s).
100

Shrinking .(1 time(s))
51
false

51 is minimal example.

Here is example output from statem:

> proper_test:test_f_statem().
......!
Failed: After 7 test(s).
[{set,{var,1},{call,proper_test,happy_f,[]}},{set,{var,2},{call,proper_test,tested_f,[81]}}]
History: [{#{},true},{#{},false}]
State: #{}
Result: {postcondition,false}

Shrinking .(1 time(s))
[{set,{var,2},{call,proper_test,tested_f,[81]}}]
History: [{#{},false}]
State: #{}
Result: {postcondition,false}
false

Shrinking is working fine on sequences of commands i.e. - happy_f was removed from example. But argument to "tested_f" was not reduced - it is still 81. Is it intended behaviour? How I could trigger arguments shrinking in stateful models?

Regards Sylwester

[kostis]

In stateful PBT, the generator is a list of commands (each of them consisting of symbolic calls) and shrinking tries to produce a command sequence of minimal length. As you see in your example, it has done so.

The shrinking machinery in stateful PropEr has never taken the arguments of the commands into account, and there is no built-in support for shrinking them; the calls in the commands are symbolic anyway. If you really need this functionality, feel free to submit a PR that supports this.

[SylwBar]

Thank you for explanation. This feature is not very much needed right now so I'm closing issue.