?FORALL_TARGETED does not work with ?TRAPEXIT

[xspirus]

Bug

While in a previous PR #201 , there was a fix so that ?FORALL_TARGETED accepted properties with ?TRAPEXIT. However, after experimenting with the targeted interface, I came across a bug referring these two macros when used in conjuction.

Example

-module(trapexit).

-export([prop_normal_targeted/0, prop_trapexit_targeted/0]).

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

nf() ->
    fun(Prev, _T) ->
        integer(Prev, inf)
    end.

gen() ->
    ?USERNF(integer(), nf()).

prop_normal_targeted() ->
    ?FORALL_TARGETED(I, gen(), 
                     begin
                         ?MAXIMIZE(I),
                         I < 1000
                     end).

prop_trapexit_targeted() ->
    ?FORALL_TARGETED(I, gen(),
                     ?TRAPEXIT(
                        begin
                            ?MAXIMIZE(I),
                            I < 1000
                        end)).

Opening this program in an erlang shell we have the following:

1> c(trapexit).
{ok, trapexit}
2> proper:quickcheck(trapexit:prop_normal_targeted()).
................................................!
Failed: After 49 test(s).
1005

Shrinking .(1 time(s))
1000
false
3> proper:quickcheck(trapexit:prop_trapexit_targeted()).
....................................................................................................
OK: Passed 100 test(s).
true

It seems that when a property is wrapped within a ?TRAPEXIT, the targeted generation is not working properly.

Problem Source

The problem seems to be related with the way that proper_sa.erl is implemented. Specifically, it uses the process dictionary to store the current state of the targeted search. So when used in conjuction with ?TRAPEXIT, which spawns a new process, the progress of the search is not actually saved in the main process.

Solution

I have come up with a solution, which is just replacing the process dictionary with the use of a public ets table, in the proper_sa.erl implementation. I will create a Pull Request later so that it can be reviewed.