1		:- module(kodkod_test, [test_kodkod/1, compare_kodkod_performance/2]).
2
3		:- use_module(library(lists)).
4
5		:- use_module(probsrc(tools),[start_ms_timer/1,stop_ms_timer/2,average/2,ajoin/2]).
6		:- use_module(probsrc(module_information),[module_info/2]).
7		:- use_module(probsrc(error_manager),[add_error/2]).
8		:- use_module(probsrc(bsyntaxtree)).
9		:- use_module(probsrc(bmachine)).
10		:- use_module(probsrc(b_interpreter)).
11		:- use_module(probsrc(store)).
12		:- use_module(probsrc(b_enumerate)).
13		:- use_module(probsrc(kernel_waitflags)).
14		:- use_module(probsrc(error_manager)).
15		:- use_module(probsrc(junit_tests)).
16		:- use_module(probsrc(translate)).
17		:- use_module(probsrc(succeed_max)).
18		:- use_module(probsrc(preferences),[get_preference/2]).
19		:- use_module(probsrc(tools_timeout),[time_out_call/2]).
20
21		:- use_module(kodkod).
22		:- use_module(kodkod_process).
23
24		:- module_info(group,kodkod).
25		:- module_info(description,'This is a test engine for the Kodkod translation functionality.').
26
27		compare_kodkod_performance(Outfile,Iterations) :-
28		kodkod_performance(Iterations,Results),
29		open(Outfile,write,S),
30		maplist(print_result(S),Results),
31		close(S).
32
33		print_result(S,translation_failed(Pred)) :-
34		print_intro(S,Pred),
35		write(S,'Status: translation failed\n').
36		print_result(S,comparision(Pred,_Ks,_Ps,Kodkod,ProB)) :-
37		print_intro(S,Pred),
38		write(S,'Status: translation succeeded\n'),
39		print_result2(S,Kodkod,KN),
40		print_result2(S,ProB,PN),
41		(KN=PN -> true ; write(S,'Error: different number of results\n')).
42		print_intro(S,Pred) :-
43		write(S,'___ Comparing for predicate ___\n'),
44		conjunction_to_list(Pred,Preds),
45		maplist(print_intro2(S),Preds).
46		print_intro2(S,Pred) :-
47		translate_bexpression(Pred,TPred),
48		format(S,'Pred: ~w~n',[TPred]).
49		print_result2(S,kodkod_timeout,_) :-
50		print_time(S,'Kodkod total',timeout),
51		print_time(S,'Kodkod preparation',timeout),
52		print_time(S,'Kodkod computation',timeout),
53		print_time(S,'Kodkod Java',timeout).
54		print_result2(S,kodkod_solved(PrepTime,CompTime,JavaTime,N),N) :-
55		memberchk(walltime/PT,PrepTime),
56		memberchk(walltime/CT,CompTime),
57		TT is PT+CT,
58		print_time(S,'Kodkod total',TT),
59		print_time(S,'Kodkod preparation',PT),
60		print_time(S,'Kodkod computation',CT),
61		print_time(S,'Kodkod Java',JavaTime).
62		print_result2(S,prob_timeout,_) :-
63		print_time(S,'ProB total',timeout).
64		print_result2(S,prob_solved(CompTime,N),N) :-
65		memberchk(walltime/TT,CompTime),
66		print_time(S,'ProB total',TT).
67		print_time(S,Name,Time) :-
68		( Time = timeout ->
69		format(S,'~w time: ~w~n', [Name,timeout])
70		;
71		format(S,'~w time: ~0f~n',[Name,Time])).
72
73
74
75		kodkod_performance(Iterations,Results) :-
76		b_get_machine_constants(Constants),
77		( Constants = [_|_] ->
78		kodkod_performance2(Constants,Iterations,Results)
79		;
80		add_error(kodkod_test,'No constants to check measure performance of Kodkod translation'),
81		fail).
82
83		kodkod_performance2(Constants,Iterations,Results) :-
84		b_get_properties_from_machine(Predicate),
85		predicate_components(Predicate,Components),
86		maplist(kodkod_performance3(Constants,Iterations),Components,Results).
87
88		kodkod_performance3(Constants,Iterations,component(Predicate,Ids),Result) :-
89		include(memberid(Ids),Constants,TIds),
90		kodkod_performance4(Predicate,TIds,Iterations,Result).
91
92		kodkod_performance4(Predicate,Constants,Iterations,comparision(Predicate,Ks,Ps,Ksum,Psum)) :-
93		kodkod_translation(Predicate,Constants,_KPred),
94		!,
95		kodkod_performance5(Predicate,Constants,Iterations,Ks,Ps),
96		summarize_kodkod(Ks,Ksum),
97		summarize_prob(Ps,Psum).
98		kodkod_performance4(Predicate,_Constants,_Iterations,translation_failed(Predicate)).
99
100		kodkod_performance5(Predicate,Constants,Iterations,[K|Krest],[P|Prest]) :-
101		Iterations > 0,!,
102		call_kodkod(Predicate,Constants,K),
103		call_prob(Predicate,Constants,P),
104		I2 is Iterations - 1,
105		kodkod_performance5(Predicate,Constants,I2,Krest,Prest).
106		kodkod_performance5(_Predicate,_Constants,_Iterations,[],[]).
107
108		summarize_kodkod(L,kodkod_timeout) :-
109		memberchk(timeout,L),!.
110		summarize_kodkod(L,kodkod_solved(PrepTime,CompTime,JavaTime,NrSolutions)) :-
111		maplist(get_kodkod_prep_time,L,PTimes),summarize_times(PTimes,PrepTime),
112		maplist(get_kodkod_comp_time,L,CTimes),summarize_times(CTimes,CompTime),
113		maplist(get_kodkod_java_time,L,JTimes),average(JTimes,JavaTime),
114		maplist(get_kodkod_nsol,L,Sols),check_same(Sols,NrSolutions).
115		summarize_prob(L,prob_timeout) :-
116		memberchk(timeout,L),!.
117		summarize_prob(L,prob_solved(CompTime,NrSolutions)) :-
118		maplist(get_prob_comp_time,L,CTimes),summarize_times(CTimes,CompTime),
119		maplist(get_prob_nsol,L,Sols),check_same(Sols,NrSolutions).
120
121		summarize_times([T|Rest],Times) :-
122		findall(S, member(S/_,T), Secs),
123		maplist(sum_time([T|Rest]), Secs, Times).
124		sum_time(Lists,Sec,Sec/Time) :-
125		member(L,Lists),member(Sec/timeout,L),!,Time=timeout.
126		sum_time(Lists,Sec,Sec/Time) :-
127		findall(T, (member(L,Lists),memberchk(Sec/T,L)), Times),
128		average(Times,Time).
129
130		check_same(L,V) :-
131		(is_same(L,V) -> true ; add_error(kodkod_test,'Inconsistent number of solutions'),fail).
132
133		is_same([E],V) :- !,E=V.
134		is_same([V|L],V) :-
135		is_same(L,V).
136
137
138		get_kodkod_prep_time(kodkod_solved(PrepTime,_CompTime,_JavaTime,_N),PrepTime).
139		get_kodkod_comp_time(kodkod_solved(_PrepTime,CompTime,_JavaTime,_N),CompTime).
140		get_kodkod_java_time(kodkod_solved(_PrepTime,_CompTime,JavaTime,_N),JavaTime).
141		get_kodkod_nsol(kodkod_solved(_PrepTime,_CompTime,_JavaTime,N),N).
142
143		get_prob_comp_time(prob_solved(CompTime,_N),CompTime).
144		get_prob_nsol(prob_solved(_CompTime,N),N).
145
146
147		:- meta_predicate measured_call(0,?).
148		measured_call(Call,TimeRes) :-
149		start_ms_timer(Timer),
150		time_out_call(Call,Timeout=true),
151		stop_ms_timer(Timer,Time),
152		( Timeout = false -> TimeRes = Time
153		; Timeout = true -> TimeRes = timeout).
154
155		call_kodkod(Predicate,Constants,Result) :-
156		measured_call(kodkod_translation(Predicate,Constants,KPred),PrepTime),
157		!,
158		clear_java_comp_time,
159		measured_call(find_solutions(Constants,KPred,States),CompTime),
160		( CompTime == timeout ->
161		Result = timeout
162		;
163		Result = kodkod_solved(PrepTime,CompTime,JavaTime,NrSolutions),
164		get_java_comp_time(JavaTime),
165		length(States,NrSolutions)).
166		call_prob(Predicate,Constants,Result) :-
167		measured_call(find_solutions(Constants,Predicate,States),CompTime),
168		( CompTime == timeout ->
169		Result = timeout
170		;
171		Result = prob_solved(CompTime,NrSolutions),
172		length(States,NrSolutions)).
173
174		kodkod_translation(Predicate,Constants,KPred) :-
175		kodkod:try_predicate_analysis_with_global_sets(Predicate,Constants,TaggedConstants,TaggedPredicate),
176		kodkod:apply_transformation2(TaggedConstants,TaggedPredicate,KPred).
177
178
179		memberid(Ids,TId) :-
180		get_texpr_id(TId,Id),memberchk(Id,Ids).
181
182		:- meta_predicate check(0,-).
183
184		test_kodkod(MaxResiduePreds) :-
185		catch( (test_kodkod2(MaxResiduePreds),store_testcase(pass)),
186		junit(Msg),
187		store_testcase(error([Msg]))).
188		test_kodkod2(MaxResiduePreds) :-
189		b_get_machine_constants(Constants),
190		b_get_properties_from_machine(Predicate),
191		check( Constants=[_|_], 'Test failed, no constants present in machine.'),
192		check( find_prob_solutions(Predicate,Constants,ProBStates),
193		'finding ProB solutions failed'),
194		check( find_kodkod_solutions(Predicate,Constants,KodkodStates,Residue),
195		'finding Kodkod solutions failed'),
196		ajoin(['too many remaining predicates: ', Residue, ' > ' , MaxResiduePreds],TooManyErrMessage),
197		check( Residue =< MaxResiduePreds,TooManyErrMessage),
198		check( ProBStates = KodkodStates,
199		'different solutions found').
200
201		find_prob_solutions(Predicate,Constants,States) :-
202		find_solutions(Constants,Predicate,States).
203
204		find_kodkod_solutions(Predicate,Constants,States,Residue) :-
205		%predicate_size(Predicate,Before),
206		replace_by_kodkod(Constants,Predicate,KPredicate),
207		check( kodkod_present(KPredicate),
208		'no kodkod translation applied'),
209		predicate_size(KPredicate,After), Residue is After-1,
210		find_solutions(Constants,KPredicate,States).
211
212		predicate_size(Predicate,Size) :-
213		conjunction_to_list(Predicate,Preds),
214		length(Preds,Size).
215
216		kodkod_present(Predicate) :-
217		conjunction_to_list(Predicate,Preds),
218		create_texpr(kodkod(_,_),pred,_,KPred),
219		memberchk(KPred,Preds).
220
221		find_solutions(Constants,Predicate,States) :-
222		get_preference(maxNrOfInitialisations,Max),
223		findall(State,
224		succeed_max_call(find_solution(Constants,Predicate,State),Max),
225		UnsortedStates),
226		sort(UnsortedStates,States).
227
228		find_solution(Constants,Predicate,NormalizedState) :-
229		empty_state(Empty),
230		set_up_typed_localstate(Constants,_Values,TypedValues,Empty,State,positive),
231		normalise_store(State,NormalizedState),
232		init_wait_flags_with_call_stack(WF,[prob_command_context(kodkod_find_solution,unknown)]),
233		b_tighter_enumerate_values_in_ctxt(TypedValues,Predicate,WF),
234		b_test_boolean_expression(Predicate,Empty,State,WF),
235		ground_wait_flags(WF).
236
237		check(Check,Msg) :-
238		( call(Check) -> true
239		; in_junit_mode -> throw(junit(Msg))
240		; add_error(kodkod_test,Msg), fail
241		).
242
243		store_testcase(Verdict) :-
244		in_junit_mode,!,
245		b_machine_name(Name),
246		create_and_print_junit_result([kodkod,comparision_with_prob],Name,0,Verdict).
247		store_testcase(_Verdict).
248
249		in_junit_mode :- junit_mode(_),!.