Shrinking for statem silently terminates with {error, wrong_type} if os:timestamp/0 is used in a generator

[robertoaloi]

I noticed that occasionally the shrinking process triggered by a failed postcondition in my statem was silently terminating earlier than usual and that actions such as the WHENFAIL one were not performed after the shrinking. Tracing the proper code led to discover that this was due to the fact that the following clause was returning a wrong_type error:

run({forall, RawType, Prop}, #ctx{mode = try_shrunk,
                                  bound = [ImmInstance | Rest]} = Ctx, Opts) ->
    [...]

I managed to narrow down the issue to the usage of os:timestamp/0 in one of the generators (it was used to create custom dates). Here is a minimal example that shows the behaviour:

-module(ra_statem).
-compile([export_all, nowarn_export_all]).
-include_lib("proper/include/proper.hrl").

initial_state() -> [].
command(_S) -> oneof([ {call,?MODULE,foo,[timestamp()]} ]).
precondition(_, _) -> true.
next_state(S, _, _) -> S.
postcondition(_S, _, _) -> false.
timestamp() -> {1,2,3}.
foo(X) -> X.

prop_simple() ->
  ?FORALL(Cmds, commands(?MODULE),
          begin
            {_H,_S,Res} = run_commands(?MODULE, Cmds),
            equals(Res, ok)
          end).

Running proper, it gives the expected output:

> proper:quickcheck(ra_statem:prop_simple()).
.!
Failed: After 2 test(s).
[{set,{var,1},{call,ra_statem,foo,[{1,2,3}]}}]
{postcondition,false} =/= ok

Shrinking (0 time(s))
[{set,{var,1},{call,ra_statem,foo,[{1,2,3}]}}]
{postcondition,false} =/= ok
false

Let's now change the timestamp() generator to use the os:timestamp/0 function:

timestamp() -> ?LET(T, os:timestamp(), T).

And run proper again:

> l(ra_statem).
> proper:quickcheck(ra_statem:prop_simple()).
.!
Failed: After 2 test(s).
[{set,{var,1},{call,ra_statem,foo,[{1543,611231,655843}]}}]
{postcondition,false} =/= ok

Shrinking here
(0 time(s))
[{set,{var,1},{call,ra_statem,foo,[{1543,611231,655843}]}}]
false

Notice how the following line is missing after the shrinking:

{postcondition,false} =/= ok

Not sure if this is expected and if there is any documentation explaining the consequences of using os:timestamp/0 in a generator, or if this should simply be considered as a bug.

[TheGeorge]

I think this is caused by how PropEr checks that the values that get generated during shrinking are of the input type and how it handled non-generator input types such as immediate values. My guess is that the values that is generated by `os: timestamp()` is transformed into an `exactly()` generator for which `isinstance` reports true for the initial value. But somehow the timestamp function gets reevaluated during shrinking (and reports something different).

…

On Fri, Nov 30, 2018, 21:59 Roberto Aloi ***@***.***> wrote: I noticed that occasionally the shrinking process triggered by a failed postcondition in my statem was silently terminating earlier than usual and that actions such as the WHENFAIL one were not performed after the shrinking. Tracing the proper code led to discover that this was due to the fact that the following clause was returning a wrong_type error: run({forall, RawType, Prop}, #ctx{mode = try_shrunk, bound = [ImmInstance | Rest]} = Ctx, Opts) -> [...] I managed to narrow down the issue to the usage of os:timestamp/0 in one of the generators (it was used to create custom dates). Here is a minimal example that shows the behaviour: -module(ra_statem). -compile(export_all). -include_lib("proper/include/proper.hrl"). initial_state() -> []. command(_S) -> oneof([ {call,?MODULE,foo,[timestamp()]} ]). precondition(_, _) -> true. next_state(S, _, _) -> S. postcondition(S, _, _) -> false. timestamp() -> {1,2,3}. foo(X) -> X. prop_simple() -> ?FORALL(Cmds, commands(?MODULE), begin {_H,_S,Res} = run_commands(?MODULE, Cmds), equals(Res, ok) end). Running proper, it gives the expected output: > proper:quickcheck(ra_statem:prop_simple()). [{set,{var,1},{call,ra_statem,foo,[todo]}}] {postcondition,false} =/= ok Shrinking (0 time(s)) [{set,{var,1},{call,ra_statem,foo,[todo]}}] {postcondition,false} =/= ok false Let's now change the timestamp() generator to use the os:timestamp/0 function: [...] timestamp() -> ?LET(T, os:timestamp(), T). [...] And run proper again: > l(ra_statem). > proper:quickcheck(ra_statem:prop_simple()). .! Failed: After 2 test(s). [{set,{var,1},{call,ra_statem,foo,[{1543,611231,655843}]}}] {postcondition,false} =/= ok Shrinking here (0 time(s)) [{set,{var,1},{call,ra_statem,foo,[{1543,611231,655843}]}}] false Notice how the following line is missing after the shrinking: {postcondition,false} =/= ok Not sure if this is expected and if there is any documentation explaining the consequences of using os:timestamp/0 in a generator, or if this should simply be considered as a bug. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#186>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAR1j5qUJyyXYdFIljLtKRHK-4ER35G-ks5u0ZwagaJpZM4Y8Ybo> .

[kostis]

Thanks for opening this issue @robertoaloi !

Not sure if this is expected and if there is any documentation explaining the consequences of using os:timestamp/0 in a generator, or if this should simply be considered as a bug.

First of all, there is currently nothing in the documentation that mentions, let alone explains, issues that may arise when using functions as os:timestamp/0 as generators. Perhaps there should be, because the issue is more general.

I played a bit with this and discovered that the same behavior can be observed pretty much with any function that is non-deterministic (i.e., it's not a function). For example, substitute your timestamp() with a call to rand:uniform() in the line:

command(_S) -> oneof([ {call,?MODULE,foo,[rand:uniform()]} ]).

and you will also get:

1> c(ra_statem).
{ok,ra_statem}
2> proper:quickcheck(ra_statem:prop_simple()).
!
Failed: After 1 test(s).
[{set,{var,1},{call,ra_statem,foo,[0.9505026909878734]}}]
{postcondition,false} =/= ok

Shrinking (0 time(s))
[{set,{var,1},{call,ra_statem,foo,[0.9505026909878734]}}]
false

So, for shrinking to work properly, PropEr currently insists (requires?) that the generators are deterministic under its control, i.e., they do not contain any non-determinism that PropEr does not capture in the environment that it maintains.

Come to think of it, this requirement makes perfect sense. Whether it's insurmountable or whether there's something that can be done (e.g., abandon the attempt to shrink) when PropEr detects this situation, I will have to think more and look deeper in the code.

But it will help to have a wider (and more representative) collection of examples. Perhaps a stripped down version of the code you have (with a ?WHENFAIL) where you detected this problem, and also one with a ?SHRINK or ?LETSHRINK construct.

[robertoaloi]

As an additional note, Proper seems to actually save the counterexample after the wrong_type failure, so that commands such as rebar3 proper --store and rebar3 proper --retry work correctly after the failure. From a practical perspective, having proper to simply abandoning the attempt to shrink further (maybe with a warning message) sounds like a good idea.