1 % (c) 2009-2013 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5
6 :- module(log_analyser,[set_log_file_to_analyse/1, analyse_log/3, analyse_log/0, set_row_identifier/1,
7 check_log/1]).
8
9
10 % to do: use argv to determine which log file(s) are to be included
11 :- use_module(tools).
12 :- use_module(error_manager).
13 :- use_module(library(lists)).
14
15 :- use_module(module_information,[module_info/2]).
16 :- module_info(group,misc).
17 :- module_info(description,'A small tool to generate Excel or Gnuplot data and scripts to analyse data generated by probcli when model checking with logging (-l).').
18
19 :- dynamic benchmark/1, benchmark/3, row_identifier/1, group/1.
20
21 assert_group(G) :- group(G) -> true ; assert(group(G)).
22
23 mc_entry(BenchT,TIME,MCTime) :- mc_entry(BenchT,TIME,MCTime,_REV).
24 mc_entry(BenchT,TIME,FullWallTime,rev(REV,FOptions)) :-
25 model_check(Now,_,_MCTime,_Res,_TotRun,TotWall),
26 loading(Now,B,_StartRun,StartWall),
27 FullWallTime is TotWall - StartWall, % assumes nothing else done
28 version(Now,_V1,_V2,_V3,_V4,REV,_LASTCHANGED),
29 options(Now,Options), filter_options(Options,FOptions),
30 %date(Now,datime(Year,Month,Day,_,_)),
31 TIME = Now, %is Now // 100,
32 get_tail_filename(B,BenchT).
33
34 init :- retractall(benchmark(_)), print('Benchmarks: '),
35 setof(B,Date^Time^mc_entry(B,Date,Time),Bench),
36 sort(Bench,SB),
37 print(SB),nl,
38 member(B1,SB),
39 assert(benchmark(B1)),fail.
40 init :- retractall(benchmark(_,_,_)),benchmark_group(Group,Benchmark,Name),
41 (benchmark(Benchmark) -> true ; print('### No entry for : '), print(Benchmark),nl,fail),
42 assert(benchmark(Benchmark,Group,Name)), assert_group(Group),
43 fail.
44 init :- benchmark(Benchmark), \+ benchmark_group(_,Benchmark,_),
45 print('* No group for: '), print(Benchmark),nl,
46 assert(benchmark(Benchmark,unknown,Benchmark)), assert_group(unknown), fail.
47 init :- retractall(row_identifier(_)),
48 use_for_row_identifier(timestamp), print('Timestamps: '),
49 setof(D,B^Time^mc_entry(B,D,Time),Dates),
50 sort(Dates,SB),
51 print(SB),nl,
52 member(D1,SB),
53 assert(row_identifier(D1)),fail.
54 init :- use_for_row_identifier(revision), print('Revisions: '),
55 setof(Rev,B^D^Time^mc_entry(B,D,Time,Rev),Revs),
56 sort(Revs,SB),
57 print(SB),nl,
58 member(D1,SB),
59 assert(row_identifier(D1)),fail.
60 init.
61
62
63 filter_options([],[]).
64 filter_options([H|T],R) :-
65 (interesting_option(H,HH) -> R=[HH|RT] %prob_cli:recognised_option(HH,H),R=[HH|RT]
66 ; R=RT),
67 filter_options(T,RT).
68 interesting_option(depth_first,df).
69 interesting_option(breadth_first,bf).
70 interesting_option(comment(C),C).
71 interesting_option(set_pref('OPERATION_REUSE',T),op_reuse) :- is_true(T).
72 interesting_option(set_pref('USE_PO',T),no_po) :- is_false(T).
73 interesting_option(set_pref('SYMMETRY_MODE',hash),hash).
74 interesting_option(set_pref('SYMMETRY_MODE',nauty),nauty).
75 interesting_option(set_pref('SYMMETRY_MODE',flood),flood).
76 interesting_option(set_pref('SYMBOLIC',T),symbolic) :- is_true(T).
77 %interesting_option(no_deadlocks,nodead).
78 %interesting_option(no_invariant_violations,noinv).
79 %interesting_option(set_pref(PREF,PREFVAL),pref(PREF,PREFVAL)).
80
81 is_true('TRUE'). is_true(true).
82 is_false('FALSE'). is_false(false).
83
84 % determine what is used to group rows
85 :- dynamic use_for_row_identifier/1.
86 use_for_row_identifier(timestamp).
87 %use_for_row_identifier(revision).
88
89 set_row_identifier(ID) :- (ID=timestamp; ID=revision),!,
90 retractall(use_for_row_identifier(_)),
91 assert(use_for_row_identifier(ID)).
92 set_row_identifier(ID) :- add_error(log_analyser,'Illegal Row Identifier: ',ID).
93
94 get_mc_time_for_row_identifier(Benchmark,ID,MCTime) :- use_for_row_identifier(timestamp),
95 ID=TimeStamp,
96 mc_entry(Benchmark,TimeStamp,MCTime,_Rev).
97 get_mc_time_for_row_identifier(Benchmark,ID,MCTime) :- use_for_row_identifier(revision),
98 ID=Revision,
99 mc_entry(Benchmark,_TimeStamp,MCTime,Revision).
100
101 :- public p/0.
102 p :- init, print_normal_table.
103
104 print_normal_table :- print_header,
105 print_row_identifier_header,
106 benchmark(_B,_,BN), print_cell(BN),
107 fail.
108 print_normal_table :- nl,
109 row_identifier(D),
110 print_row(D),
111 fail.
112 print_normal_table :- nl.
113
114 print_transposed_excel_table :- print_header,
115 print_cell('Revision'), row_identifier(D), print_row_identifier1(D),fail.
116 print_transposed_excel_table :- nl,
117 print_cell('Benchmark/Options'), row_identifier(D), print_row_identifier2(D),fail.
118 print_transposed_excel_table :- nl,
119 group(G), print_cell(G),nl,
120 print_message(treating_group(G)),
121 benchmark(B,G,BN), print_cell(BN),
122 print_benchmark_line(B),
123 fail.
124 print_transposed_excel_table :- nl.
125
126 print_benchmark_line(B) :- row_identifier(RowID), print_mc_time_cell(B,RowID),fail.
127 print_benchmark_line(_) :- nl.
128
129 print_row(RowID) :- print_row_identifier(RowID),
130 benchmark(B,_,_), print_mc_time_cell(B,RowID),
131 fail.
132 print_row(_) :- nl.
133
134 print_mc_time_cell(B,RowID) :-
135 (get_mc_time_for_row_identifier(B,RowID,MCTime) -> print_cell(MCTime) ; print_cell('??')).
136
137 print_row_identifier_header :- use_for_row_identifier(revision),!,
138 print_cell('Revision'), print_cell('Options').
139 print_row_identifier_header :- print_cell('Timestamp').
140
141 print_row_identifier1(rev(ID,_Options)) :- print_cell(ID),!.
142 print_row_identifier1(X) :- print_row_identifier(X).
143 print_row_identifier2(rev(_ID,Options)) :- print_cell(Options),!.
144 print_row_identifier2(X) :- print_row_identifier(X).
145
146 print_row_identifier(rev(ID,Options)) :- use_for_row_identifier(revision),!,
147 print_cell(ID),print_cell(Options).
148 print_row_identifier(TimeStamp) :-
149 (date(TimeStamp,datime(Year,Month,Day,Hour,Minutes,Seconds))
150 -> RealTime is Seconds + Minutes*60 + Hour*60*60 +
151 Day*24*60*60 + Month*31*24*60*60 + (Year-2008)*12*31*24*60*60,
152 print_cell(RealTime)
153 ; print_cell(TimeStamp), tools:print_error(unknown(TimeStamp))
154 ).
155
156 print_cell(X) :- var(X),!,print('_VARIABLE_'), print_sep.
157 print_cell([H|T]) :- !, print('"'),print_list([H|T]), print('"'), print_sep.
158 print_cell(X) :- print(X), print_sep.
159
160 print_list([]).
161 print_list([H|T]) :- print(H), print_list(T).
162
163 print_gnuplot_script :- data_file(F),
164 format('set xtics 1,1~Nset style data linespoints~Nset title ""~Nset grid ytics~Nset terminal postscript eps enhanced~Nset output "~p.ps"~N',[F]),
165 % set term aqua
166 print('plot '),
167 findall(BN,benchmark(_B,_,BN),Benchs),
168 nth1(Nr,Benchs,BB),
169 (Nr>1 -> print(', \\'),nl ; true),
170 print_data_file,
171 N1 is Nr+1,
172 print('using 1:'), print(N1), print(' title "'),print(BB), print('"'),
173 fail.
174 print_gnuplot_script :- nl.
175
176 print_data_file :- data_file(F), print('"'),print(F),print('" ').
177
178
179 :- dynamic log_file/1.
180 log_file('../log/puzzle.log').
181
182 set_log_file_to_analyse(F) :- retractall(log_file(_)), assert(log_file(F)),
183 split_filename(F,Base,_Extension),
184 data_file_extension(DExt),
185 string_concatenate(Base,DExt,DF),
186 print_message(data_file(DF)),
187 retractall(data_file(_)), assert(data_file(DF)),
188 string_concatenate(Base,'.plot',PF),
189 print_message(script_file(PF)),
190 retractall(script_file(_)), assert(script_file(PF)).
191
192 :- dynamic data_file/1.
193 data_file('../log/puzzle.data').
194
195 :- dynamic script_file/1.
196 script_file('../log/puzzle.plot').
197
198
199 :- dynamic for_gnuplot/0.
200 for_gnuplot.
201
202 print_header :- for_gnuplot,!,print('# ').
203 print_header.
204
205 print_sep :- for_gnuplot,!,print('\t'). % for gnuplot
206 print_sep :- print(', '). % for Excel CSV
207
208
209 data_file_extension(Ext) :-
210 (for_gnuplot -> Ext = '.data' ; Ext = '.csv').
211
212 % -------------------
213
214 analyse_log(F,RowID,ForGnuPlot) :- set_row_identifier(RowID),
215 retractall(for_gnuplot),
216 (ForGnuPlot=true -> assert(for_gnuplot) ; true),
217 set_log_file_to_analyse(F),
218 analyse_log.
219
220 :- dynamic benchmark_group/3.
221
222 analyse_log :- log_file(LF), consult_without_redefine_warning(LF),
223 print_message('Initialising'),
224 init,
225 data_file(F),
226 print_message('Generating Table'),
227 tell(F),
228 (for_gnuplot -> print_normal_table ; print_transposed_excel_table),
229 told,
230 print_message('Finished Generating Table'),
231 (for_gnuplot
232 -> script_file(SF),
233 tell(SF),
234 print_gnuplot_script,
235 told,
236 print('Now run "gnuplot '), print(SF), print('"'),nl,
237 print(' and then open "'),print(F),print('.ps"'),nl % we could execute it also in Prolog
238 ; print('Now open "'), print(F), print('" using Excel'),nl
239 ).
240
241
242 consult_without_redefine_warning(File) :-
243 prolog_flag(redefine_warnings, Old, off),
244 (% load in dynamic mode: so that we can retract later
245 my_consult(File)
246 -> OK=true ; OK=false),
247 prolog_flag(redefine_warnings, _, Old),
248 (OK=true -> true ;
249 add_error_and_fail(bmachine,'Consulting of File failed: ',File)).
250
251 my_consult(File) :- on_exception(error(existence_error(_,_),_),
252 load_files(File,[compilation_mode(assert_all)]),
253 add_error_fail(my_consult,'File does not exist: ',File)).
254
255 % ------------------------
256
257 % a version suitable for analysing the Siemens RuleBase validation output
258 % run with probcli -p CLPFD TRUE -p TIME_OUT 5000 *.v -l all.log -init -expcterr setup_constants_fails
259 :- dynamic loading/4.
260 :- dynamic error_occurred/2, loading_failed/4, expected_error_did_not_occur/2.
261 :- dynamic start_animation/3, finished_processing/2.
262
263 check_log(F) :- consult_without_redefine_warning(F),
264 print('File'), print_sep, print('Result'), print_sep,
265 print('Loading time'), print_sep, print('(Walltime)'), print_sep,
266 print('Checking time'), print_sep, print('(Walltime)'), nl,
267 lookup(loading(NOW,Filename,StartTime,StartWTime)),nl,
268 get_tail_filename(Filename,Tail),
269 print(Tail), print_sep,
270 (lookup(error_occurred(NOW,parse_error)) -> print('PARSE ERROR')
271 ; lookup(error_occurred(NOW,type_error)) -> print('TYPE ERROR')
272 ; lookup(error_occurred(NOW,time_out)) -> print('TIME_OUT')
273 ; lookup(error_occurred(NOW,cbc_assertions_time_out)) -> print('TIME_OUT')
274 ; lookup(loading_failed(NOW,Filename,_,_)) -> print('OTHER LOAD ERROR')
275 ; lookup(error_occurred(NOW,cbc_assertions))
276 -> print('** KO **') % print('*** COUNTER EXAMPLE FOUND ***')
277 ; lookup(cbc_assertions_finished(NOW,no_counterexample_found,_,_))
278 -> print('OK (ENUM WARNING)')
279 % TO DO: also register if b_global_sets:unfixed_deferred_set(_) TRUE or not
280 % ; lookup(cbc_assertions_finished(NOW,no_counterexample_exists,_,_)
281 % \+ b_global_sets:unfixed_deferred_set(_)
282 % -> print('PROOF')
283 ; print('OK')
284 ),
285 print_times(NOW,StartTime,StartWTime),
286 fail.
287 check_log(_) :- nl.
288
289 lookup(Fact) :- on_exception(error(existence_error(_,_),_),call(Fact),fail).
290
291 print_times(NOW,StartTime,StartWTime) :-
292 start_animation(NOW,T1,W1),!,
293 print_sep,print_time(loading,StartTime,StartWTime,T1,W1),print_sep,
294 (lookup(cli_start_initialisation_failed(NOW,T2,W2))
295 -> print_time(checking_OK,T1,W1,T2,W2) % no counter-example found
296 ; lookup(cbc_assertions_finished(NOW,_,T2,W2))
297 -> print_time(checking,T1,W1,T2,W2) % counter-example found
298 ; lookup(finished_processing(NOW,T2,W2))
299 -> print_time(checking_ERR,T1,W1,T2,W2) % other error
300 ).
301 print_times(NOW,StartTime,StartWTime) :-
302 lookup(loading_failed(NOW,_Filename,T1,W1)),!,
303 print_sep,print_time(loading_failure,StartTime,StartWTime,T1,W1).
304
305
306 print_time(_Msg,Start,WStart,End,WEnd) :-
307 %print(Msg), print_sep,
308 T is End-Start, print(T), print(' ms'), print_sep,
309 W is WEnd-WStart, print(W), print(' ms').
310
311 %check_error_occurred(NOW,Err) :- on_exception(error(existence_error(_,_),_),
312 % error_occurred(NOW,Err), fail).
313 %check_loading_failed(NOW,Err) :- on_exception(error(existence_error(_,_),_),
314 % loading_failed(NOW,Err), fail).
315 %check_expected_error_did_not_occur(NOW,Err) :- on_exception(error(existence_error(_,_),_),
316 % expected_error_did_not_occur(NOW,Err), fail).
317
318 /*
319 Desired output:
320 <Prob>
321 <resultat> OK ou KO </resultat>
322 <commentaires> aficher les contradications </commentaires>
323 <temps> temps de traitement </temps>
324 </Prob>
325 */