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