Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 689 lines (590 sloc) 23.76 kb
6d826f9 Manolis Papadakis Fix copyright notices
authored
1 %%% Copyright 2010-2011 Manolis Papadakis <manopapad@gmail.com>,
2 %%% Eirini Arvaniti <eirinibob@gmail.com>
3 %%% and Kostis Sagonas <kostis@cs.ntua.gr>
78c6b91 Manolis Papadakis added Mastermind usage example
authored
4 %%%
5 %%% This file is part of PropEr.
6 %%%
7 %%% PropEr is free software: you can redistribute it and/or modify
8 %%% it under the terms of the GNU General Public License as published by
9 %%% the Free Software Foundation, either version 3 of the License, or
10 %%% (at your option) any later version.
11 %%%
12 %%% PropEr is distributed in the hope that it will be useful,
13 %%% but WITHOUT ANY WARRANTY; without even the implied warranty of
14 %%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 %%% GNU General Public License for more details.
16 %%%
17 %%% You should have received a copy of the GNU General Public License
18 %%% along with PropEr. If not, see <http://www.gnu.org/licenses/>.
19
b36c594 Manolis Papadakis Remove e-mail addresses from EDoc output
authored
20 %%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
6d826f9 Manolis Papadakis Fix copyright notices
authored
21 %%% @version {@version}
b36c594 Manolis Papadakis Remove e-mail addresses from EDoc output
authored
22 %%% @author Manolis Papadakis
6d826f9 Manolis Papadakis Fix copyright notices
authored
23 %%% @doc PropEr usage example: Static mastermind solver
78c6b91 Manolis Papadakis added Mastermind usage example
authored
24
25 -module(mm).
175fcc0 Manolis Papadakis minor tidier-related fixes
authored
26 -export([mastermind/3, mastermind/4]).
78c6b91 Manolis Papadakis added Mastermind usage example
authored
27 -export([prop_all_combinations_are_produced/0,
28 prop_all_selections_are_produced/0,
29 prop_remove_insert_symmetry/0,
30 prop_delete_insert_all_symmetry/0,
31 prop_compatible_works/0,
32 prop_io_filters_are_symmetric/0,
33 prop_next_comb_produces_all_combinations_in_order/0,
34 prop_all_compatibles_are_produced/0,
35 prop_all_produced_solutions_are_valid/1,
36 prop_secret_combination_is_not_discarded/1,
37 prop_invalidated_instances_reject_original_secret/1]).
38
39 -include_lib("proper/include/proper.hrl").
40
41
42 %% -----------------------------------------------------------------------------
43 %% Problem statement
44 %% -----------------------------------------------------------------------------
45
46 %% Given a list of guesses for the secret combination in a game of Mastermind
47 %% and their corresponding score of black and white pegs, find the first
48 %% combination that is compatible with all the guess-score pairs (the order of
49 %% combinations is derived lexicographically from the order of colors).
50
51 %% Colors are represented as hex digits, but we allow the use of letters up to
52 %% 'z' - thus, there may be up to 36 colors ('0' - '9' and 'a' - 'z'). The
53 %% combinations are represented as strings of such characters. That is also the
54 %% expected format for the answer. If there is no combination compatible with
55 %% all the guesses, the program should return the string "-1".
56
57 %% The module should export a function mastermind/3, that takes the following
58 %% arguments:
59 %% 1) the length of the combinations (> 1)
60 %% 2) the number of colors (1..36)
61 %% 3) the list of guess-score pairs, in the format:
62 %% {guess, num_black_pegs, num_white_pegs}
63
64 %% Expected output:
65 %% mm:mastermind(4, 10, [{"3157",1,2},{"1350",2,1},{"6120",0,2},{"2381",3,0}]).
66 %% "2351"
67 %% mm:mastermind(4, 10, [{"3557",1,2},{"1350",2,1},{"6120",0,2},{"2381",3,0}]).
68 %% "-1"
69 %% mm:mastermind(4, 10, [{"3557",1,2},{"1350",0,1},{"2575",2,1},{"5574",3,0}]).
70 %% "5576"
71 %% mm:mastermind(5, 10, [{"12345",1,0},{"02789",1,2},{"82900",3,0}]).
72 %% "22902"
73 %% mm:mastermind(5, 10, [{"23543",0,2},{"45674",1,2},{"67242",2,0}]).
74 %% "67375"
75 %% mm:mastermind(5, 10, [{"74562",0,0},{"11300",1,0}]).
76 %% "18888"
77 %% mm:mastermind(4, 10, [{"1234",1,0},{"0004",1,0},{"0222",0,0},{"4444",1,0},
78 %% {"5554",1,0},{"6664",2,0},{"6784",2,2}]).
79 %% "6874"
80 %% mm:mastermind(6, 10, [{"353523",0,5},{"294333",3,2},{"254672",2,1}]).
81 %% "534332"
82 %% mm:mastermind(6, 10, [{"097654",1,3},{"000465",1,1},{"011579",0,2},
83 %% {"227496",1,3},{"347963",4,1}]).
84 %% "467963"
85 %% mm:mastermind(6, 10, [{"006892",0,2},{"115258",2,2},{"357368",2,1}]).
86 %% "112365"
87 %% mm:mastermind(7, 10, [{"2104767",1,3},{"3541285",3,1},{"7567128",1,4},
88 %% {"0117285",1,4},{"1521775",2,2},{"3261781",4,0}]).
89 %% "3570781"
90 %% mm:mastermind(8, 10, [{"11244556",0,2},{"66756572",1,4},{"00026667",1,3},
91 %% {"03663775",1,3},{"22677262",0,3},{"67568688",7,0}]).
92 %% "67568689"
93 %% mm:mastermind(8, 10, [{"21244767",3,0},{"35455685",3,1},{"75687658",2,4}]).
94 %% "05258667"
95 %% mm:mastermind(8, 10, [{"76897034",5,0},{"76284933",3,2}]).
96 %% "06097033"
97 %% mm:mastermind(9, 10, [{"345352352",0,5},{"287639433",3,2},{"276235467",5,2},
98 %% {"523459878",0,5}]).
99 %% "082235466"
100 %% mm:mastermind(10, 10, [{"3476453523",0,5},{"2876394333",3,2},
101 %% {"2762354672",5,2},{"5234598781",0,5}]).
102 %% "0122374372"
103
104
105 %% -----------------------------------------------------------------------------
106 %% Utility functions
107 %% -----------------------------------------------------------------------------
108
109 %% Function: all_combinations/2
110 %% Produces all 'Len'-length combinations made up of colors selected from
111 %% 'ColorsList'.
112 all_combinations(Len, ColorsList) ->
113 all_combinations_tr(Len, ColorsList, [[]]).
114
115 all_combinations_tr(0, _ColorsList, Acc) ->
116 Acc;
117 all_combinations_tr(Left, ColorsList, Acc) ->
118 NewAcc = [[Color|Rest] || Color <- ColorsList, Rest <- Acc],
119 all_combinations_tr(Left - 1, ColorsList, NewAcc).
120
121 %% Function: all_selections/2
122 %% Returns all possible selections of 'N' elements from list 'List'.
123 all_selections(0, _List) ->
124 [[]];
125 all_selections(N, List) when N >= 1 ->
126 Len = length(List),
127 case N > Len of
128 true ->
129 erlang:error(badarg);
130 false ->
131 all_selections(N, List, Len)
132 end.
133
134 all_selections(1, List, _Len) ->
135 [[X] || X <- List];
136 all_selections(_Len, List, _Len) ->
137 [List];
138 all_selections(Take, [Head|Tail], Len) ->
139 [[Head|Rest] || Rest <- all_selections(Take - 1, Tail, Len - 1)]
140 ++ all_selections(Take, Tail, Len - 1).
141
142 %% Function: all_selection_pos/2
143 %% Returns all possible selections of 'N' positions from a 'Len'-length list.
144 all_selection_pos(N, Len) ->
145 all_selections(N, lists:seq(1,Len)).
146
147 %% Function: remove/2
148 %% Removes from a list, 'List', the elements at positions 'Positions'. Returns
149 %% both the resulting list and a list of the removed elements, in the same
150 %% order they were removed.
151 %% Note that the positions must be given in order.
152 remove(Positions, List) ->
153 remove_tr(Positions, List, 1, [], []).
154
155 remove_tr([], List, _CurrPos, Kept, Removed) ->
156 {lists:reverse(Kept) ++ List, lists:reverse(Removed)};
157 remove_tr([CurrPos|PosTail], [X|ListTail], CurrPos, Kept, Removed) ->
158 remove_tr(PosTail, ListTail, CurrPos + 1, Kept, [X|Removed]);
159 remove_tr(Positions, [X|ListTail], CurrPos, Kept, Removed) ->
160 remove_tr(Positions, ListTail, CurrPos + 1, [X|Kept], Removed).
161
162 %% Function: insert/3
163 %% Inserts into a list, 'List', the elements of 'ToInsert', in the corresponding
164 %% positions, 'Positions'.
165 %% Note that the positions must be given in order.
166 insert(Positions, ToInsert, List) ->
167 insert_tr(Positions, ToInsert, List, 1, []).
168
169 insert_tr([], [], List, _CurrPos, Acc) ->
170 lists:reverse(Acc) ++ List;
171 insert_tr([CurrPos|PosTail], [X|ToInsertTail], List, CurrPos, Acc) ->
172 insert_tr(PosTail, ToInsertTail, List, CurrPos + 1, [X|Acc]);
173 insert_tr(Positions, ToInsert, [X|ListTail], CurrPos, Acc) ->
174 insert_tr(Positions, ToInsert, ListTail, CurrPos + 1, [X|Acc]).
175
176 %% Function: delete/2
177 %% Removes from a list, 'List', a subsequence of that list, 'ToDelete'.
178 delete(List, ToDelete) ->
179 delete_tr(List, ToDelete, []).
180
181 delete_tr(List, [], Acc) ->
182 lists:reverse(Acc) ++ List;
183 delete_tr([_Same|ListTail], [_Same|ToDeleteTail], Acc) ->
184 delete_tr(ListTail, ToDeleteTail, Acc);
185 delete_tr([X|Rest], ToDelete, Acc) ->
186 delete_tr(Rest, ToDelete, [X|Acc]).
187
188 %% Function: insert_all/2
189 %% Returns all possible insertions of the elements of the first list inside the
190 %% second list.
191 insert_all([], List) ->
192 [List];
193 insert_all([X|Rest], List) ->
194 [L2 || L1 <- insert_all(Rest, List), L2 <- all_insertions(X, L1)].
195
196 %% Function: all_insertions/2
197 %% Returns all possible insertions of 'X' inside 'List'.
198 all_insertions(X, List) ->
199 all_insertions_tr(X, [], List, []).
200
201 all_insertions_tr(X, Front, [], Acc) ->
202 [Front ++ [X] | Acc];
203 all_insertions_tr(X, Front, Back = [BackHead|BackTail], Acc) ->
204 all_insertions_tr(X, Front ++ [BackHead], BackTail,
205 [Front ++ [X] ++ Back | Acc]).
206
207 %% Function true_permutation/2
208 %% Returns true iff two permutations of the same list have no element in the
209 %% same position.
210 true_permutation([], []) ->
211 true;
212 true_permutation([_Same|_NewTail], [_Same|_OldTail]) ->
213 false;
214 true_permutation([_NewHead|NewTail], [_OldHead|OldTail]) ->
215 true_permutation(NewTail, OldTail).
216
217
218 %% -----------------------------------------------------------------------------
219 %% Solver code
220 %% -----------------------------------------------------------------------------
221
222 %% Function: compatible/4
223 %% Tests whether combination A produces the given score when compared against
224 %% combination B. This is always the same as when combination B is compared
225 %% against combination A.
226 compatible(A, B, {Blacks,Whites}, Colors) ->
227 correct_blacks(A, B, Blacks)
228 andalso correct_sum(A, B, Blacks + Whites, Colors).
229
230 correct_blacks([], [], 0) -> true;
231 correct_blacks([], [], _N) -> false;
232 correct_blacks([_Same|_At], [_Same|_Bt], 0) -> false;
233 correct_blacks([_Same|At], [_Same|Bt], N) -> correct_blacks(At, Bt, N - 1);
234 correct_blacks([_Ah|At], [_Bh|Bt], N) -> correct_blacks(At, Bt, N).
235
236 correct_sum(A, B, N, Colors) ->
237 AFreqs = collect_freqs(A, Colors),
238 BFreqs = collect_freqs(B, Colors),
239 Common = lists:zipwith(fun erlang:min/2, AFreqs, BFreqs),
240 lists:sum(Common) =:= N.
241
242 collect_freqs(Combination, Colors) ->
243 lists:foldl(fun(C,F) -> inc_freq(C,F) end, lists:duplicate(Colors,0),
244 Combination).
245
246 inc_freq(Color, Freqs) ->
247 {H,[OldFreq | T]} = lists:split(Color, Freqs),
248 H ++ [OldFreq + 1] ++ T.
249
250 %% Function: score/2
251 %% Compares two combinations A and B and calculates the corresponding score.
252 %% A and B must be of the same length and color number. The order of the
253 %% arguments is not important (i.e. it is always score(A,B) = score(B,A)).
254 %% This implementation is sub-optimal on purpose.
255 score(A, B) ->
256 {Blacks,AA,BB} = remove_sames(A, B),
257 Whites = get_whites(AA, BB),
258 {Blacks, Whites}.
259
260 remove_sames(A, B) ->
261 remove_sames_tr(A, B, 0, [], []).
262
263 remove_sames_tr([], [], N, AccA, AccB) ->
264 {N, AccA, AccB};
265 remove_sames_tr([_Same|At], [_Same|Bt], N, AccA, AccB) ->
266 remove_sames_tr(At, Bt, N + 1, AccA, AccB);
267 remove_sames_tr([Ah|At], [Bh|Bt], N, AccA, AccB) ->
268 remove_sames_tr(At, Bt, N, [Ah|AccA], [Bh|AccB]).
269
270 get_whites(A, B) ->
271 SA = lists:sort(A),
272 SB = lists:sort(B),
273 get_whites_tr(SA, SB, 0).
274
275 get_whites_tr([], _B, N) ->
276 N;
277 get_whites_tr(_A, [], N) ->
278 N;
279 get_whites_tr([_Same|At], [_Same|Bt], N) ->
280 get_whites_tr(At, Bt, N + 1);
281 get_whites_tr([Ah|At], B = [Bh|_Bt], N) when Ah < Bh ->
282 get_whites_tr(At, B, N);
283 get_whites_tr(A = [Ah|_At], [Bh|Bt], N) when Ah > Bh ->
284 get_whites_tr(A, Bt, N).
285
286 %% Function: mastermind/3
287 %% Main entry function, serves as input/output filter for an actual solver
288 %% function, which must return a list of combinations that are compatible with
289 %% every guess-score pair provided. Such a list needn't be sorted - actually,
290 %% it needn't even be complete (i.e. containing all plausible secret
291 %% combinations), but it must contain the minimum combination compatible with
292 %% the input, if such a combination exists (being complete, however, helps with
293 %% testing).
294 mastermind(Len, Colors, RawGuesses) ->
295 mastermind(Len, Colors, RawGuesses, heur).
296
297 %% Function: mastermind/4
298 %% The last argument is used to select a particular solver - valid solvers are
299 %% 'simple', 'stream' and 'heur', default is 'heur'.
300 mastermind(Len, Colors, RawGuesses, SolverName) ->
175fcc0 Manolis Papadakis minor tidier-related fixes
authored
301 Guesses = [{parse(RawComb),{B,W}} || {RawComb,B,W} <- RawGuesses],
78c6b91 Manolis Papadakis added Mastermind usage example
authored
302 case valid_input(Len, Colors, Guesses) of
303 true -> ok;
304 false -> erlang:error(badarg)
305 end,
306 Solver = get_solver(SolverName),
307 Result = case Solver(Len, Colors, Guesses) of
308 [] -> error;
309 L -> lists:min(L)
310 end,
311 export(Result).
312
313 parse(RawComb) ->
175fcc0 Manolis Papadakis minor tidier-related fixes
authored
314 [digit_to_integer(X) || X <- RawComb].
78c6b91 Manolis Papadakis added Mastermind usage example
authored
315
316 export(error) ->
317 "-1";
318 export(Comb) ->
175fcc0 Manolis Papadakis minor tidier-related fixes
authored
319 [integer_to_digit(X) || X <- Comb].
78c6b91 Manolis Papadakis added Mastermind usage example
authored
320
321 digit_to_integer(X) when X >= $0, X =< $9 -> X - $0;
322 digit_to_integer(X) when X >= $a, X =< $z -> X - $a + 10;
323 digit_to_integer(X) when X >= $A, X =< $Z -> X - $A + 10.
324
325 integer_to_digit(X) when X >= 0, X =< 9 -> X + $0;
326 integer_to_digit(X) when X >= 10, X =< 35 -> X - 10 + $a.
327
328 valid_input(Len, Colors, Guesses) ->
329 Len > 0 andalso Colors > 0
330 andalso lists:all(fun(G) -> valid_guess(Len, Colors, G) end, Guesses).
331
332 valid_guess(Len, Colors, {Comb,{Blacks,Whites}}) ->
333 Blacks >= 0 andalso Whites >= 0
334 andalso (Blacks + Whites < Len
335 orelse Blacks + Whites =:= Len andalso Whites =/= 1)
336 andalso length(Comb) =:= Len
337 andalso lists:all(fun(X) -> X >= 0 andalso X =< Colors end, Comb).
338
339 get_solver(SolverName) ->
340 case SolverName of
175fcc0 Manolis Papadakis minor tidier-related fixes
authored
341 simple -> fun simple_solver/3;
342 stream -> fun stream_solver/3;
343 heur -> fun heur_solver/3
78c6b91 Manolis Papadakis added Mastermind usage example
authored
344 end.
345
346 %% Function: simple_solver/3
347 %% Simple way to produce all combinations which are compatible with a given
348 %% list of guess-score pairs:
349 %% * create a list of all possible 'Len'-length combinations of 'Colors' colors
350 %% * filter the list with all provided guess-score pairs (for each pair, we
351 %% remove from the list those combinations that are incompatible with it)
352 %% Note that the resulting list is always complete and sorted.
353 simple_solver(Len, Colors, Guesses) ->
354 Combs = all_combinations(Len, lists:seq(0,Colors-1)),
355 filter_guesses(Colors, Guesses, Combs).
356
357 filter_guesses(_Colors, _Guesses, []) ->
358 [];
359 filter_guesses(_Colors, [], Combs) ->
360 Combs;
361 filter_guesses(Colors, [{Guess,Score} | Rest], Combs) ->
362 IsCompatible = fun(C) -> compatible(Guess, C, Score, Colors) end,
363 NewCombs = lists:filter(IsCompatible, Combs),
364 filter_guesses(Colors, Rest, NewCombs).
365
366 %% Function: stream_solver/3
367 %% Low-memory solver: lazily produces and checks all possible combinations in
368 %% order until it finds one that is compatible with all guess-score pairs.
369 %% Note that the resulting list is almost certainly incomplete, since we only
370 %% return the first instance we find.
371 stream_solver(Len, Colors, Guesses) ->
372 stream_solver_tr(Colors, Guesses, lists:duplicate(Len,0)).
373
374 stream_solver_tr(_Colors, _Guesses, done) ->
375 [];
376 stream_solver_tr(Colors, Guesses, Comb) ->
377 case lists:all(fun({C,S}) -> compatible(C,Comb,S,Colors) end, Guesses) of
378 true -> [Comb];
379 false -> stream_solver_tr(Colors, Guesses, next_comb(Colors,Comb))
380 end.
381
382 next_comb(Colors, Comb) ->
383 next_comb_tr(Colors - 1, lists:reverse(Comb), []).
384
385 next_comb_tr(_MaxColor, [], _Acc) ->
386 done;
387 next_comb_tr(MaxColor, [MaxColor | Rest], Acc) ->
388 next_comb_tr(MaxColor, Rest, [0 | Acc]);
389 next_comb_tr(_MaxColor, [X | Rest], Acc) ->
390 lists:reverse(Rest) ++ [X+1] ++ Acc.
391
392 %% Function: heur_solver/3
393 %% More sophisticated solver (avoids the construction of all possible
394 %% combinations):
395 %% * if the guess list is empty, return [[0,0,...,0]], else:
396 %% * sort the guesses by applying a selectivity heuristic (guesses whose
397 %% score will result in more combinations being rejected are prefered)
398 %% * take the first guess-score pair and produce all the combinations it's
399 %% compatible with
400 %% * filter the list with the rest of the pairs
401 %% Note that the resulting list is always complete (except for the special case
402 %% when Guesses =:= []) but is not necessarily sorted.
403 heur_solver(Len, _Colors, []) ->
404 [lists:duplicate(Len, 0)];
405 heur_solver(Len, Colors, Guesses) ->
406 [First|Rest] = lists:sort(fun(A,B) -> more_selective(A,B,Colors) end,
407 Guesses),
408 Combs = all_compatibles(Len, Colors, First),
409 filter_guesses(Colors, Rest, Combs).
410
411 %% Function: more_selective/2
412 %% Selectivity heuristic used to sort guess-score pairs. We suspect that
413 %% guess-score pair A is more selective than B if:
414 %% 1) it has a greater total score
415 %% 2) it has more black pegs
416 %% 3) it has fewer distinct colors
417 %% The above criteria are processed in that exact order.
418 more_selective({CombA,{BlacksA,WhitesA}}, {CombB,{BlacksB,WhitesB}}, Colors) ->
419 case sign((BlacksA + WhitesA) - (BlacksB + WhitesB)) of
420 +1 -> true;
421 -1 -> false;
422 0 -> case sign(BlacksA - BlacksB) of
423 +1 -> true;
424 -1 -> false;
425 0 -> distinct_colors(CombA, Colors)
426 =< distinct_colors(CombB, Colors)
427 end
428 end.
429
430 sign(0) -> 0;
431 sign(X) when X > 0 -> +1;
432 sign(X) when X < 0 -> -1.
433
434 distinct_colors(Comb, Colors) ->
435 lists:foldl(fun(F,S) -> sign(F) + S end, 0, collect_freqs(Comb, Colors)).
436
437 %% Function: all_compatibles/3
438 %% Runs the 'all_whites' function for all possible selections of 'Blacks'
439 %% positions in the given combination.
440 all_compatibles(Len, Colors, {Comb,{Blacks,Whites}}) ->
441 NonFixedLen = Len - Blacks,
442 [C || BlackSelPos <- all_selection_pos(Blacks, Len),
443 C <- all_whites(NonFixedLen, Whites, Colors, Comb, BlackSelPos)].
444
445 all_whites(NonFixedLen, Whites, Colors, Comb, BlackSelPos) ->
446 RejectedLen = NonFixedLen - Whites,
447 {NonFixed,Fixed} = remove(BlackSelPos, Comb),
448 UnsortedWhiteSels =
449 [{Sel,lists:sort(Sel)} || Sel <- all_selections(Whites, NonFixed)],
450 WhiteSels = lists:ukeysort(2, UnsortedWhiteSels),
451 [insert(BlackSelPos, Fixed, C)
452 || {WhiteSel,_} <- WhiteSels,
453 C <- all_moves(NonFixed, WhiteSel, RejectedLen, Colors)].
454
455 all_moves(NonFixed, WhiteSel, RejectedLen, Colors) ->
456 Rejected = delete(NonFixed, WhiteSel),
457 RemainingColors = lists:seq(0,Colors-1) -- Rejected,
458 AllCombs = all_combinations(RejectedLen, RemainingColors),
459 UnsortedAllMoves = [L || C <- AllCombs,
460 L <- insert_all(WhiteSel, C),
461 true_permutation(L, NonFixed)],
462 lists:usort(UnsortedAllMoves).
463
464
465 %% -----------------------------------------------------------------------------
466 %% Properties to check
467 %% -----------------------------------------------------------------------------
468
469 prop_all_combinations_are_produced() ->
470 ?FORALL({Len, ColorsList},
471 {range(0,5), short_nd_list(integer())},
472 begin
473 AllCombs = all_combinations(Len, ColorsList),
474 NumAllCombs = pow(length(ColorsList), Len),
475 lofl_check(AllCombs, NumAllCombs, Len, ColorsList)
476 andalso no_duplicates(AllCombs)
477 end).
478
479 short_nd_list(ElemType) ->
480 ?LET(L,
481 resize(7, list(ElemType)),
482 lists:usort(L)).
483
484 lofl_check(Lofl, NumLists, ListLen, ListElems) ->
485 lofl_check(Lofl, NumLists, ListLen, ListElems, 0).
486
487 lofl_check([], NumLists, _ListLen, _ListElems, Acc) ->
488 Acc =:= NumLists;
489 lofl_check([List|Rest], NumLists, ListLen, ListElems, Acc) ->
490 list_check(List, ListLen, ListElems)
491 andalso lofl_check(Rest, NumLists, ListLen, ListElems, Acc + 1).
492
493 list_check([], 0, _Elems) ->
494 true;
495 list_check([], _Left, _Elems) ->
496 false;
497 list_check([X|Rest], Left, Elems) ->
498 lists:member(X, Elems)
499 andalso list_check(Rest, Left - 1, Elems).
500
501 pow(X, Y) ->
502 pow_tr(X, Y, 1).
503
504 pow_tr(_X, 0, Acc) ->
505 Acc;
506 pow_tr(X, Y, Acc) ->
507 pow_tr(X, Y - 1, X * Acc).
508
509 no_duplicates(L) -> length(L) =:= length(lists:usort(L)).
510
511 prop_all_selections_are_produced() ->
512 ?FORALL(List,
513 short_ne_list(integer()),
514 begin
515 Len = length(List),
516 ?FORALL(N,
517 range(0,Len),
518 begin
519 AllSels = all_selections(N, List),
520 NumAllSels = num_sels(N, Len),
521 lofl_check(AllSels, NumAllSels, N, List)
522 end)
523 end).
524
525 short_list(ElemType) ->
526 resize(10, list(ElemType)).
527
528 short_ne_list(ElemType) ->
529 non_empty(short_list(ElemType)).
530
531 num_sels(N, Len) ->
532 fact(Len) div fact(N) div fact(Len - N).
533
534 fact(0) ->
535 1;
536 fact(N) when N >= 1 ->
537 N * fact(N-1).
538
539 prop_remove_insert_symmetry() ->
540 ?FORALL(List,
541 short_ne_list(integer()),
542 ?FORALL(Positions,
543 pos_selection(List),
544 begin
545 {Kept,Removed} = remove(Positions,List),
546 insert(Positions,Removed,Kept) =:= List
547 end)).
548
549 pos_selection(List) ->
550 Len = length(List),
551 ?LET(N,
552 range(0,Len),
553 oneof(all_selection_pos(N, Len))).
554
555 prop_delete_insert_all_symmetry() ->
556 ?FORALL(List,
557 short_list(integer()),
558 ?FORALL(Subseq,
559 subsequence(List),
560 lists:member(List,
561 insert_all(Subseq,delete(List,Subseq))))).
562
563 subsequence(List) ->
564 ?LET(L,
565 [{X,boolean()} || X <- List],
566 [Y || {Y,true} <- L]).
567
568 prop_compatible_works() ->
569 ?FORALL({Colors,A,B},
570 two_combinations(),
571 compatible(A, B, score(A,B), Colors)).
572
573 combination(Len, Colors) ->
574 vector(Len, range(0,Colors-1)).
575
576 two_combinations() ->
577 ?LET({Len, Colors},
578 {range(0,30), range(1,36)},
579 {Colors, combination(Len,Colors), combination(Len,Colors)}).
580
581 prop_io_filters_are_symmetric() ->
582 ?FORALL(L,
583 list(digit()),
584 collect(num_digits(length(L)),
585 export(parse(L)) =:= L)).
586
587 digit() -> union([range($0,$9), range($a,$z)]).
588
589 num_digits(X) when X >= 0, X =< 9 -> 1;
590 num_digits(X) when X >= 10 -> 1 + num_digits(X div 10).
591
592 prop_next_comb_produces_all_combinations_in_order() ->
593 ?FORALL({Len, Colors},
594 {range(0,5), range(1,10)},
595 list_is_produced(Colors, lists:duplicate(Len,0),
596 all_combinations(Len,lists:seq(0,Colors-1)))).
597
598 list_is_produced(_Colors, done, []) ->
599 true;
600 list_is_produced(Colors, Same, [Same | Rest]) ->
601 list_is_produced(Colors, next_comb(Colors,Same), Rest);
602 list_is_produced(_Colors, _Comb, _List) ->
603 false.
604
605 prop_all_compatibles_are_produced() ->
606 ?FORALL({Len, Colors, Guess},
607 one_guess_instance(),
608 simple_solver(Len, Colors, [Guess])
609 =:= lists:sort(all_compatibles(Len, Colors, Guess))).
610
611 one_guess_instance() ->
612 ?LET({Len, Colors},
613 {range(2,5), range(2,10)},
614 {Len, Colors, scored_guess(Len,Colors)}).
615
616 scored_guess(Len, Colors) ->
617 ?LET(Score,
618 valid_score(Len),
619 {combination(Len,Colors), Score}).
620
621 valid_score(Len) ->
622 ?LET(Blacks,
623 range(0,Len),
624 ?LET(Whites,
625 ?SUCHTHAT(W,
626 range(0,Len-Blacks),
627 W =/= 1 orelse Blacks + W =/= Len),
628 {Blacks,Whites})).
629
630 prop_all_produced_solutions_are_valid(SolverName) ->
631 Solver = get_solver(SolverName),
632 ?FORALL({Len, Colors, Guesses},
633 instance(),
634 begin
635 Solutions = Solver(Len, Colors, Guesses),
636 collect(Solutions =:= [],
637 lists:all(fun(Solution) ->
638 lists:all(fun({C,Score}) ->
639 compatible(C,Solution,
640 Score,Colors)
641 end,
642 Guesses)
643 end,
644 Solutions))
645 end).
646
647 instance() ->
648 ?LET({Len, Colors},
649 {range(2,5), range(2,10)},
650 {Len, Colors, short_list(scored_guess(Len,Colors))}).
651
652 %% Note that the next property is not necessarily true for solvers that don't
653 %% return complete lists.
654 prop_secret_combination_is_not_discarded(SolverName) ->
655 Solver = get_solver(SolverName),
656 ?FORALL({Len,Colors,Secret,Guesses},
657 full_non_trivial_instance(),
658 lists:member(Secret, Solver(Len,Colors,Guesses))).
659
660 full_non_trivial_instance() ->
661 ?LET({Len, Colors},
662 {range(2,5), range(2,10)},
663 ?LET({Secret, Guesses},
664 {combination(Len,Colors), short_ne_list(combination(Len,Colors))},
665 {Len,Colors,Secret,[{G,score(G,Secret)} || G <- Guesses]})).
666
667 prop_invalidated_instances_reject_original_secret(SolverName) ->
668 Solver = get_solver(SolverName),
669 ?FORALL({Len,Colors,Secret,Guesses},
670 invalid_instance(),
671 not lists:member(Secret, Solver(Len,Colors,Guesses))).
672
673 invalid_instance() ->
674 ?LET({Len,Colors,Secret,Guesses},
675 full_non_trivial_instance(),
676 ?LET(Pos,
677 range(1,length(Guesses)),
678 begin
679 {Comb,OldScore} = lists:nth(Pos,Guesses),
680 ?LET(NewScore,
681 ?SUCHTHAT(S, valid_score(Len), S =/= OldScore),
682 {Len,Colors,Secret,
683 list_update(Pos,{Comb,NewScore},Guesses)})
684 end)).
685
686 list_update(Index, NewElem, List) ->
687 {H,[_OldElem | T]} = lists:split(Index - 1, List),
688 H ++ [NewElem] ++ T.
Something went wrong with that request. Please try again.