1%%% -*- coding: utf-8; erlang-indent-level: 2 -*-
2%%% -------------------------------------------------------------------
3%%% Copyright 2010-2021 Manolis Papadakis <manopapad@gmail.com>,
4%%%                     Eirini Arvaniti <eirinibob@gmail.com>
5%%%                 and Kostis Sagonas <kostis@cs.ntua.gr>
6%%%
7%%% This file is part of PropEr.
8%%%
9%%% PropEr is free software: you can redistribute it and/or modify
10%%% it under the terms of the GNU General Public License as published by
11%%% the Free Software Foundation, either version 3 of the License, or
12%%% (at your option) any later version.
13%%%
14%%% PropEr is distributed in the hope that it will be useful,
15%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
16%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
17%%% GNU General Public License for more details.
18%%%
19%%% You should have received a copy of the GNU General Public License
20%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
21
22%%% @copyright 2010-2021 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
23%%% @version {@version}
24%%% @author Manolis Papadakis
25%%% @doc This module contains PropEr's Unit tests. You need the EUnit
26%%%      application to compile it.
27
28-module(proper_tests).
29
30-compile([nowarn_untyped_record]).  % deliberately contains one untyped record
31
32-include_lib("proper/include/proper.hrl").
33-include_lib("eunit/include/eunit.hrl").
34
35%% NOTE: Possibly here temporarily until the compiler's warnings are fixed.
36-export_type([my_native_type/0, type_and_fun/0, type_only/0, id/1, lof/0]).
37-export_type([bin4/0, bits42/0, bits5x/0, bits7x/0, untyped/0]).
38
39%%------------------------------------------------------------------------------
40%% Helper macros
41%%------------------------------------------------------------------------------
42
43%% NOTE: Never add long_result to Opts for these macros.
44
45state_is_clean() ->
46    get() =:= [].
47
48assertEqualsOneOf(_X, none) ->
49    ok;
50assertEqualsOneOf(X, List) ->
51    ?assert(lists:any(fun(Y) -> Y =:= X end, List)).
52
53-define(_passes(Test),
54	?_passes(Test, [])).
55
56-define(_passes(Test, Opts),
57	?_assertRun(true, Test, Opts, true)).
58
59-define(_errorsOut(ExpReason, Test),
60	?_errorsOut(ExpReason, Test, [])).
61
62-define(_errorsOut(ExpReason, Test, Opts),
63	?_assertRun({error,ExpReason}, Test, Opts, true)).
64
65-define(_assertRun(ExpResult, Test, Opts, AlsoLongResult),
66	?_test(begin
67	    ?assertMatch(ExpResult, proper:quickcheck(Test,Opts)),
68	    proper:clean_garbage(),
69	    ?assert(state_is_clean()),
70	    case AlsoLongResult of
71		true ->
72		    ?assertMatch(ExpResult,
73				 proper:quickcheck(Test,[long_result|Opts])),
74		    proper:clean_garbage(),
75		    ?assert(state_is_clean());
76		false ->
77		    ok
78	    end
79	end)).
80
81-define(_assertCheck(ExpShortResult, CExm, Test),
82	?_assertCheck(ExpShortResult, CExm, Test, [])).
83
84-define(_assertCheck(ExpShortResult, CExm, Test, Opts),
85	?_test(?assertCheck(ExpShortResult, CExm, Test, Opts))).
86
87-define(assertCheck(ExpShortResult, CExm, Test, Opts),
88	begin
89	    ?assertMatch(ExpShortResult, proper:check(Test,CExm,Opts)),
90	    ?assert(state_is_clean())
91	end).
92
93-define(_fails(Test),
94	?_fails(Test, [])).
95
96-define(_fails(Test, Opts),
97	?_assertFailRun(none, Test, Opts)).
98
99-define(_failsWith(ExpCExm, Test),
100	?_failsWith(ExpCExm, Test, [])).
101
102-define(_failsWith(ExpCExm, Test, Opts),
103	?_assertFailRun(none, Test, Opts, ExpCExm)).
104
105-define(_failsWithOneOf(AllCExms, Test),
106	?_failsWithOneOf(AllCExms, Test, [])).
107
108-define(_failsWithOneOf(AllCExms, Test, Opts),
109	?_assertFailRun(AllCExms, Test, Opts)).
110
111-define(SHRINK_TEST_OPTS, [{start_size,10},{max_shrinks,10000}]).
112
113-define(_shrinksTo(ExpShrunk, Type),
114	?_assertFailRun(none, ?FORALL(_X,Type,false),
115			?SHRINK_TEST_OPTS, [ExpShrunk])).
116
117-define(_shrinksToOneOf(AllShrunk, Type),
118	?_assertFailRun([[X] || X <- AllShrunk], ?FORALL(_X,Type,false),
119			?SHRINK_TEST_OPTS)).
120
121-define(_nativeShrinksTo(ExpShrunk, TypeStr),
122	?_assertFailRun(none,
123			?FORALL(_X,assert_can_translate(?MODULE,TypeStr),false),
124			?SHRINK_TEST_OPTS, [ExpShrunk])).
125
126-define(_nativeShrinksToOneOf(AllShrunk, TypeStr),
127	?_assertFailRun([[X] || X <- AllShrunk],
128			?FORALL(_X,assert_can_translate(?MODULE,TypeStr),false),
129			?SHRINK_TEST_OPTS)).
130
131-define(_assertFailRun(AllCExms, Test, Opts),
132	?_test(begin
133		   ShortResult = proper:quickcheck(Test, Opts),
134		   CExm1 = get_cexm(),
135		   ?checkNoExpCExp(CExm1, AllCExms, Test, Opts),
136		   ?assertEqual(false, ShortResult),
137		   LongResult = proper:quickcheck(Test, [long_result|Opts]),
138		   CExm2 = get_cexm(),
139		   ?checkNoExpCExp(CExm2, AllCExms, Test, Opts),
140		   ?checkNoExpCExp(LongResult, AllCExms, Test, Opts)
141	       end)).
142-define(_assertFailRun(AllCExms, Test, Opts, ExpCExm),
143	?_test(begin
144		   ShortResult = proper:quickcheck(Test, Opts),
145		   CExm1 = get_cexm(),
146		   ?checkCExm(CExm1, AllCExms, Test, Opts, ExpCExm),
147		   ?assertEqual(false, ShortResult),
148		   LongResult = proper:quickcheck(Test, [long_result|Opts]),
149		   CExm2 = get_cexm(),
150		   ?checkCExm(CExm2, AllCExms, Test, Opts, ExpCExm),
151		   ?checkCExm(LongResult, AllCExms, Test, Opts, ExpCExm)
152	       end)).
153
154-define(_cexmMatchesWith(Pattern, Test),
155	?_test(begin
156		   ?assertEqual(false, proper:quickcheck(Test)),
157		   ?assertMatch(Pattern, get_cexm())
158	       end)).
159
160get_cexm() ->
161    CExm = proper:counterexample(),
162    proper:clean_garbage(),
163    ?assert(state_is_clean()),
164    CExm.
165
166%%
167%% The two macros below differ in that the first one we do not know the
168%% expected counterexample pattern, so there is no need to match against it.
169%%
170-define(checkNoExpCExp(CExm, AllCExms, Test, Opts),
171	begin
172	    ?assertCheck(false, CExm, Test, Opts),
173	    assertEqualsOneOf(CExm, AllCExms)
174	end).
175-define(checkCExm(CExm, AllCExms, Test, Opts, ExpCExm),
176	begin
177	    ?assertCheck(false, CExm, Test, Opts),
178	    ?assertMatch(ExpCExm, CExm),
179	    assertEqualsOneOf(CExm, AllCExms)
180	end).
181
182-define(_assertTempBecomesN(N, ExpShortResult, Prop),
183	?_assertTempBecomesN(N, ExpShortResult, Prop, [])).
184
185-define(_assertTempBecomesN(N, ExpShortResult, Prop, Opts),
186	?_test(begin
187		   ?assertMatch(ExpShortResult, proper:quickcheck(Prop, Opts)),
188		   ?assertEqual(N, get_temp()),
189		   erase_temp(),
190		   proper:clean_garbage(),
191		   ?assert(state_is_clean())
192	       end)).
193%%
194%% Used when we are only interested in checking that a property fails.
195%%
196-define(_failsChk(Test, Opts),
197	?_assertEqual(false, proper:quickcheck(Test, Opts))).
198
199inc_temp() ->
200    inc_temp(1).
201
202inc_temp(Inc) ->
203    case get(temp) of
204	undefined -> put(temp, Inc);
205	X         -> put(temp, X + Inc)
206    end,
207    ok.
208
209get_temp() ->
210    get(temp).
211
212erase_temp() ->
213    erase(temp),
214    ok.
215
216non_deterministic(Behaviour) ->
217    inc_temp(),
218    N = get_temp(),
219    {MustReset,Result} = get_result(N, 0, Behaviour),
220    case MustReset of
221	true  -> erase_temp();
222	false -> ok
223    end,
224    Result.
225
226get_result(N, Sum, [{M,Result}]) ->
227    {N >= Sum + M, Result};
228get_result(N, Sum, [{M,Result} | Rest]) ->
229    NewSum = Sum + M,
230    case N =< NewSum of
231	true  -> {false, Result};
232	false -> get_result(N, NewSum, Rest)
233    end.
234
235setup_run_commands(Module, Cmds, Env) ->
236    Module:set_up(),
237    Res = proper_statem:run_commands(Module, Cmds, Env),
238    Module:clean_up(),
239    Res.
240
241
242%%------------------------------------------------------------------------------
243%% Helper functions
244%%------------------------------------------------------------------------------
245
246assert_type_works({Type,Are,_Target,Arent,TypeStr}, IsSimple) ->
247    case Type of
248	none ->
249	    ok;
250	_ ->
251	    lists:foreach(fun(X) -> assert_is_instance(X,Type) end, Are),
252	    assert_can_generate(Type, IsSimple),
253	    lists:foreach(fun(X) -> assert_not_is_instance(X,Type) end, Arent)
254    end,
255    case TypeStr of
256	none ->
257	    ok;
258	_ ->
259	    TransType = assert_can_translate(?MODULE, TypeStr),
260	    lists:foreach(fun(X) -> assert_is_instance(X,TransType) end, Are),
261	    assert_can_generate(TransType, IsSimple),
262	    lists:foreach(fun(X) -> assert_not_is_instance(X,TransType) end,
263			  Arent)
264    end.
265
266assert_can_translate(Mod, TypeStr) ->
267    proper_typeserver:start(),
268    Type = {Mod,TypeStr},
269    Result1 = proper_typeserver:translate_type(Type),
270    Result2 = proper_typeserver:translate_type(Type),
271    proper_typeserver:stop(),
272    ?assert(state_is_clean()),
273    {ok,Type1} = Result1,
274    {ok,Type2} = Result2,
275    ?assert(proper_types:equal_types(Type1,Type2)),
276    Type1.
277
278assert_cant_translate(Mod, TypeStr) ->
279    proper_typeserver:start(),
280    Result = proper_typeserver:translate_type({Mod,TypeStr}),
281    proper_typeserver:stop(),
282    ?assert(state_is_clean()),
283    ?assertMatch({error,_}, Result).
284
285%% TODO: after fixing the type system, use generic reverse function.
286assert_is_instance(X, Type) ->
287    ?assert(proper_types:is_inst(X, Type) andalso state_is_clean()).
288
289assert_can_generate(Type, CheckIsInstance) ->
290    lists:foreach(fun(Size) -> try_generate(Type,Size,CheckIsInstance) end,
291		  [1, 2, 5, 10, 20, 40, 50]).
292
293try_generate(Type, Size, CheckIsInstance) ->
294    {ok,Instance} = proper_gen:pick(Type, Size),
295    ?assert(state_is_clean()),
296    case CheckIsInstance of
297	true  -> assert_is_instance(Instance, Type);
298	false -> ok
299    end.
300
301assert_seeded_runs_return_same_result(Type) ->
302    lists:foreach(fun(Size) -> try_generate_seeded(Type, Size) end,
303                  [1, 2, 5, 10, 20, 40, 50]).
304
305try_generate_seeded(Type, Size) ->
306    Seed = os:timestamp(),
307    {ok, Instance1} = proper_gen:pick(Type, Size, Seed),
308    {ok, Instance2} = proper_gen:pick(Type, Size, Seed),
309    ?assert(Instance1 =:= Instance2).
310
311assert_native_can_generate(Mod, TypeStr, CheckIsInstance) ->
312    assert_can_generate(assert_can_translate(Mod,TypeStr), CheckIsInstance).
313
314assert_cant_generate(Type) ->
315    ?assertEqual(error, proper_gen:pick(Type)),
316    ?assert(state_is_clean()).
317
318assert_cant_generate_cmds(Type, N) ->
319    ?assertEqual(error, proper_gen:pick(?SUCHTHAT(T, Type, length(T) > N))),
320    ?assert(state_is_clean()).
321
322assert_not_is_instance(X, Type) ->
323    ?assert(not proper_types:is_inst(X, Type) andalso state_is_clean()).
324
325assert_function_type_works(FunType) ->
326    {ok,F} = proper_gen:pick(FunType),
327    %% TODO: this isn't exception-safe
328    ?assert(proper_types:is_instance(F, FunType)),
329    assert_is_pure_function(F),
330    proper:global_state_erase(),
331    ?assert(state_is_clean()).
332
333assert_is_pure_function(F) ->
334    {arity,Arity} = erlang:fun_info(F, arity),
335    ArgsList = [lists:duplicate(Arity,0), lists:duplicate(Arity,1),
336		lists:seq(1,Arity), lists:seq(0,Arity-1)],
337    lists:foreach(fun(Args) -> ?assertEqual(apply(F,Args),apply(F,Args)) end,
338		  ArgsList).
339
340
341%%------------------------------------------------------------------------------
342%% Unit test arguments
343%%------------------------------------------------------------------------------
344
345simple_types_with_data() ->
346    [{integer(), [-1,0,1,42,-200], 0, [0.3,someatom,<<1>>], "integer()"},
347     {integer(7,88), [7,8,87,88,23], 7, [1,90,a], "7..88"},
348     {integer(0,42), [0,11,42], 0, [-1,43], "0..42"},
349     {integer(-99,0), [-88,-99,0], 0, [1,-1112], "-99..0"},
350     {integer(-999,-12), [-34,-999,-12], -12, [0,5], "-999..-12"},
351     {integer(-99,21), [-98,0,21], 0, [-100], "-99..21"},
352     {integer(0,0), [0], 0, [1,-1,100,-100], "0..0"},
353     {pos_integer(), [12,1,444], 1, [-12,0], "pos_integer()"},
354     {non_neg_integer(), [42,0], 0, [-9,rr], "non_neg_integer()"},
355     {neg_integer(), [-222,-1], -1, [0,1111], "neg_integer()"},
356     {float(), [17.65,-1.12], 0.0, [11,atomm,<<>>], "float()"},
357     {float(7.4,88.0), [7.4,88.0], 7.4, [-1.0,3.2], none},
358     {float(0.0,42.1), [0.1,42.1], 0.0, [-0.1], none},
359     {float(-99.9,0.0), [-0.01,-90.0], 0.0, [someatom,-12,-100.0,0.1], none},
360     {float(-999.08,-12.12), [-12.12,-12.2], -12.12, [-1111.0,1000.0], none},
361     {float(-71.8,99.0), [-71.8,99.0,0.0,11.1], 0.0, [100.0,-71.9], none},
362     {float(0.0,0.0), [0.0], 0.0, [0.1,-0.1], none},
363     {non_neg_float(), [88.8,98.9,0.0], 0.0, [-12,1,-0.01], none},
364     {atom(), [elvis,'Another Atom',''], '', ["not_an_atom",12,12.2], "atom()"},
365     {binary(), [<<>>,<<12,21>>], <<>>, [<<1,2:3>>,binary_atom,42], "binary()"},
366     {binary(), [], <<>>, [], "<<_:_*8>>"},
367     {binary(3), [<<41,42,43>>], <<0,0,0>>, [<<1,2,3,4>>], "<<_:24>>"},
368     {binary(0), [<<>>], <<>>, [<<1>>], "<<_:0>>"},
369     {bitstring(), [<<>>,<<87,76,65,5:4>>], <<>>, [{12,3},11], "bitstring()"},
370     {bitstring(), [], <<>>, [], "<<_:_*1>>"},
371     {bitstring(18), [<<0,1,2:2>>,<<1,32,123:2>>], <<0,0,0:2>>, [<<12,1,1:3>>],
372      "<<_:18, _:_*0>>"},
373     {bitstring(32), [<<120,120,120,120>>], <<0,0,0,0>>, [7,8], "<<_:32>>"},
374     {bitstring(0), [<<>>], <<>>, [<<1>>], "<<>>"},
375     {list(integer()), [[],[2,42],[0,1,1,2,3,5,8,13,21,34,55,89,144]], [],
376      [[4,4.2],{12,1},<<12,113>>], "[integer()]"},
377     {list(atom()), [[on,the,third,day,'of',christmas,my,true,love,sent,to,me]],
378      [], [['not',1,list,'of',atoms],not_a_list], "[atom()]"},
379     {list(union([integer(),atom()])), [[3,french,hens,2],[turtle,doves]], [],
380      [{'and',1}], "[integer() | atom()]"},
381     {vector(5,atom()), [[partridge,in,a,pear,tree],[a,b,c,d,e]],
382      ['','','','',''], [[a,b,c,d],[a,b,c,d,e,f]], none},
383     {vector(2,float()), [[0.0,1.1],[4.4,-5.5]], [0.0,0.0], [[1,1]], none},
384     {vector(0,integer()), [[]], [], [[1],[2]], none},
385     {union([good,bad,ugly]), [good,bad,ugly], good, [clint,"eastwood"],
386      "good | bad | ugly"},
387     {union([integer(),atom()]), [twenty_one,21], 0, ["21",<<21>>],
388      "integer() | atom()"},
389     {weighted_union([{10,luck},{20,skill},{15,concentrated_power_of_will},
390		      {5,pleasure},{50,pain},{100,remember_the_name}]),
391      [skill,pain,pleasure], luck, [clear,20,50], none},
392     {{integer(0,42),list(atom())}, [{42,[a,b]},{21,[c,de,f]},{0,[]}], {0,[]},
393      [{-1,[a]},{12},{21,[b,c],12}], "{0..42,[atom()]}"},
394     {tuple(), [{a,42},{2.56,<<42>>,{a}},{},{a,{a,17},3.14,{{}}}], {},
395      [#{a => 17},[{}],42], "tuple()"},
396     {tuple([atom(),integer()]), [{the,1}], {'',0}, [{"a",0.0}],
397      "{atom(),integer()}"},
398     {{}, [{}], {}, [[],{1,2}], "{}"},
399     {loose_tuple(integer()), [{1,44,-1},{},{99,-99}], {}, [4,{hello,2},[1,2]],
400      none},
401     {loose_tuple(union([atom(),float()])), [{a,4.4,b},{},{'',c},{1.2,-3.4}],
402      {}, [an_atom,0.4,{hello,2},[aa,bb,3.1]], none},
403     {loose_tuple(list(integer())), [{[1,-1],[],[2,3,-12]},{}], {},
404      [[[1,2],[3,4]],{1,12},{[1,99,0.0],[]}], none},
405     {loose_tuple(loose_tuple(integer())), [{},{{}},{{1,2},{-1,11},{}}], {},
406      [{123},[{12},{24}]], none},
407     {exactly({[writing],unit,[tests,is],{2},boring}),
408      [{[writing],unit,[tests,is],{2},boring}],
409      {[writing],unit,[tests,is],{2},boring}, [no,its,'not','!'], none},
410     {[], [[]], [], [[a],[1,2,3]], "[]"},
411     {fixed_list([neg_integer(),pos_integer()]), [[-12,32],[-1,1]], [-1,1],
412      [[0,0]], none},
413     {[atom(),integer(),atom(),float()], [[forty_two,42,forty_two,42.0]],
414      ['',0,'',0.0], [[proper,is,licensed],[under,the,gpl]], none},
415     {[42 | list(integer())], [[42],[42,44,22]], [42], [[],[11,12]], none},
416     {number(), [12,32.3,-9,-77.7], 0, [manolis,papadakis], "number()"},
417     {boolean(), [true,false], false, [unknown], "boolean()"},
418     {string(), ["hello","","world"], "", ['hello'], "string()"},
419     {arity(), [0,2,17,42,255], 0, [-1,256], "arity()"},
420     {timeout(), [0,42,infinity,666], 0, [-1,infinite,3.14], "timeout()"},
421     {?LAZY(integer()), [0,2,99], 0, [1.1], "integer()"},
422     {?LAZY(list(float())), [[0.0,1.2,1.99],[]], [], [1.1,[1,2]], "[float()]"},
423     {zerostream(10), [[0,0,0],[],[0,0,0,0,0,0,0]], [], [[1,0,0],[0.1]], none},
424     {?SHRINK(pos_integer(),[0]), [1,12,0], 0, [-1,-9,6.0], none},
425     {?SHRINK(float(),[integer(),atom()]), [1.0,0.0,someatom,'',42,0], 0,
426      [<<>>,"hello"], none},
427     {noshrink(?SHRINK(42,[0,1])), [42,0,1], 42, [-1], "42 | 0 | 1"},
428     {non_empty(list(integer())), [[1,2,3],[3,42],[11]], [0], [[],[0.1]],
429      "[integer(),...]"},
430     {default(42,float()), [4.1,-99.0,0.0,42], 42, [43,44], "42 | float()"},
431     {?SUCHTHAT(X,non_neg_integer(),X rem 4 =:= 1), [1,5,37,89], 1, [4,-12,11],
432      none},
433     {?SUCHTHATMAYBE(X,non_neg_integer(),X rem 4 =:= 1), [1,2,3,4,5,37,89], 0,
434      [1.1,2.2,-12], "non_neg_integer()"},
435     {?SUCHTHAT(L, non_empty(list(non_neg_integer())), hd(L) < 5),
436      [[1], [1,2,3,4], [0,2]], [0], [[], "Fail","something", [5]], none},
437     {any(), [1,-12,0,99.9,-42.2,0.0,an_atom,'',<<>>,<<1,2>>,<<1,2,3:5>>,[],
438	      [42,<<>>],{},{tag,12},{tag,[vals,12,12.2],[],<<>>}],
439	     0, [], "any()"},
440     {list(any()), [[<<>>,a,1,-42.0,{11.8,[]}]], [], [{1,aa},<<>>], "[any()]"},
441     {deeplist(), [[[],[]], [[[]],[]]], [], [[a]], "deeplist()"},
442     {none, [[234,<<1>>,[<<78>>,[]],0],[]], [], [21,3.1,[7.1],<<22>>],
443      "iolist()"},
444     {none, [[234,<<1>>,[<<78>>,[]],0],[],<<21,15>>], <<>>, [21,3.1,[7.1]],
445      "iodata()"}].
446
447%% TODO: These rely on the intermediate form of the instances.
448constructed_types_with_data() ->
449    [{?LET({A,B},{bitstring(3),binary()},<<A/bits,B/bits>>),
450      [{'$used',{<<1:3>>,<<3,4>>},<<32,96,4:3>>}], <<0:3>>, [],
451      "<<_:3,_:_*8>>"},
452     {?LET(X,range(1,5),X*X), [{'$used',1,1},{'$used',5,25}], 1,
453      [4,{'$used',3,8},{'$used',0,0}], none},
454     {?LET(L,non_empty(list(atom())),oneof(L)),
455      [{'$used',[aa],aa},{'$used',[aa,bb],aa},{'$used',[aa,bb],bb}], '',
456      [{'$used',[],''},{'$used',[aa,bb],cc}], none},
457     {?LET(X,pos_integer(),?LET(Y,range(0,X),X-Y)),
458      [{'$used',3,{'$used',2,1}},{'$used',9,{'$used',9,0}},
459       {'$used',5,{'$used',0,5}}], 1,
460      [{'$used',0,{'$used',0,0}},{'$used',3,{'$used',4,-1}},
461       {'$used',7,{'$used',6,2}}], none},
462     {?LET(Y,?LET(X,integer(),X*X),-Y),
463      [{'$used',{'$used',-9,81},-81},{'$used',{'$used',2,4},-4}], 0,
464      [{'$used',{'$used',1,2},-2},{'$used',{'$used',3,9},9}], none},
465     {?SUCHTHAT(Y,?LET(X,oneof([1,2,3]),X+X),Y>3),
466      [{'$used',2,4},{'$used',3,6}], 4, [{'$used',1,2}], none},
467     {?LET(X,?SUCHTHAT(Y,pos_integer(),Y=/=0),X*X),
468      [{'$used',3,9},{'$used',1,1},{'$used',11,121}], 1,
469      [{'$used',-1,1},{'$used',0,0}], none},
470     {tree(integer()), [{'$used',[null,null],{node,42,null,null}},
471			{'$used',[{'$used',[null,null],{node,2,null,null}},
472				  {'$used',[null,null],{node,3,null,null}}],
473			 {node,-1,{node,2,null,null},{node,3,null,null}}},
474			 {'$to_part',null},
475			 {'$to_part',{'$used',[null,null],{node,7,null,null}}}],
476      null, [{'$used',[null,null],{node,1.1,null,null}}], "tree(integer())"},
477     {?LETSHRINK(L,[],{tag,L}), [{'$used',[],{tag,[]}}], {tag,[]}, [], none},
478     {?LETSHRINK(L,non_empty(list(atom())),{tag,L}),
479      [{'$used',[aa],{tag,[aa]}},{'$to_part',aa}], '', [], none},
480     {a(), [aleaf, {'$used',[aleaf],{anode,aleaf,bleaf}},
481	    {'$used',[aleaf],{anode,aleaf,{'$to_part',bleaf}}}],
482      aleaf, [], "a()"},
483     {b(), [bleaf, {'$used',[bleaf],{bnode,aleaf,bleaf}},
484	    {'$used',[bleaf],{bnode,{'$to_part',aleaf},bleaf}}],
485      bleaf, [], "b()"},
486     {gen_tree(integer()),
487      [{'$used',[null,null],{12,[null,null]}},{'$to_part',null}],
488      null, [{'$used',[],{42,[]}}], "gen_tree(integer())"},
489     {none, [{'$used',[],{tag,[]}}, {'$used',[null,null],{tag,[null,null]}},
490	     {'$used',[{'$used',[],{tag,[]}},{'$to_part',null}],
491	      {tag,[{tag,[]},null]}}, {'$to_part',{'$used',[],{tag,[]}}}],
492      null, [], "g()"},
493     {none, [{'$used',[null],{tag,[{ok,null}]}}, {'$to_part',null},
494	     {'$used',[null,null],{tag,[{ok,null},{ok,null}]}}],
495      null, [], "h()"},
496     {none, [{'$used',[null,null,{'$used',[null],{tag,null,[]}}],
497	      {tag,null,[null,{tag,null,[]}]}}, {'$to_part',null}],
498      null, [], "i()"},
499     {none, [{'$used',[{'$to_part',null},{'$used',[null],{one,null}},null,null],
500	      {tag,null,{one,null},[null,null],[null]}}], null, [], "j()"},
501     {none, [{tag,[]}, {tag,[{null,null}]},
502	     {tag,[{{tag,[]},null},{null,{tag,[]}}]}],
503      null, [{'$to_part',null}], "k()"},
504     {none, [{'$used',[null,null,{'$used',[null,null],{tag,null,[null]}}],
505	      {tag,null,[null,{tag,null,[null]}]}}, {'$to_part',null}],
506      null, [{'$used',[null],{tag,null,[]}}], "l()"},
507     {utf8(), [{'$used',{'$used',0,[]},<<>>}, {'$used',{'$used',1,[0]},<<0>>},
508	       {'$used',{'$used',1,[127]},<<127>>},
509	       {'$used',{'$used',1,[353]},<<197,161>>}],
510      <<>>, [{'$used',{'$used',1,[128]},<<128>>}], none},
511     {utf8(0), [{'$used',{'$used',0,[]},<<>>}], <<>>, [], none},
512     {utf8(1), [{'$used',{'$used',0,[]},<<>>},
513		{'$used',{'$used',1,[127]},<<127>>},
514		{'$used',{'$used',1,[353]},<<197,161>>}], <<>>, [], none},
515     {utf8(2), [{'$used',{'$used',1,[353]},<<197,161>>},
516		{'$used',{'$used',2,[127,353]},<<127,197,161>>}],
517      <<>>, [], none},
518     {utf8(inf, 1), [{'$used',{'$used',0,[]},<<>>},
519		     {'$used',{'$used',1,[0]},<<0>>},
520		     {'$used',{'$used',2,[0,0]},<<0,0>>},
521		     {'$used',{'$used',3,[0,0,0]},<<0,0,0>>}], <<>>, [], none},
522     {utf8(inf, 2), [{'$used',{'$used',3,[0,0,0]},<<0,0,0>>},
523		     {'$used',{'$used',1,[353]},<<197,161>>}],
524      <<>>, [], none}].
525
526function_types() ->
527    [{function([],atom()), "fun(() -> atom())"},
528     {function([integer(),integer()],atom()),
529      "fun((integer(),integer()) -> atom())"},
530     {function(5,union([a,b])), "fun((_,_,_,_,_) -> a | b)"},
531     {function(0,function(1,integer())),
532      "fun(() -> fun((_) -> integer()))"}].
533
534remote_native_types() ->
535    [{types_test1,["#rec1{}","rec1()","exp1()","type1()","type2(atom())",
536		   "rem1()","rem2()","types_test1:exp1()",
537		   "types_test2:exp1(float())","types_test2:exp2()"]},
538     {types_test2,["exp1(#rec1{})","exp2()","#rec1{}","types_test1:exp1()",
539		   "types_test2:exp1(binary())","types_test2:exp2()"]}].
540
541impossible_types() ->
542    [?SUCHTHAT(X, pos_integer(), X =< 0),
543     ?SUCHTHAT(X, non_neg_integer(), X < 0),
544     ?SUCHTHAT(X, neg_integer(), X >= 0),
545     ?SUCHTHAT(X, integer(1,10), X > 20),
546     ?SUCHTHAT(X, float(0.0,10.0), X < 0.0),
547     ?SUCHTHAT(L, vector(12,integer()), length(L) =/= 12),
548     ?SUCHTHAT(B, binary(), lists:member(256,binary_to_list(B))),
549     ?SUCHTHAT(X, exactly('Lelouch'), X =:= 'vi Brittania'),
550     ?SUCHTHAT(X, utf8(), unicode:characters_to_list(X) =:= [16#D800]),
551     ?SUCHTHAT(X, utf8(1, 1), size(X) > 1),
552     %% Nested constraints, of which the inner one fails
553     ?SUCHTHAT(X, ?SUCHTHAT(Y, pos_integer(), Y < 0), X > 0),
554     %% Nested constraints, of which the outer one fails
555     ?SUCHTHAT(X, ?SUCHTHAT(Y, pos_integer(), Y > 0), X < 0),
556     %% Nested constraints, one strict and one non-strict, where the
557     %% inner one fails
558     ?SUCHTHATMAYBE(_X, ?SUCHTHAT(Y, pos_integer(), Y < 0), true),
559     %% Nested constraints, one strict and one non-strict, where the
560     %% outer one fails
561     ?SUCHTHAT(X, ?SUCHTHATMAYBE(Y, pos_integer(), Y < 0), X < 0),
562     %% Two failing constraints within a ?LET macro, where both
563     %% constraints are used as a 'raw type'
564     ?LET({X,Y}, {?SUCHTHAT(X1, pos_integer(), X1 < 0),
565		  ?SUCHTHAT(Y1, pos_integer(), Y1 < 0)}, {X,Y})
566    ].
567
568impossible_native_types() ->
569    [{types_test1, ["1.1","no_such_module:type1()","no_such_type()"]},
570     {types_test2, ["types_test1:type1()","function()","fun((...) -> atom())",
571		    "pid()","port()","ref()"]}].
572
573recursive_native_types() ->
574    [{rec_test1, ["a()","b()","a()|b()","d()","f()","deeplist()",
575		  "mylist(float())","aa()","bb()","expc()"]},
576     {rec_test2, ["a()","expa()","rec()"]}].
577
578impossible_recursive_native_types() ->
579    [{rec_test1, ["c()","e()","cc()","#rec{}","expb()"]},
580     {rec_test2, ["b()","#rec{}","aa()"]}].
581
582symb_calls() ->
583    [{[3,2,1], "lists:reverse([1,2,3])", [], {call,lists,reverse,[[1,2,3]]}},
584     {[a,b,c,d], "erlang:'++'([a,b],[c,d])",
585      [{a,some_value}], {call,erlang,'++',[[a,b],[c,d]]}},
586     {42, "erlang:'*'(erlang:'+'(3,3),erlang:'-'(8,1))",
587      [{b,dummy_value},{e,another_dummy}],
588      {call,erlang,'*',[{call,erlang,'+',[3,3]},{call,erlang,'-',[8,1]}]}},
589     {something, "something",
590      [{a,somebody},{b,put},{c,something},{d,in_my_drink}], {var,c}},
591     {{var,b}, "{var,b}", [{a,not_this},{c,neither_this}], {var,b}},
592     {42, "erlang:'+'(40,2)", [{m,40},{n,2}],
593      {call,erlang,'+',[{var,m},{var,n}]}},
594     {[i,am,{var,iron},man],
595      "erlang:'++'(lists:reverse([am,i]),erlang:'++'([{var,iron}],[man]))",
596      [{a,man},{b,woman}],
597      {call,erlang,'++',[{call,lists,reverse,[[am,i]]},
598			 {call,erlang,'++',[[{var,iron}],[{var,a}]]}]}}].
599
600undefined_symb_calls() ->
601    [{call,erlang,error,[an_error]},
602     {call,erlang,throw,[a_throw]},
603     {call,erlang,exit,[an_exit]},
604     {call,lists,reverse,[<<12,13>>]},
605     {call,erlang,'+',[1,2,3]}].
606
607combinations() ->
608    [{[{1,[1,3,5,7,9,10]}, {2,[2,4,6,8,11]}], 5, 11, [1,2,3,4,5,6,7,8,9,10,11], 2, 2,
609      [{1,[1,3,5,7,8,11]}, {2,[2,4,6,9,10]}]},
610     {[{1,[1,3,5]}, {2,[7,8,9]}, {3,[2,4,6]}], 3, 9, [1,3,5,7,8,9], 3, 2,
611      [{1,[6,8,9]}, {2,[1,3,5]}, {3,[2,4,7]}]}].
612
613first_comb() ->
614    [{10,3,3,[{1,[7,8,9,10]}, {2,[4,5,6]}, {3,[1,2,3]}]},
615     {11,5,2,[{1,[6,7,8,9,10,11]}, {2,[1,2,3,4,5]}]},
616     {12,3,4,[{1,[10,11,12]}, {2,[7,8,9]}, {3,[4,5,6]}, {4,[1,2,3]}]}].
617
618lists_to_zip() ->
619    [{[],[],[]},
620     {[], [dummy, atom], []},
621     {[1, 42, 1, 42, 1, 2 ,3], [], []},
622     {[a, b, c], lists:seq(1,6), [{a,1}, {b,2}, {c,3}]},
623     {[a, b, c], lists:seq(1,3), [{a,1}, {b,2}, {c,3}]},
624     {[a, d, d, d, d], lists:seq(1,3), [{a,1}, {d,2}, {d,3}]}].
625
626command_names() ->
627    [{[{set,{var,1},{call,erlang,put,[a,0]}},
628       {set,{var,3},{call,erlang,erase,[a]}},
629       {set,{var,4},{call,erlang,get,[b]}}],
630      [{erlang,put,2},
631       {erlang,erase,1},
632       {erlang,get,1}]},
633     {[{set,{var,1},{call,foo,bar,[]}},
634       {set,{var,2},{call,bar,foo,[a,{var,1}]}},
635       {set,{var,3},{call,bar,foo,[a,[[3,4]]]}}],
636      [{foo,bar,0},
637       {bar,foo,2},
638       {bar,foo,2}]},
639     {[],[]}].
640
641valid_command_sequences() ->
642    %% {module, initial_state, command_sequence, symbolic_state_after,
643    %%  dynamic_state_after,initial_environment}
644    [{pdict_statem, [], [{init,[]},
645			 {set,{var,1},{call,erlang,put,[a,0]}},
646			 {set,{var,2},{call,erlang,put,[b,1]}},
647			 {set,{var,3},{call,erlang,erase,[a]}},
648			 {set,{var,4},{call,erlang,get,[b]}},
649			 {set,{var,5},{call,erlang,erase,[b]}},
650			 {set,{var,6},{call,erlang,put,[a,4]}},
651			 {set,{var,7},{call,erlang,put,[a,42]}}],
652      [{a,42}], [{a,42}], []},
653     {pdict_statem, [], [{init,[]},
654			 {set,{var,1},{call,erlang,put,[b,5]}},
655			 {set,{var,2},{call,erlang,erase,[b]}},
656			 {set,{var,3},{call,erlang,put,[a,5]}}],
657      [{a,5}], [{a,5}], []},
658     {pdict_statem, [], [{init,[]},
659			 {set,{var,1},{call,erlang,put,[a,{var,start_value}]}},
660			 {set,{var,2},{call,erlang,put,[b,{var,another_start_value}]}},
661			 {set,{var,3},{call,erlang,get,[b]}},
662			 {set,{var,4},{call,erlang,get,[b]}}],
663      [{b,{var,another_start_value}}, {a,{var,start_value}}], [{b,-1}, {a, 0}],
664      [{start_value, 0}, {another_start_value, -1}]}].
665
666symbolic_init_invalid_sequences() ->
667    %% {module, command_sequence, environment, shrunk}
668    [{pdict_statem, [{init,[{a,{call,foo,bar,[some_arg]}}]},
669		     {set,{var,1},{call,erlang,put,[b,42]}},
670		     {set,{var,2},{call,erlang,get,[b]}}],
671      [{some_arg, 0}],
672      [{init,[{a,{call,foo,bar,[some_arg]}}]}]}].
673
674invalid_precondition() ->
675    %% {module, command_sequence, environment, shrunk}
676    [{pdict_statem, [{init,[]},
677		      {set,{var,1},{call,erlang,put,[a,0]}},
678		      {set,{var,2},{call,erlang,put,[b,1]}},
679		      {set,{var,3},{call,erlang,erase,[a]}},
680		      {set,{var,4},{call,erlang,get,[a]}}],
681       [], [{set,{var,4},{call,erlang,get,[a]}}]}].
682
683invalid_var() ->
684    [{pdict_statem, [{init,[]},
685		     {set,{var,2},{call,erlang,put,[b,{var,1}]}}]},
686     {pdict_statem, [{init,[]},
687		     {set,{var,1},{call,erlang,put,[b,9]}},
688		     {set,{var,5},{call,erlang,put,[a,3]}},
689		     {set,{var,6},{call,erlang,get,[{var,2}]}}]}].
690
691arguments_not_defined() ->
692    [{[simple,atoms,are,valid,{var,42}], []},
693     {[{var,1}], [{var,2},{var,3},{var,4}]},
694     {[hello,world,[hello,world,{var,6}]], []},
695     {[{1,2,3,{var,1},{var,2}},not_really], []},
696     {[[[[42,{var,42}]]]], []},
697     {[{43,41,{1,{var,42}}},why_not], []}].
698
699all_data() ->
700    [1, 42.0, "$hello", "world\n", [smelly, cat, {smells,bad}],
701     '$this_should_be_copied', '$this_one_too', 'but$ this$ not',
702     or_this].
703
704dollar_data() ->
705    ['$this_should_be_copied', '$this_one_too'].
706
707%%------------------------------------------------------------------------------
708%% Unit tests
709%%------------------------------------------------------------------------------
710
711%% TODO: write tests for old datatypes, use old tests
712%% TODO: check output redirection, quiet, verbose, to_file, on_output/2 (maybe
713%%       by writing to a string in the process dictionary), statistics printing,
714%%	 standard verbose behaviour
715%% TODO: fix compiler warnings
716%% TODO: LET and LETSHRINK testing (these need their intermediate form for
717%%	 standalone instance testing and shrinking) - update needed after
718%%	 fixing the internal shrinking in LETs, use recursive datatypes, like
719%%	 trees, for testing, also test with noshrink and LAZY
720%% TODO: use size=100 for is_instance testing?
721%% TODO: typeserver: check that the same type is returned for consecutive calls,
722%%	 even with no caching (no_caching option?)
723%% TODO: typeserver: recursive types containing functions
724%% TODO: ?LET, ?LETSHRINK: only the top-level base type can be a native type
725%% TODO: Test with native types: ?SUCHTHATMAYBE, noshrink, ?LAZY, ?SHRINK,
726%%	 resize, ?SIZED
727%% TODO: no debug_info at compile time => call, not type
728%%	 no debug_info at runtime => won't find type
729%%	 no module in code path at runtime => won't find type
730%% TODO: try some more expressions with a ?FORALL underneath
731%% TODO: various constructors like '|' (+ record notation) are parser-rejected
732%% TODO: test nonempty recursive lists
733%% TODO: test list-recursive with instances
734%% TODO: more ADT tests: check bad declarations, bad variable use, multi-clause,
735%%	 is_subtype, unacceptable range, unexported opaque, no-specs opaque,
736%%	 unexported/unspecced functions, unbound variables, check as constructed
737%% TODO: module, check_spec, check_module_specs, retest_spec (long result mode
738%%	 too, other options pass)
739%% TODO: proper_typeserver:is_instance (with existing types too, plus types we
740%%	 can't produce, such as impropers) (also check that everything we
741%%	 produce based on a type is an instance)
742%% TODO: check that functions that throw exceptions pass
743%% TODO: property inside a ?TIMEOUT returning false
744%% TODO: some branch of a ?FORALL has a collect while another doesn't
745%% TODO: symbolic functions returning functions are evaluated?
746%% TODO: pure_check
747%% TODO: spec_timeout option
748%% TODO: defined option precedence
749%% TODO: conversion of maybe_improper_list
750%% TODO: debug option to output tests passed, fail reason, etc.
751%% TODO: test expected distribution of random functions
752
753simple_types_test_() ->
754    [?_test(assert_type_works(TD, true)) || TD <- simple_types_with_data()].
755
756constructed_types_test_() ->
757    [?_test(assert_type_works(TD, false))
758     || TD <- constructed_types_with_data()].
759
760%% TODO: specific test-starting instances would be useful here
761%%	 (start from valid Xs)
762shrinks_to_test_() ->
763    All = simple_types_with_data() ++ constructed_types_with_data(),
764    [?_shrinksTo(Target, Type)
765     || {Type,_Xs,Target,_Ys,_TypeStr} <- All, Type =/= none].
766
767native_shrinks_to_test_() ->
768    All = simple_types_with_data() ++ constructed_types_with_data(),
769    [?_nativeShrinksTo(Target, TypeStr)
770     || {_Type,_Xs,Target,_Ys,TypeStr} <- All, TypeStr =/= none].
771
772cant_generate_test_() ->
773    [?_test(assert_cant_generate(Type)) || Type <- impossible_types()].
774
775proper_exported_types_test_() ->
776    [?_assertEqual({[],12}, proper_exported_types_test:not_handled())].
777
778%%------------------------------------------------------------------------------
779%% Verify that failing constraints are correctly reported
780%%------------------------------------------------------------------------------
781
782cant_generate_constraints_test_() ->
783  [%% An impossible generator specified in the same function
784   ?_errorsOut({cant_generate, [{?MODULE, cant_generate_constraints_test_, 0}]},
785               ?FORALL(_, ?SUCHTHAT(X, pos_integer(), X =< 0), true)),
786   %% An impossible generator specified in a separate function
787   ?_errorsOut({cant_generate, [{?MODULE, impossible, 0}]},
788               ?FORALL(_X, impossible(), true)),
789   %% An impossible generator in presence of multiple constraints
790   ?_errorsOut({cant_generate, [{?MODULE, possible, 0},
791				{?MODULE, possible_made_impossible, 0}]},
792               ?FORALL(_X, possible_made_impossible(), true)),
793   %% An impossible generator in presence of multiple, duplicated constraints
794   ?_errorsOut({cant_generate, [{?MODULE, possible, 0},
795				{?MODULE, possible_made_impossible_2, 0}]},
796               ?FORALL(_X, possible_made_impossible_2(), true))
797  ].
798
799possible() ->
800  ?SUCHTHAT(X, pos_integer(), X > 0).
801
802impossible() ->
803  ?SUCHTHAT(X, pos_integer(), X =< 0).
804
805possible_made_impossible() ->
806  ?SUCHTHAT(X, possible(), X =< 0).
807
808possible_made_impossible_2() ->
809  ?SUCHTHAT(Y, ?SUCHTHAT(X, possible(), X =< 0), Y =< 0).
810
811%%------------------------------------------------------------------------------
812
813native_cant_translate_test_() ->
814    [?_test(assert_cant_translate(Mod,TypeStr))
815     || {Mod,Strings} <- impossible_native_types(), TypeStr <- Strings].
816
817remote_native_types_test_() ->
818    [?_test(assert_can_translate(Mod,TypeStr))
819     || {Mod,Strings} <- remote_native_types(), TypeStr <- Strings].
820
821recursive_native_types_test_() ->
822    [?_test(assert_native_can_generate(Mod,TypeStr,false))
823     || {Mod,Strings} <- recursive_native_types(), TypeStr <- Strings].
824
825recursive_native_cant_translate_test_() ->
826    [?_test(assert_cant_translate(Mod,TypeStr))
827     || {Mod,Strings} <- impossible_recursive_native_types(),
828	TypeStr <- Strings].
829
830random_functions_test_() ->
831    [[?_test(assert_function_type_works(FunType)),
832      ?_test(assert_function_type_works(assert_can_translate(proper,TypeStr)))]
833     || {FunType,TypeStr} <- function_types()].
834
835parse_transform_test_() ->
836    [?_passes(auto_export_test1:prop_1()),
837     ?_assertError(undef, auto_export_test2:prop_1()),
838     ?_assertError(undef, no_native_parse_test:prop_1()),
839     ?_passes(let_tests:prop_1()),
840     ?_failsWith([3*42], let_tests:prop_2())].
841
842native_type_props_test_() ->
843    [?_passes(?FORALL({X,Y}, {my_native_type(),my_proper_type()},
844		      is_integer(X) andalso is_atom(Y))),
845     ?_passes(?FORALL([X,Y,Z],
846		      [my_native_type(),my_proper_type(),my_native_type()],
847		      is_integer(X) andalso is_atom(Y) andalso is_integer(Z))),
848     ?_passes(?FORALL([Y,X,{Z,W}],
849		      [my_proper_type() | [my_native_type()]] ++
850		      [{my_native_type(),my_proper_type()}],
851		      is_integer(X) andalso is_atom(Y) andalso is_integer(Z)
852		      andalso is_atom(W))),
853     ?_passes(?FORALL([X|Y], [my_native_type()|my_native_type()],
854		      is_integer(X) andalso is_integer(Y))),
855     ?_passes(?FORALL(X, type_and_fun(), is_atom(X))),
856     ?_passes(?FORALL(X, type_only(), is_integer(X))),
857     ?_passes(?FORALL(L, [integer()], length(L) =:= 1)),
858     ?_fails(?FORALL(L, id([integer()]), length(L) =:= 1)),
859     ?_passes(?FORALL(_, types_test1:exp1(), true)),
860     ?_assertError(undef, ?FORALL(_,types_test1:rec1(),true)),
861     ?_assertError(undef, ?FORALL(_,no_such_module:some_call(),true)),
862     {setup, fun() -> code:purge(to_remove),
863		      code:delete(to_remove),
864		      code:purge(to_remove),
865		      file:rename("tests/to_remove.beam",
866				  "tests/to_remove.bak") end,
867	     fun(_) -> file:rename("tests/to_remove.bak",
868				   "tests/to_remove.beam") end,
869	     ?_passes(?FORALL(_, to_remove:exp1(), true))},
870     ?_passes(rec_props_test1:prop_1()),
871     ?_passes(rec_props_test2:prop_2()),
872     ?_passes(?FORALL(L, vector(2,my_native_type()),
873		      length(L) =:= 2
874		      andalso lists:all(fun erlang:is_integer/1, L))),
875     ?_passes(?FORALL(F, function(0,my_native_type()), is_integer(F()))),
876     ?_passes(?FORALL(X, union([my_proper_type(),my_native_type()]),
877		      is_integer(X) orelse is_atom(X))),
878     ?_assertError(undef, begin
879			    Vector5 = fun(T) -> vector(5,T) end,
880			    ?FORALL(V, Vector5(types_test1:exp1()),
881				    length(V) =:= 5)
882			end),
883     ?_passes(?FORALL(X, ?SUCHTHAT(Y,types_test1:exp1(),is_atom(Y)),
884		      is_atom(X))),
885     ?_passes(?FORALL(L,non_empty(lof()),length(L) > 0)),
886     ?_passes(?FORALL(X, ?LET(L,lof(),lists:min([99999.9|L])),
887		      is_float(X))),
888     ?_shrinksTo(0, ?LETSHRINK([X],[my_native_type()],{'tag',X})),
889     {"Shrinking tuples",
890      [{"All elements are generators",
891        [?_shrinksTo({0,0}, proper_types:tuple([proper_types:integer(), proper_types:integer()])),
892         ?_shrinksTo({0,0}, {proper_types:integer(), proper_types:integer()})]},
893       {"Some elements are generators",
894        [?_shrinksTo({0,0}, proper_types:tuple([proper_types:integer(), 0])),
895         ?_shrinksTo({0,2}, proper_types:tuple([proper_types:integer(), 2])),
896         ?_shrinksTo({0,0}, {proper_types:integer(), 0}),
897         ?_shrinksTo({0,2}, {proper_types:integer(), 2})]},
898       {"All elements are consts",
899         [?_shrinksTo({3,2}, proper_types:tuple([3, 2])),
900          ?_shrinksTo({3,2}, {3, 2})]}]},
901     {"Shrinking fixed lists",
902      [{"All elements are generators",
903        [?_shrinksTo([0,0], proper_types:fixed_list([proper_types:integer(), proper_types:integer()])),
904         ?_shrinksTo([0,0], [proper_types:integer(), proper_types:integer()]),
905         ?_shrinksTo([0|0], [proper_types:integer()|proper_types:integer()])]},
906       {"Some elements are generators",
907        [?_shrinksTo([0,0], proper_types:fixed_list([proper_types:integer(), 0])),
908         ?_shrinksTo([0,2], proper_types:fixed_list([proper_types:integer(), 2])),
909         ?_shrinksTo([0|2], proper_types:fixed_list([proper_types:integer()|2])),
910         ?_shrinksTo([0,0], [proper_types:integer(), 0]),
911         ?_shrinksTo([0,2], [proper_types:integer(), 2]),
912         ?_shrinksTo([12,42], [12,42|list(integer())])]},
913       {"All elements are consts",
914         [?_shrinksTo([3|2], proper_types:fixed_list([3|2])),
915          ?_shrinksTo([3,2], proper_types:fixed_list([3, 2])),
916          ?_shrinksTo([3,2], [3, 2])]}]},
917     ?_passes(weird_types:prop_export_all_works()),
918     ?_passes(weird_types:prop_no_auto_import_works()),
919
920     ?_passes(?FORALL(B, utf8(), unicode:characters_to_binary(B) =:= B)),
921     ?_passes(?FORALL(B, utf8(1), length(unicode:characters_to_list(B)) =< 1)),
922     ?_passes(?FORALL(B, utf8(1, 1), size(B) =< 1)),
923     ?_passes(?FORALL(B, utf8(2, 1), size(B) =< 2)),
924     ?_passes(?FORALL(B, utf8(4), size(B) =< 16)),
925     ?_passes(?FORALL(B, utf8(),
926                      length(unicode:characters_to_list(B)) =< size(B)))
927    ].
928
929-type bin4()   :: <<_:32>>.
930-type bits42() :: <<_:42>>.
931-type bits5x() :: <<_:_*5>>.
932-type bits7x() :: <<_:_*7>>.
933
934-record(untyped, {a, b = 12}).
935-type untyped() :: #untyped{}.
936
937true_props_test_() ->
938    [?_passes(?FORALL(X,integer(),X < X + 1)),
939     ?_passes(?FORALL(A,atom(),list_to_atom(atom_to_list(A)) =:= A)),
940     ?_passes(?FORALL(B,bin4(),byte_size(B) =:= 4)),
941     ?_passes(?FORALL(B,bits42(),bit_size(B) =:= 42)),
942     ?_passes(?FORALL(B,bits5x(),bit_size(B) =/= 42)),
943     ?_passes(?FORALL(B,bits7x(),bit_size(B) rem 7 =:= 0)),
944     ?_passes(?FORALL(L,list(integer()),is_sorted(L,quicksort(L)))),
945     ?_passes(?FORALL(L,ulist(integer()),is_sorted(L,lists:usort(L)))),
946     ?_passes(?FORALL(L,non_empty(list(integer())),L =/= [])),
947     ?_passes(?FORALL({I,L}, {integer(),list(integer())},
948		      ?IMPLIES(no_duplicates(L),
949			       not lists:member(I,lists:delete(I,L))))),
950     ?_passes(?FORALL(L, ?SIZED(Size,resize(Size div 5,list(integer()))),
951		      length(L) =< 20), [{max_size,100}]),
952     %% TODO: check that the samples are collected correctly
953     ?_passes(?FORALL(L, list(integer()),
954		      collect(length(L), collect(L =:= [],
955			      lists:reverse(lists:reverse(L)) =:= L)))),
956     ?_passes(?FORALL(L, list(integer()),
957		      aggregate(smaller_lengths_than_my_own(L), true))),
958     ?_assertTempBecomesN(300, true,
959			  numtests(300,?FORALL(_,1,begin inc_temp(),true end))),
960     ?_assertTempBecomesN(30, true, ?FORALL(X, ?SIZED(Size,Size),
961					    begin inc_temp(X),true end),
962			  [{numtests,12},{max_size,4}]),
963     ?_assertTempBecomesN(12, true,
964			  ?FORALL(X, ?SIZED(Size,Size),
965				  begin inc_temp(X),true end),
966			  [{numtests,3},{start_size,4},{max_size,4}]),
967     ?_assertTempBecomesN(30, true,
968                          ?FORALL_TARGETED(X, ?USERNF(?SIZED(Size,Size),
969                                                      fun (_, _) -> ?SIZED(Size, Size) end),
970                                           begin inc_temp(X),true end),
971                          [{numtests,12},{max_size,4}]),
972     ?_assertTempBecomesN(12, true,
973                          ?FORALL_TARGETED(X, ?USERNF(?SIZED(Size,Size),
974                                                      fun (_, _) -> ?SIZED(Size, Size) end),
975                                           begin inc_temp(X),true end),
976                          [{numtests,3},{start_size,4},{max_size,4}]),
977     ?_passes(?FORALL(X, integer(), ?IMPLIES(abs(X) > 1, X * X > X))),
978     ?_passes(?FORALL(X, integer(), ?IMPLIES(X >= 0, true))),
979     ?_passes(?FORALL({X,Lim}, {int(),?SIZED(Size,Size)}, abs(X) =< Lim)),
980     ?_passes(?FORALL({X,Lim}, {nat(),?SIZED(Size,Size)}, X =< Lim)),
981     ?_passes(?FORALL(L, orderedlist(integer()), is_sorted(L))),
982     ?_passes(conjunction([
983		  {one, ?FORALL(_, integer(), true)},
984		  {two, ?FORALL(X, integer(), collect(X > 0, true))},
985		  {three, conjunction([{a,true},{b,true}])}
986	      ])),
987     ?_passes(?FORALL(X, untyped(), is_record(X, untyped))),
988     ?_passes(fun_tests:prop_fun_bool())].
989
990true_stateful_test_() ->
991    [?_passes(improper_lists_statem:prop_simple()),
992     ?_passes(symb_statem:prop_simple()),
993     ?_passes(symb_statem_maps:prop_simple()),
994     ?_passes(more_commands_test:prop_commands_passes(), [{numtests,42}]),
995     {timeout, 10, ?_passes(ets_statem_test:prop_ets())},
996     {timeout, 20, ?_passes(ets_statem_test:prop_parallel_ets())},
997     {timeout, 20, ?_passes(pdict_fsm:prop_pdict())},
998     {timeout, 20, ?_passes(symb_statem:prop_parallel_simple())},
999     {timeout, 20, ?_passes(symb_statem_maps:prop_parallel_simple())},
1000     {timeout, 42, ?_passes(targeted_statem:prop_random(), [{numtests,500}])},
1001     {timeout, 42, ?_passes(targeted_fsm:prop_random(), [{numtests,500}])}].
1002
1003false_props_test_() ->
1004    [?_failsWith([[Same,Same]],
1005		 ?FORALL(L,list(integer()),is_sorted(L,lists:usort(L)))),
1006     ?_failsWith([[Same2,Same2],Same2],
1007		 ?FORALL(L, non_empty(list(union([a,b,c,d]))),
1008			 ?FORALL(X, elements(L),
1009				 not lists:member(X,lists:delete(X,L))))),
1010     ?_failsWith(['\000\000\000\000'],
1011		 ?FORALL(A, atom(), length(atom_to_list(A)) < 4)),
1012     %% TODO: check that these only run once
1013     ?_failsWith([1], ?FORALL(X, non_neg_integer(),
1014			      case X > 0 of
1015				  true  -> throw(not_zero);
1016				  false -> true
1017			      end)),
1018     ?_fails(?FORALL(_, 1, lists:min([]) > 0)),
1019     ?_failsWith([[12,42]], ?FORALL(L, [12,42|list(integer())],
1020				    case lists:member(42, L) of
1021					true  -> erlang:exit(you_got_it);
1022					false -> true
1023				    end)),
1024     %% TODO: Check that the following two tests shrink properly on _N
1025     ?_cexmMatchesWith([{_,_N}], fun_tests:prop_fun_int_int()),
1026     ?_cexmMatchesWith([{_,_,[_N]}], fun_tests:prop_lists_map_filter()),
1027     ?_fails(?FORALL(_, integer(), ?TIMEOUT(100,timer:sleep(150) =:= ok))),
1028     ?_failsWith([20], ?FORALL(X, pos_integer(), ?TRAPEXIT(creator(X) =:= ok))),
1029     ?_assertTempBecomesN(7, false,
1030			  ?FORALL(X, ?SIZED(Size,integer(Size,Size)),
1031				  begin inc_temp(), X < 5 end),
1032			  [{numtests,5}, {max_size,5}]),
1033     %% it runs 2 more times: one while shrinking (recursing into the property)
1034     %% and one when the minimal input is rechecked
1035     ?_assertTempBecomesN(2, false,
1036			  ?FORALL(L, list(atom()),
1037				  ?WHENFAIL(inc_temp(), length(L) < 5))),
1038     ?_assertTempBecomesN(3, false,
1039			  ?FORALL(S, ?SIZED(Size,Size),
1040				  begin inc_temp(), S =< 20 end),
1041			  [{numtests,3},{max_size,40},noshrink]),
1042     ?_failsWithOneOf([[{true,false}],[{false,true}]],
1043		      ?FORALL({B1,B2}, {boolean(),boolean()}, equals(B1,B2))),
1044     ?_failsWith([2,1],
1045		 ?FORALL(X, integer(1,10), ?FORALL(Y, integer(1,10), X =< Y))),
1046     ?_failsWith([1,2],
1047		 ?FORALL(Y, integer(1,10), ?FORALL(X, integer(1,10), X =< Y))),
1048     ?_failsWithOneOf([[[0,1]],[[0,-1]],[[1,0]],[[-1,0]]],
1049		      ?FORALL(L, list(integer()), lists:reverse(L) =:= L)),
1050     ?_failsWith([[1,2,3,4,5,6,7,8,9,10]],
1051		 ?FORALL(_L, shuffle(lists:seq(1,10)), false)),
1052     %% TODO: check that these don't shrink
1053     ?_fails(?FORALL(_, integer(0,0), false)),
1054     ?_fails(?FORALL(_, float(0.0,0.0), false)),
1055     ?_fails(fails(?FORALL(_, integer(), false))),
1056     ?_failsWith([16], ?FORALL(X, ?LET(Y,integer(),Y*Y), X < 15)),
1057     ?_failsWith([0.0],
1058		 ?FORALL(_, ?LETSHRINK([A,B], [float(),atom()], {A,B}), false)),
1059     ?_failsWith([], conjunction([{some,true},{thing,false}])),
1060     ?_failsWith([{2,1},[{group,[[{sub_group,[1]}]]},{stupid,[1]}]],
1061	 ?FORALL({X,Y}, {pos_integer(),pos_integer()},
1062		 conjunction([
1063		     {add_next, ?IMPLIES(X > Y, X + 1 > Y)},
1064		     {symmetry,
1065			 conjunction([
1066			     {add_sym, collect(X+Y, X+Y =:= Y+X)},
1067			     {sub_sym,
1068			      ?WHENFAIL(io:format("'-' isn't symmetric!~n",[]),
1069					X-Y =:= Y-X)}
1070			 ])},
1071		     {group,
1072		      conjunction([
1073			  {add_group,
1074			   ?WHENFAIL(io:format("This shouldn't happen!~n",[]),
1075				     ?FORALL(Z, pos_integer(),
1076					     (X+Y)+Z =:= X+(Y+Z)))},
1077			  {sub_group,
1078			   ?WHENFAIL(io:format("'-' doesn't group!~n",[]),
1079				     ?FORALL(W, pos_integer(),
1080					     (X-Y)-W =:= X-(Y-W)))}
1081		      ])},
1082		     {stupid, ?FORALL(_, pos_integer(), throw(woot))}
1083		 ]))),
1084     ?_failsWith([[a,a,a,a,a]], shrinking_gotchas:prop_shrink_list_same_elem()),
1085     ?_fails(more_commands_test:prop_more_commands_fails(), [{numtests,42}]),
1086     ?_failsWith([500], targeted_shrinking_test:prop_int()),
1087     ?_failsWith([500], targeted_shrinking_test:prop_let_int()),
1088     ?_failsWith([500], targeted_shrinking_test:prop_int_shrink_outer()),
1089     ?_failsWith([500], targeted_shrinking_test:prop_int_shrink_inner()),
1090     {timeout, 20, ?_fails(ets_counter:prop_ets_counter())},
1091     ?_fails(post_false:prop_simple())].
1092
1093false_stateful_test_() ->
1094  Opts = [{numtests,1000}],
1095  [{timeout, 42, ?_fails(targeted_statem:prop_targeted(), Opts)},
1096   {timeout, 42, ?_fails(targeted_statem:prop_targeted_init(), Opts)},
1097   {timeout, 42, ?_fails(targeted_fsm:prop_targeted(), Opts)},
1098   {timeout, 42, ?_fails(targeted_fsm:prop_targeted_init(), Opts)}].
1099
1100exception_props_test_() ->
1101     [?_fails(error_statem:prop_simple())].
1102
1103error_props_test_() ->
1104    [?_errorsOut({cant_generate,[{?MODULE,error_props_test_,0}]},
1105		 ?FORALL(_, ?SUCHTHAT(X, pos_integer(), X =< 0), true)),
1106     ?_errorsOut(cant_satisfy,
1107		 ?FORALL(X, pos_integer(), ?IMPLIES(X =< 0, true))),
1108     ?_errorsOut(type_mismatch,
1109		 ?FORALL({X,Y}, [integer(),integer()], X < Y)),
1110     ?_assertCheck({error,rejected}, [2],
1111		   ?FORALL(X, integer(), ?IMPLIES(X > 5, X < 6))),
1112     ?_assertCheck({error,too_many_instances}, [1,ab],
1113		   ?FORALL(X, pos_integer(), X < 0)),
1114     ?_errorsOut({cant_generate,[{proper_statem,commands_gen,4}]},
1115		 prec_false:prop_simple()),
1116     ?_errorsOut({cant_generate,[{nogen_statem,impossible_arg,0}]},
1117		 nogen_statem:prop_simple()),
1118     ?_errorsOut(non_boolean_result, ?FORALL(_, integer(), not_a_boolean)),
1119     ?_errorsOut(non_boolean_result,
1120		 ?FORALL(_, ?SHRINK(42,[0]),
1121			 non_deterministic([{2,false},{1,not_a_boolean}]))),
1122     ?_assertRun(false,
1123		 ?FORALL(_, ?SHRINK(42,[0]),
1124			 non_deterministic([{4,false},{1,true}])),
1125		 [], false),
1126     ?_assertRun(false,
1127		 ?FORALL(_, ?SHRINK(42,[0]),
1128			 non_deterministic([{3,false},{1,true},{1,false}])),
1129		 [], false),
1130     ?_assertRun(false,
1131		 ?FORALL(_, ?LAZY(non_deterministic([{1,1},{1,2},{1,3},{1,4}])),
1132			 false), [], false)].
1133
1134eval_test_() ->
1135    [?_assertEqual(Result, eval(Vars,SymbCall))
1136     || {Result,_Repr,Vars,SymbCall} <- symb_calls()].
1137
1138pretty_print_test_() ->
1139    [?_assert(equal_ignoring_ws(Repr, proper_symb:pretty_print(Vars,SymbCall)))
1140     || {_Result,Repr,Vars,SymbCall} <- symb_calls()].
1141
1142not_defined_test_() ->
1143    [?_assertNot(defined(SymbCall))
1144     || SymbCall <- undefined_symb_calls()].
1145
1146options_test_() ->
1147    [?_assertEqual({error,{erroneous_option,{numtests,0}}},
1148		   proper:module(command_props, [{numtests,0}])),
1149     ?_assertEqual({error,{unrecognized_option,gazonk}},
1150		   proper:quickcheck(rec_props_test1:prop_1(), [42,gazonk])),
1151     ?_assertTempBecomesN(300, true,
1152			  ?FORALL(_, 1, begin inc_temp(), true end),
1153			  [{numtests,300}]),
1154     ?_assertTempBecomesN(300, true,
1155			  ?FORALL(_, 1, begin inc_temp(), true end),
1156			  [300]),
1157     ?_failsWith([42], ?FORALL(T, any(), T < 42),
1158		 [any_to_integer,verbose,nocolors]),
1159     ?_failsWith([42], ?FORALL(I, integer(), I < 42),
1160		 [{numtests,4711}, {on_output,fun print_in_magenta/2}]),
1161     ?_failsWith([42], ?FORALL(_, ?SHRINK(42,[0,1]), false), [noshrink]),
1162     ?_failsWith([42], ?FORALL(_, ?SHRINK(42,[0,1]), false), [{max_shrinks,0}]),
1163     ?_fails(?FORALL(_, integer(), false), [fails]),
1164     ?_assertRun({error,{cant_generate,[{?MODULE,options_test_,0}]}},
1165		 ?FORALL(_, ?SUCHTHAT(X, pos_integer(), X > 42), true),
1166		 [{constraint_tries,1}], true),
1167     ?_failsWith([12],
1168		 ?FORALL(_, ?SIZED(Size, integer(Size, Size)), false),
1169		 [{start_size,12}])].
1170
1171print_in_magenta(S, L) ->
1172   io:format("\033[1;35m"++S++"\033[0m", L).
1173
1174setup_prop() ->
1175    ?SETUP(fun () ->
1176		   put(setup_token, true),
1177		   fun () ->
1178			   erase(setup_token),
1179			   ok
1180		   end
1181	   end,
1182	   ?FORALL(_, exactly(ok), get(setup_token))).
1183
1184failing_setup_prop() ->
1185    ?SETUP(fun () ->
1186		   put(setup_token, true),
1187		   fun () ->
1188			   erase(setup_token),
1189			   ok
1190		   end
1191	   end,
1192	   ?FORALL(_, exactly(ok), not get(setup_token))).
1193
1194double_setup_prop() ->
1195    ?SETUP(fun () ->
1196		   put(setup_token2, true),
1197		   fun () ->
1198			   erase(setup_token2),
1199			   ok
1200		   end
1201	   end,
1202	   ?SETUP(fun () ->
1203			  put(setup_token, true),
1204			  fun () ->
1205				  erase(setup_token),
1206				  ok
1207			  end
1208		  end,
1209		  ?FORALL(_, exactly(ok),
1210			  get(setup_token) andalso get(setup_token2)))).
1211
1212setup_test_() ->
1213    [?_passes(setup_prop(), [10]),
1214     ?_assert(proper:quickcheck(setup_prop(), 10)
1215	      andalso undefined =:= get(setup_token)),
1216     ?_fails(failing_setup_prop(), [10]),
1217     ?_assert(not proper:quickcheck(failing_setup_prop(), [10, noshrink, quiet])
1218	      andalso undefined =:= get(setup_token)),
1219     ?_assert(proper:check(setup_prop(), [ok], 10)),
1220     ?_assert(proper:check(setup_prop(), [ok], 10)
1221	      andalso undefined =:= get(setup_token)),
1222     ?_assert(not proper:check(failing_setup_prop(), [ok], 10)),
1223     ?_assert(not proper:check(failing_setup_prop(), [ok], 10)
1224	      andalso undefined =:= get(setup_token)),
1225     ?_passes(double_setup_prop(), [10]),
1226     ?_assert(proper:quickcheck(double_setup_prop(), 10)
1227	      andalso undefined =:= get(setup_token)
1228	      andalso undefined =:= get(setup_token2)),
1229     ?_assert(proper:check(double_setup_prop(), [ok], 10)),
1230     ?_assert(true = proper:check(double_setup_prop(), [ok], 10)
1231	      andalso undefined =:= get(setup_token)
1232	      andalso undefined =:= get(setup_token2))].
1233
1234adts1_test_() ->
1235    {timeout, 60,	% for Kostis' old laptop
1236      ?_passes(?FORALL({X,S},{integer(),sets:set(integer())},
1237		       sets:is_element(X,sets:add_element(X,S))), [20])}.
1238
1239adts2_test_() ->
1240    {timeout, 60,	% for 18.x (and onwards?)
1241     ?_passes(?FORALL({X,Y,D},
1242		      {integer(),float(),dict:dict(integer(),float())},
1243		      dict:fetch(X,dict:store(X,Y,eval(D))) =:= Y), [30])}.
1244
1245adts3_test_() ->
1246     {timeout, 60,
1247      ?_fails(?FORALL({X,D},
1248	      {boolean(),dict:dict(boolean(),integer())},
1249	      dict:erase(X, dict:store(X,42,D)) =:= D))}.
1250
1251parameter_test_() ->
1252    ?_passes(?FORALL(List, [zero1(),zero2(),zero3(),zero4()],
1253		     begin
1254			 [?assertEqual(undefined, proper_types:parameter(P))
1255			  || P <- [x1,x2,y2,x3,y3,x4,y4,v,w,z]],
1256			 lists:all(fun is_zero/1, List)
1257		     end)).
1258
1259parameter_targeted_test_() ->
1260  BaseType = ?LAZY(proper_types:parameter(param)),
1261  UserNF = ?USERNF(BaseType, fun (_, _) -> BaseType end),
1262  Type = proper_types:with_parameter(param, 1, UserNF),
1263  ?_passes(?FORALL_TARGETED(X, Type, X =:= 1)).
1264
1265zip_test_() ->
1266    [?_assertEqual(proper_statem:zip(X, Y), Expected)
1267     || {X,Y,Expected} <- lists_to_zip()].
1268
1269command_names_test_() ->
1270    [?_assertEqual(proper_statem:command_names(Cmds), Expected)
1271     || {Cmds,Expected} <- command_names()].
1272
1273command_names_parallel1_test_() ->
1274    [?_assertEqual(proper_statem:command_names({Cmds,[]}), Expected)
1275     || {Cmds,Expected} <- command_names()].
1276
1277command_names_parallel2_test_() ->
1278    [?_assertEqual(proper_statem:command_names({[],[Cmds]}), Expected)
1279     || {Cmds,Expected} <- command_names()].
1280
1281command_names_parallel3_test_() ->
1282    [?_assertEqual(proper_statem:command_names({Cmds,[Cmds]}), Expected++Expected)
1283     || {Cmds,Expected} <- command_names()].
1284
1285command_names_parallel4_test_() ->
1286    [?_assertEqual(proper_statem:command_names({Cmds,[Cmds,Cmds]}), Expected++Expected++Expected)
1287     || {Cmds,Expected} <- command_names()].
1288
1289valid_cmds_test_() ->
1290    [?_assert(proper_statem:is_valid(Mod, State, Cmds, Env))
1291     || {Mod,State,Cmds,_,_,Env} <- valid_command_sequences()].
1292
1293invalid_cmds_test_() ->
1294    [?_assertNot(proper_statem:is_valid(Mod, Mod:initial_state(), Cmds, []))
1295     || {Mod,Cmds,_,_} <- invalid_precondition()] ++
1296    [?_assertNot(proper_statem:is_valid(Mod, Mod:initial_state(), Cmds, []))
1297     || {Mod,Cmds} <- invalid_var()].
1298
1299state_after_test_() ->
1300    [?_assertEqual(proper_statem:state_after(Mod, Cmds), StateAfter)
1301     || {Mod,_,Cmds,StateAfter,_,_} <- valid_command_sequences()].
1302
1303cannot_generate_commands_test_() ->
1304    [?_test(assert_cant_generate_cmds(proper_statem:commands(Mod), 6))
1305     || Mod <- [prec_false]].
1306
1307can_generate_commands0_test_() ->
1308    [?_test(assert_can_generate(proper_statem:commands(Mod), false))
1309     || Mod <- [pdict_statem]].
1310
1311can_generate_commands1_test_() ->
1312    [?_test(assert_can_generate(proper_statem:commands(Mod, StartState), false))
1313     || {Mod,StartState} <- [{pdict_statem,[{a,1},{b,1},{c,100}]}]].
1314
1315can_generate_parallel_commands0_test_() ->
1316    {timeout, 20,
1317     [?_test(assert_can_generate(proper_statem:parallel_commands(Mod), false))
1318      || Mod <- [ets_counter]]}.
1319
1320can_generate_parallel_commands1_test_() ->
1321    {timeout, 20,
1322     [?_test(assert_can_generate(
1323	       proper_statem:parallel_commands(Mod, Mod:initial_state()),
1324	       false))
1325      || Mod <- [ets_counter]]}.
1326
1327seeded_runs_return_same_result_test_() ->
1328    [?_test(assert_seeded_runs_return_same_result(proper_statem:commands(Mod)))
1329     || Mod <- [pdict_statem]].
1330
1331run_valid_commands_test_() ->
1332    [?_assertMatch({_H,DynState,ok}, setup_run_commands(Mod, Cmds, Env))
1333     || {Mod,_,Cmds,_,DynState,Env} <- valid_command_sequences()].
1334
1335run_init_error_test_() ->
1336    [?_assertMatch({_H,_S,initialization_error},
1337		   setup_run_commands(Mod, Cmds, Env))
1338     || {Mod,Cmds,Env,_Shrunk} <- symbolic_init_invalid_sequences()].
1339
1340run_precondition_false_test_() ->
1341    [?_assertMatch({_H,_S,{precondition,false}},
1342		   setup_run_commands(Mod, Cmds, Env))
1343     || {Mod,Cmds,Env,_Shrunk} <- invalid_precondition()].
1344
1345run_postcondition_false_test_() ->
1346    Mod = post_false,
1347    Cmds = [{set,{var,1},{call,Mod,foo,[]}},
1348	    {set,{var,2},{call,Mod,bar,[]}},
1349	    {set,{var,3},{call,Mod,foo,[]}},
1350	    {set,{var,4},{call,Mod,bar,[]}},
1351	    {set,{var,5},{call,Mod,bar,[]}},
1352	    {set,{var,6},{call,Mod,foo,[]}}],
1353    State = {state,5}, PostF = {postcondition,false},
1354    [?_assertMatch({_H1,State,PostF}, run_commands(Mod, Cmds))].
1355
1356run_statem_exceptions_test_() ->
1357    Mod = error_statem,
1358    Cmds = [{set,{var,1},{call,Mod,foo,[42]}}],
1359    State = {state,0},
1360    [?_assertMatch({_H,State,{exception,throw,badarg,_}},
1361		   run_commands(Mod, Cmds))].
1362
1363get_next_test_() ->
1364    [?_assertEqual(Expected,
1365		   proper_statem:get_next(L, Len, MaxIndex, Available, W, N))
1366     || {L, Len, MaxIndex, Available, W, N, Expected} <- combinations()].
1367
1368mk_first_comb_test_() ->
1369    [?_assertEqual(Expected, proper_statem:mk_first_comb(N, Len, W))
1370     || {N, Len, W, Expected} <- first_comb()].
1371
1372args_not_defined_test() ->
1373    [?_assertNot(proper_statem:args_defined(Args, SymbEnv))
1374     || {Args, SymbEnv} <- arguments_not_defined()].
1375
1376command_props_test_() ->
1377    {timeout, 150, [?_assertEqual([], proper:module(command_props))]}.
1378
1379%% TODO: is_instance check fails because of ?LET in fsm_commands/1?
1380can_generate_fsm_commands_test_() ->
1381    [?_test(assert_can_generate(proper_fsm:commands(Mod), false))
1382     || Mod <- [pdict_fsm, numbers_fsm]].
1383
1384transition_target_test_() ->
1385    {timeout, 20, [?_assertEqual([], proper:module(numbers_fsm))]}.
1386
1387dollar_only_cp_test_() ->
1388    ?_assertEqual(
1389       dollar_data(),
1390       [K || K <- all_data(),
1391	     is_atom(K),
1392	     re:run(atom_to_list(K), ["^[$]"], [{capture,none}]) =:= match]).
1393
1394sampleshrink_test_() ->
1395    Gen = non_empty(?LET({N,Lst}, {range(0,5),list(a)}, lists:sublist(Lst, N))),
1396    [{"Test type with restrain",
1397      [{"Try another way to call shrinking (not sampleshrink)",
1398        ?_shrinksTo([a], Gen)},
1399       ?_test(proper_gen:sampleshrink(Gen))]}].
1400
1401
1402%%------------------------------------------------------------------------------
1403%% Performance tests
1404%%------------------------------------------------------------------------------
1405
1406max_size_test() ->
1407    %% issue a call to load the test module and ensure that the test exists
1408    ?assert(lists:member({prop_identity,0},
1409			 perf_max_size:module_info(exports))),
1410    %% run some tests with a small and a big max_size option
1411    {Ts,true} = timer:tc(fun() -> max_size_test_aux(42) end),
1412    {Tb,true} = timer:tc(fun() -> max_size_test_aux(16#ffffffff) end),
1413    %% ensure that the test with the big max_size option does not take
1414    %% much longer than the small one to complete
1415    ?assert(2*Ts >= Tb).
1416
1417max_size_test_aux(Size) ->
1418    proper:quickcheck(perf_max_size:prop_identity(), [5,{max_size,Size}]).
1419
1420
1421%%------------------------------------------------------------------------------
1422%% Erlang abstract code tests
1423%%------------------------------------------------------------------------------
1424
1425erlang_abstract_code_test_() ->
1426    M = erlang_abstract_code_test,
1427    Props = [bits, expr, guard, term, module],
1428    Opts = [{numtests, 200}, noshrink],
1429    {timeout, 42,
1430     [?_assertEqual(true, proper:quickcheck(M:Prop(), Opts)) || Prop <- Props]}.
1431
1432%%------------------------------------------------------------------------------
1433%% Helper predicates
1434%%------------------------------------------------------------------------------
1435
1436no_duplicates(L) ->
1437    length(lists:usort(L)) =:= length(L).
1438
1439is_sorted([]) -> true;
1440is_sorted([_]) -> true;
1441is_sorted([A | [B|_] = T]) when A =< B -> is_sorted(T);
1442is_sorted(_) -> false.
1443
1444same_elements(L1, L2) ->
1445    length(L1) =:= length(L2) andalso same_elems(L1, L2).
1446
1447same_elems([], []) ->
1448    true;
1449same_elems([H|T], L) ->
1450    lists:member(H, L) andalso same_elems(T, lists:delete(H, L));
1451same_elems(_, _) ->
1452    false.
1453
1454is_sorted(Old, New) ->
1455    same_elements(Old, New) andalso is_sorted(New).
1456
1457equal_ignoring_ws(Str1, Str2) ->
1458    WhiteSpace = [32,9,10],
1459    equal_ignoring_chars(Str1, Str2, WhiteSpace).
1460
1461equal_ignoring_chars([], [], _Ignore) ->
1462    true;
1463equal_ignoring_chars([Ch1|Rest1], [Ch2|Rest2], Ignore) when Ch1 =:= Ch2 ->
1464    equal_ignoring_chars(Rest1, Rest2, Ignore);
1465equal_ignoring_chars([Ch1|Rest1] = Str1, [Ch2|Rest2] = Str2, Ignore) ->
1466    case lists:member(Ch1, Ignore) of
1467	true ->
1468	    equal_ignoring_chars(Rest1, Str2, Ignore);
1469	false ->
1470	    case lists:member(Ch2, Ignore) of
1471		true ->
1472		    equal_ignoring_chars(Str1, Rest2, Ignore);
1473		false ->
1474		    false
1475	    end
1476    end.
1477
1478smaller_lengths_than_my_own(L) ->
1479    lists:seq(0, length(L)).
1480
1481is_zero(X) -> X =:= 0.
1482
1483
1484%%------------------------------------------------------------------------------
1485%% Functions to test
1486%%------------------------------------------------------------------------------
1487
1488partition(Pivot, List) ->
1489    partition_tr(Pivot, List, [], []).
1490
1491partition_tr(_Pivot, [], Lower, Higher) ->
1492    {Lower, Higher};
1493partition_tr(Pivot, [H|T], Lower, Higher) ->
1494    case H =< Pivot of
1495	true  -> partition_tr(Pivot, T, [H|Lower], Higher);
1496	false -> partition_tr(Pivot, T, Lower, [H|Higher])
1497    end.
1498
1499quicksort([]) -> [];
1500quicksort([H|T]) ->
1501    {Lower, Higher} = partition(H, T),
1502    quicksort(Lower) ++ [H] ++ quicksort(Higher).
1503
1504creator(X) ->
1505    Self = self(),
1506    spawn_link(fun() -> destroyer(X,Self) end),
1507    receive
1508	_ -> ok
1509    end.
1510
1511destroyer(X, Father) ->
1512    case X < 20 of
1513	true  -> Father ! not_yet;
1514	false -> exit(this_is_the_end)
1515    end.
1516
1517
1518%%------------------------------------------------------------------------------
1519%% Datatypes to test
1520%%------------------------------------------------------------------------------
1521
1522%% TODO: remove this if you make 'shuffle' a default constructor
1523shuffle([]) ->
1524    [];
1525shuffle(L) ->
1526    ?LET(X, elements(L), [X | shuffle(lists:delete(X,L))]).
1527
1528ulist(ElemType) ->
1529    ?LET(L, list(ElemType), L--(L--lists:usort(L))).
1530
1531zerostream(ExpectedMeanLen) ->
1532    ?LAZY(frequency([
1533	{1, []},
1534	{ExpectedMeanLen, [0 | zerostream(ExpectedMeanLen)]}
1535    ])).
1536
1537-type my_native_type() :: integer().
1538my_proper_type() -> atom().
1539-type type_and_fun() :: integer().
1540type_and_fun() -> atom().
1541-type type_only() :: integer().
1542-type id(X) :: X.
1543-type lof() :: [float()].
1544
1545-type deeplist() :: [deeplist()].
1546
1547deeplist() ->
1548    ?SIZED(Size, deeplist(Size)).
1549
1550deeplist(0) ->
1551    [];
1552deeplist(Size) ->
1553    ?LAZY(proper_types:distlist(Size, fun deeplist/1, false)).
1554
1555-type tree(T) :: 'null' | {'node',T,tree(T),tree(T)}.
1556
1557tree(ElemType) ->
1558    ?SIZED(Size, tree(ElemType,Size)).
1559
1560tree(_ElemType, 0) ->
1561    null;
1562tree(ElemType, Size) ->
1563    LeftTree = tree(ElemType, Size div 2),
1564    RightTree = tree(ElemType, Size div 2),
1565    frequency([
1566	{1, tree(ElemType,0)},
1567	{5, ?LETSHRINK([L,R], [LeftTree,RightTree], {node,ElemType,L,R})}
1568    ]).
1569
1570-type a() :: 'aleaf' | {'anode',a(),b()}.
1571-type b() :: 'bleaf' | {'bnode',a(),b()}.
1572
1573a() ->
1574    ?SIZED(Size, a(Size)).
1575
1576a(0) ->
1577    aleaf;
1578a(Size) ->
1579    union([
1580	?LAZY(a(0)),
1581	?LAZY(?LETSHRINK([A], [a(Size div 2)], {anode,A,b(Size)}))
1582    ]).
1583
1584b() ->
1585    ?SIZED(Size, b(Size)).
1586
1587b(0) ->
1588    bleaf;
1589b(Size) ->
1590    union([
1591	?LAZY(b(0)),
1592	?LAZY(?LETSHRINK([B], [b(Size div 2)], {bnode,a(Size),B}))
1593    ]).
1594
1595-type gen_tree(T) :: 'null' | {T,[gen_tree(T),...]}.
1596
1597gen_tree(ElemType) ->
1598    ?SIZED(Size, gen_tree(ElemType,Size)).
1599
1600gen_tree(_ElemType, 0) ->
1601    null;
1602gen_tree(ElemType, Size) ->
1603    SubGen = fun(S) -> gen_tree(ElemType,S) end,
1604    oneof([
1605	?LAZY(gen_tree(ElemType,0)),
1606	?LAZY(?LETSHRINK(Children, proper_types:distlist(Size, SubGen, true),
1607			 {ElemType,Children}))
1608    ]).
1609
1610-type g() :: 'null' | {'tag',[g()]}.
1611-type h() :: 'null' | {'tag',[{'ok',h()}]}.
1612-type i() :: 'null' | {'tag',i(),[i()]}.
1613-type j() :: 'null' | {'one',j()} | {'tag',j(),j(),[j()],[j()]}.
1614-type k() :: 'null' | {'tag',[{k(),k()}]}.
1615-type l() :: 'null' | {'tag',l(),[l(),...]}.
1616
1617zero1() ->
1618    proper_types:with_parameter(
1619      x1, 0, ?SUCHTHAT(I, range(-1, 1), I =:= proper_types:parameter(x1))).
1620
1621zero2() ->
1622    proper_types:with_parameters(
1623      [{x2,41}],
1624      ?LET(X,
1625	   proper_types:with_parameter(
1626	     y2, 43,
1627	     ?SUCHTHAT(
1628		I, range(41, 43),
1629		I > proper_types:parameter(x2)
1630		andalso I < proper_types:parameter(y2))),
1631	   X - 42)).
1632
1633zero3() ->
1634    ?SUCHTHAT(I, range(-1, 1),
1635	      I > proper_types:parameter(x3, -1)
1636	      andalso I < proper_types:parameter(y3, 1)).
1637
1638zero4() ->
1639    proper_types:with_parameters(
1640      [{x4,-2}, {y4,2}],
1641      proper_types:with_parameters(
1642	[{x4,-1}, {y4,1}],
1643	?SUCHTHAT(I, range(-1, 1),
1644		  I > proper_types:parameter(x4)
1645		  andalso I < proper_types:parameter(y4)))).
1646
1647
1648%%------------------------------------------------------------------------------
1649%% Old Tests and datatypes
1650%%------------------------------------------------------------------------------
1651
1652% nelist(ElemType) ->
1653%     [ElemType | list(ElemType)].
1654%
1655% uvector(0, _ElemType) ->
1656%    [];
1657% uvector(N, ElemType) ->
1658%     ?LET(Rest,
1659% 	 uvector(N-1, ElemType),
1660% 	 ?LET(Elem,
1661% 	      ?SUCHTHAT(E, ElemType, not lists:member(E,Rest)),
1662% 	      [Elem | Rest])).
1663%
1664% subset(Generators) ->
1665%     ?LET(Keep,
1666% 	 [{boolean(),G} || G <- Generators],
1667% 	 [G || {true,G} <- Keep]).
1668%
1669% unique(ElemTypes) ->
1670%     ?LET(Values,
1671% 	 list(ElemTypes),
1672% 	 lists:usort(Values)).
1673%
1674% ulist2(ElemType) ->
1675%     ?SUCHTHAT(L, list(ElemType), no_duplicates(L)).
1676%
1677% kvlist(KeyType, ValueType) ->
1678%     ?LET(Keys,
1679% 	 list(KeyType),
1680% 	 [{K,ValueType} || K <- Keys]).
1681%
1682% tree_member(_X, {node,_X,_L,_R}) -> true;
1683% tree_member(X, {node,_Y,L,R}) -> tree_member(X, L) orelse tree_member(X, R);
1684% tree_member(_X, {empty}) -> false.
1685%
1686% symbdict(KeyType, ValueType) ->
1687%     ?SIZED(Size, symbdict(Size, KeyType, ValueType)).
1688%
1689% symbdict(0, _KeyType, _ValueType) ->
1690%     {call,dict,new,[]};
1691% symbdict(Size, KeyType, ValueType) ->
1692%     ?LAZY(
1693% 	frequency([
1694% 	    {1,symbdict(0, KeyType, ValueType)},
1695% 	    {4,?LETSHRINK([Smaller], [symbdict(Size - 1, KeyType, ValueType)],
1696% 			  {call, dict, append,[KeyType,ValueType,Smaller]})}
1697% 	])
1698%     ).
1699%
1700% test(15) ->
1701%     ?FORALL(T,
1702% 	    ?LET(L,
1703% 		 non_empty(list(integer())),
1704% 		 ?LET(Y,
1705% 		      elements(L),
1706% 		      {Y,L})),
1707% 	    erlang:element(1,T) =/= 42);
1708% test(18) ->
1709%     ?FORALL(L, kvlist(atom(),integer()), not lists:keymember(42,2,L));
1710% test(19) ->
1711%     ?FORALL(T, tree(integer()), not tree_member(42, T));
1712% test(20) ->
1713%     ?FORALL(X,
1714% 	    ?LET(L, non_empty(list(integer())), list(oneof(L))),
1715% 	    length(X) < 10);
1716% test(27) ->
1717%     ?FORALL(SD,
1718% 	    symbdict(integer(),integer()),
1719% 	    not dict:is_key(42, eval(SD)));
1720% test(29) ->
1721%     ?FORALL({F,L},
1722% 	    {function(1,integer(1,100)), list(integer())},
1723% 	    lists:all(fun(X) -> F(X) =/= 42 end, L));
1724% correct_smaller_length_aggregation(Tests, SmallerLens) ->
1725%     {Zeros,Larger} = lists:partition(fun(X) -> X =:= 0 end, SmallerLens),
1726%     length(Zeros) =:= Tests
1727%     andalso correct_smaller_length_aggregation(Tests, Larger, 1).
1728%
1729% correct_smaller_length_aggregation(0, SmallerLens, _Len) ->
1730%     SmallerLens =:= [];
1731% correct_smaller_length_aggregation(NotMoreThan, SmallerLens, Len) ->
1732%     {Lens,Larger} = lists:partition(fun(X) -> X =:= Len end, SmallerLens),
1733%     Num = length(Lens),
1734%     Num =< NotMoreThan
1735%     andalso correct_smaller_length_aggregation(Num, Larger, Len+1).
1736