1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
%%% Copyright 2010-2016 Manolis Papadakis <manopapad@gmail.com>,
%%% Eirini Arvaniti <eirinibob@gmail.com>
%%% and Kostis Sagonas <kostis@cs.ntua.gr>
%%%
%%% This file is part of PropEr.
%%%
%%% PropEr is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU General Public License as published by
%%% the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% PropEr is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%%% GNU General Public License for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>.
%%% @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @author Eirini Arvaniti
-module(command_props).
-include_lib("proper/include/proper.hrl").
-define(MOD, ets_counter).
-define(MOD1, pdict_statem).
ne_nd_list(ElemType) ->
?LET(L, non_empty(list(ElemType)), lists:usort(L)).
short_ne_nd_list(ElemType) ->
?LET(L, resize(8, non_empty(list(ElemType))), lists:usort(L)).
no_duplicates(L) ->
length(L) =:= length(lists:usort(L)).
prop_index() ->
?FORALL(List, ne_nd_list(integer()),
?FORALL(X, union(List),
lists:nth(proper_statem:index(X, List), List) =:= X)).
prop_all_insertions() ->
?FORALL(List, list(integer()),
begin
Len = length(List),
?FORALL(Limit, range(1,Len+1),
?FORALL(X, integer(),
begin
AllIns = proper_statem:all_insertions(X, Limit, List),
length(AllIns) =:= Limit
end))
end).
prop_insert_all() ->
?FORALL(List, short_ne_nd_list(integer()),
begin
Len = length(List),
{L1, L2} = lists:split(Len div 2, List),
AllIns = proper_statem:insert_all(L1, L2),
?WHENFAIL(io:format("~nList: ~w, L1: ~w, L2: ~w~nAllIns: ~w~n",
[List,L1,L2,AllIns]),
lists:all(fun(L) ->
length(L) =:= Len andalso
no_duplicates(L) andalso
lists:subtract(L,L2) =:= L1
end, AllIns))
end).
prop_zip() ->
?FORALL({X, Y}, {list(), list()},
begin
LenX = length(X),
LenY = length(Y),
Res = if LenX < LenY ->
lists:zip(X, lists:sublist(Y, LenX));
LenX =:= LenY ->
lists:zip(X, Y);
LenX > LenY ->
lists:zip(lists:sublist(X, LenY), Y)
end,
equals(zip(X, Y), Res)
end).
prop_state_after() ->
?FORALL(Cmds, proper_statem:commands(?MOD1),
begin
SymbState = proper_statem:state_after(?MOD1, Cmds),
{_, S, ok} = proper_statem:run_commands(?MOD1, Cmds),
?MOD1:clean_up(),
equals(proper_symb:eval(SymbState), S)
end).
prop_parallel_ets_counter() ->
?FORALL({_Seq, [P1, P2]}, proper_statem:parallel_commands(?MOD),
begin
Len1 = length(P1),
Len2 = length(P2),
Len1 =:= Len2 orelse (Len1 + 1) =:= Len2
end).
prop_check_true() ->
?FORALL({Seq, Par}, proper_statem:parallel_commands(?MOD),
begin
?MOD:clean_up(),
?MOD:set_up(),
{{_, State, ok}, Env} = proper_statem:run(?MOD, Seq, []),
Res = [proper_statem:execute(C, Env, ?MOD) || C <- Par],
V = proper_statem:check(?MOD, State, Env, false, [], Res),
equals(V, true)
end).
|
