Slightly different property

This commit is contained in:
Thomas Arts 2019-06-03 11:08:08 +02:00
parent e8390e52d1
commit 3d6ac9df92

View File

@ -65,24 +65,29 @@ prop_fuzz() ->
prop_order() -> prop_order() ->
?FORALL({FateData1, FateData2, FateData3}, {fate_data(), fate_data(), fate_data()}, ?FORALL(Items, vector(3, fate_data()),
case aeb_fate_data:lt(FateData1, FateData2) of begin
true -> %% Use lt to take minimum
case aeb_fate_data:lt(FateData2, FateData3) of Min = lt_min(Items),
true -> Max = lt_max(Items),
equals(aeb_fate_data:lt(FateData1, FateData3), true); conjunction([ {minimum, is_empty([ {Min, '>', I} || I<-Items, aeb_fate_data:lt(I, Min)])},
false -> {maximum, is_empty([ {Max, '<', I} || I<-Items, aeb_fate_data:lt(Max, I)])}])
equals(aeb_fate_data:lt(FateData2, FateData1), false)
end;
false ->
case aeb_fate_data:lt(FateData1, FateData3) of
true ->
equals(aeb_fate_data:lt(FateData2, FateData3), true);
false ->
equals(aeb_fate_data:elt(FateData2, FateData1), true)
end
end). end).
lt_min([X, Y | Rest]) ->
case aeb_fate_data:lt(X, Y) of
true -> lt_min([X | Rest]);
false -> lt_min([Y| Rest])
end;
lt_min([X]) -> X.
lt_max([X, Y | Rest]) ->
case aeb_fate_data:lt(X, Y) of
true -> lt_max([Y | Rest]);
false -> lt_max([X| Rest])
end;
lt_max([X]) -> X.
fate_data() -> fate_data() ->
?SIZED(Size, ?LET(Data, fate_data(Size, [map, variant]), eqc_symbolic:eval(Data))). ?SIZED(Size, ?LET(Data, fate_data(Size, [map, variant]), eqc_symbolic:eval(Data))).
@ -165,3 +170,6 @@ injection(Binary) ->
<<X:M, _:8, Z/binary>> = Binary, <<X:M, _:8, Z/binary>> = Binary,
<<X:M, Inj:8, Z/binary>> <<X:M, Inj:8, Z/binary>>
end). end).
is_empty(L) ->
?WHENFAIL(eqc:format("~p\n", [L]), L == []).