1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2025-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(rule_validation,[setup_rules_extras/0, reset_rules_extras/0,
6 generate_html_report/1, generate_html_report/2, generate_html_report/3,
7 generate_dependency_graph/1]).
8
9 :- use_module(probsrc(module_information),[module_info/2]).
10 :- module_info(group,rules_dsl).
11 :- module_info(description,'This module provides functionality for the B Rules DSL.').
12
13 :- use_module(library(lists)).
14 :- use_module(library(aggregate),[forall/2]).
15 :- use_module(probsrc(bmachine),[bmachine_is_precompiled/0, get_machine_identifiers/2,
16 b_get_main_filename/1, b_get_definition_string_from_machine/2,
17 get_operation_info/2]).
18 :- use_module(probsrc(debug)).
19 :- use_module(probsrc(error_manager)).
20 :- use_module(probsrc(preferences),[get_preference/2]).
21 :- use_module(probsrc(specfile),[animation_minor_mode/1]).
22 :- use_module(probsrc(tools),[read_string_from_file/2, ajoin/2, get_tail_filename/2]).
23 :- use_module(probsrc(tools_io),[safe_open_file/4, with_open_stream_to_codes/4]).
24
25 :- dynamic computation/1, rule/1, dependencies/2, tags/2, classification/2, rule_id/2.
26 :- dynamic rule_report_template_file_codes/2.
27
28 assert_from_template(Filename) :-
29 absolute_file_name(rulesdslsrc(Filename), Absolute, []),
30 read_string_from_file(Absolute,String),
31 assertz(rule_report_template_file_codes(Filename,String)).
32
33 :- assert_from_template('validation_report_header.html').
34 :- assert_from_template('validation_report_footer.html').
35
36 write_rule_report_template(HtmlFile,Stream) :-
37 rule_report_template_file_codes(HtmlFile,Codes),
38 format(Stream,'~s~n',[Codes]).
39
40 setup_rules_extras :-
41 reset_rules_extras,
42 (animation_minor_mode(rules_dsl) -> true
43 ; b_get_main_filename(BFile),
44 add_error(rule_validation,'Cannot set up rules DSL mode, current machine is not a rules machine (.rmch): ',BFile),
45 fail),
46 (bmachine_is_precompiled -> true ; add_error(setup_rules_extras,'bmachine not precompiled'), fail),
47 get_machine_identifiers(operations,Ops),
48 get_machine_identifiers(variables,Vars),
49 forall(member(Op,Ops),
50 (extract_rule_operations(Op,Vars),
51 extract_dependencies(Op),
52 extract_operation_attributes(Op))), % tags, classification, rule_id
53 debug_println(19,'% setup for rules DSL complete.').
54
55 reset_rules_extras :-
56 retractall(computation(_)),
57 retractall(rule(_)),
58 retractall(dependencies(_,_)),
59 retractall(tags(_,_)),
60 retractall(classification(_,_)),
61 retractall(rule_id(_,_)).
62
63 extract_rule_operations(Id,Vars) :-
64 counterexample_name_from_id(Id,CId), % we could double check with successful
65 ? (member(CId,Vars) -> assertz(rule(Id)) ; assertz(computation(Id))).
66
67 counterexample_name_from_id(Id,CId) :- ajoin([Id,'_Counterexamples'],CId).
68 successful_name_from_id(Id,CId) :- ajoin([Id,'_Successful'],CId).
69 unchecked_name_from_id(Id,CId) :- ajoin([Id,'_Unchecked'],CId).
70
71 :- use_module(probsrc(b_operation_guards),[get_operation_propositional_guards/3]).
72 extract_dependencies(OpName) :-
73 get_operation_propositional_guards(OpName,Guards,_RestBody),
74 findall(Id, (member(Guard, Guards), is_rule_comp_dependency(Guard,Id)), Deps),
75 assertz(dependencies(OpName,Deps)).
76
77 is_rule_comp_dependency(b(equal(b(identifier(Id),string,_),b(string('SUCCESS'),string,_)),pred,_), Id) :- rule(Id).
78 is_rule_comp_dependency(b(equal(b(identifier(Id),string,_),b(string('EXECUTED'),string,_)),pred,_), Id) :- computation(Id).
79
80 extract_operation_attributes(OpName) :-
81 get_operation_info(OpName,Infos),
82 (member(rules_info(RInfos),Infos) -> true ; RInfos = []),
83 (member(tags(Tags),RInfos) -> assertz(tags(OpName,Tags)) ; true),
84 (member(classification(Classification),RInfos)
85 -> (classification(Classification,OpList)
86 -> retractall(classification(Classification,_)),
87 assertz(classification(Classification,[OpName|OpList]))
88 ; assertz(classification(Classification,[OpName])))
89 ; true),
90 (member(rule_id(RId),RInfos) -> assertz(rule_id(OpName,RId)) ; true).
91
92 get_computations(Comps) :- findall(X, computation(X), Comps).
93 get_rules(Rules) :- findall(X, rule(X), Rules).
94
95 get_simple_rule_status(BState,RuleName,Status) :-
96 rule(RuleName),
97 member(bind(RuleName,string(Status)),BState).
98 get_rule_status(BState,RuleName,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDeps) :-
99 rule(RuleName),
100 dependencies(RuleName,Deps),
101 member(bind(RuleName,string(Status)),BState), % rule status: NOT_CHECKED, DISABLED, FAIL, SUCCESS
102 include(get_failed_dependencies(BState),Deps,FailDep),
103 include(get_not_executed_dependencies(BState),Deps,NotExecDeps),
104 get_rule_counterexamples(RuleName,BState,CounterEx),
105 get_rule_success_messages(RuleName,BState,SuccessMsg),
106 get_rule_unchecked_messages(RuleName,BState,UncheckedMsg).
107
108 get_simple_computation_status(BState,CompName,Status) :-
109 computation(CompName),
110 member(bind(CompName,string(Status)),BState).
111
112 get_failed_dependencies(State,Dep) :-
113 rule(Dep),
114 member(bind(Dep,string('FAIL')),State).
115
116 get_not_executed_dependencies(State,Dep) :-
117 member(bind(Dep,string(DepStatus)),State),
118 (DepStatus = 'DISABLED' ;
119 (rule(Dep)
120 -> DepStatus = 'NOT_CHECKED'
121 ; DepStatus = 'NOT_EXECUTED')).
122
123 get_rule_counterexamples(RuleName,State,CounterEx) :-
124 counterexample_name_from_id(RuleName,CId),
125 evaluate_rule_results(CId,State,CounterEx).
126
127 get_rule_success_messages(RuleName,State,SuccessMsg) :-
128 successful_name_from_id(RuleName,SId),
129 evaluate_rule_results(SId,State,SuccessMsg).
130
131 get_rule_unchecked_messages(RuleName,State,UncheckedMsg) :-
132 unchecked_name_from_id(RuleName,UId),
133 evaluate_rule_results(UId,State,UncheckedMsg).
134
135 evaluate_rule_results(Id,State,RuleRes) :-
136 member(bind(Id,RR0),State),
137 custom_explicit_sets:expand_custom_set_to_list(RR0,RR1), % TODO: enumeration warning (infinitely many messages)
138 maplist(extract_rule_result,RR1,RuleRes).
139
140 extract_rule_result((int(ErrorCode),string(ResultStr)),rule_result(ErrorCode,ResultStr)).
141
142 :- use_module(probsrc(state_space),[current_state_id/1,visited_expression/2]).
143 :- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/1,extract_variables_from_state/2]).
144 get_variables_for_export(StateID,VarState) :-
145 visited_expression(StateID,State),
146 state_corresponds_to_initialised_b_machine(State),!,
147 extract_variables_from_state(State,VarState).
148 get_variables_for_export(_,_) :-
149 add_error(rule_validation,'Cannot export rule validation results for uninitialised state'), fail.
150
151 %%%%%%%%% BEGIN HTML REPORT %%%%%%%%%%
152 generate_html_report(File) :- generate_html_report(File,[]). % /1 default (for current state)
153 generate_html_report(File,Options) :- % /2 current state with options
154 current_state_id(ID),
155 generate_html_report(ID,File,Options).
156 generate_html_report(StateID,File,Options) :- % /3 any state with options TODO: language option
157 (animation_minor_mode(rules_dsl) -> true
158 ; b_get_main_filename(BFile),
159 add_error(rule_validation,'Cannot create rule validation report, is not a rules machine (.rmch): ',BFile),
160 fail),
161 get_variables_for_export(StateID,VarState),
162 safe_open_file(File,write,Stream,[encoding(utf8)]),
163 generate_html_to_stream(Stream,VarState,[html_file/File|Options]),
164 close(Stream),
165 formatsilent('% created rule validation report at ~w.~n',[File]).
166
167 :- use_module(probsrc(runtime_profiler),[tcltk_get_operations_profile_info/1]).
168 :- use_module(library(system),[datime/1]).
169 :- use_module(probsrc(tools_strings),[number_codes_min_length/3]).
170 :- use_module(probsrc(version),[version_str/1,revision/1]).
171 generate_html_to_stream(Stream,State,Options) :-
172 write_rule_report_template('validation_report_header.html',Stream),
173 get_rules(Rules),
174 (get_preference(prob_profiling_on,true)
175 -> tcltk_get_operations_profile_info(list(ProfileList)),
176 get_total_walltime(ProfileList,TotalWT)
177 ; ProfileList = [],
178 (member(checktime(TotalWT),Options) -> true ; TotalWT = -1) % option to provide checktime from ProB2 if profiling is off
179 ),
180 gen_report_infos(Stream,Rules,State),
181 forall(classification(CName,OpList),gen_classifications(Stream,CName,OpList,State,ProfileList)),
182 format(Stream,' <div class="rule-list normal">~n',[]),
183 forall((member(Rule,Rules), \+ (classification(_,OpList), member(Rule,OpList))), % all rules w/o classification
184 gen_rule_result(Stream,Rule,State,ProfileList)),
185 format(Stream,' </div>~n',[]),
186 (TotalWT > 0 -> convert_ms_s(TotalWT,WTPrint), format(Stream,' Check finished after: ~w~n',[WTPrint]) ; true),
187 version_str(VStr), revision(VRev),
188 format(Stream,' <br>ProB Version: ~w (~w)~n',[VStr,VRev]),
189 datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
190 number_codes_min_length(Min,2,MC),
191 format(Stream,' <br>Generated on ~w/~w/~w at ~w:~s~n',[Day,Mon,Yr,Hr,MC]),
192 write_rule_report_template('validation_report_footer.html',Stream).
193
194 gen_report_infos(Stream,Rules,BState) :-
195 length(Rules,NrRules),
196 precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD),
197 b_get_main_filename(Filename),
198 get_tail_filename(Filename,MName),
199 format(Stream,' Checked machine: <b>~w</b>~n',[MName]),
200 (b_get_definition_string_from_machine('RULE_REPORT_CONTEXT',RepCtx)
201 -> format(Stream,' <br>With context: <b>~w</b>~n',[RepCtx])
202 ; true),
203 format(Stream,' <div style="line-height:25px;">~n',[]),
204 format(Stream,' <br>Total number of rules: <b>~w</b>~n',[NrRules]),
205 format(Stream,' <br>Number of checked rules: <b>~w</b>~n',[NrC]),
206 format(Stream,' <br>Number of successful rules: <b>~w</b>~n',[NrS]),
207 format(Stream,' <br>Number of failed rules: <b>~w</b>~n',[NrF]),
208 format(Stream,' <br>Number of disabled rules: <b>~w</b>~n',[NrD]),
209 format(Stream,' </div>~n',[]),
210 format(Stream,' <br>~n',[]).
211
212 get_total_walltime([_|T],WT) :- get_total_walltime1(T,WT). % ignore table legend
213 get_total_walltime1([],0).
214 get_total_walltime1([list([_,_,WT0,_,_,_,_])|T],WT) :-
215 get_total_walltime1(T,WT1),
216 WT is WT0+WT1.
217
218 precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD) :-
219 maplist(get_simple_rule_status(BState), Rules, Statuses),
220 count_statuses(Statuses,NrS,NrF,NrD),
221 NrC is NrS+NrF.
222
223 count_statuses([],0,0,0).
224 count_statuses([Status|T],NrS,NrF,NrD) :-
225 count_statuses(T,S,F,D),
226 (Status = 'SUCCESS' -> NrS is S+1 ; NrS = S),
227 (Status = 'FAIL' -> NrF is F+1 ; NrF = F),
228 (Status = 'DISABLED' -> NrD is D+1 ; NrD = D).
229
230 gen_classifications(Stream,CName,OpList,BState,ProfileList) :-
231 format(Stream,' <div class="classification-list">~n',[]),
232 format(Stream,' <div class="classification-header" onclick="openDetails(\'classification_~w\')">~n',[CName]),
233 length(OpList,NrOps),
234 format(Stream,' <b>~w</b> (~w)~n',[CName,NrOps]),
235 format(Stream,' </div>~n',[]),
236 format(Stream,' <div class="rule-list classification" id="classification_~w">~n',[CName]),
237 forall(member(Rule,OpList), gen_rule_result(Stream,Rule,BState,ProfileList)),
238 format(Stream,' </div>~n',[]),
239 format(Stream,' </div>~n',[]),
240 format(Stream,' </div>~n',[]).
241
242 gen_rule_result(Stream,Rule,BState,ProfileList) :-
243 get_rule_status(BState,Rule,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep),
244 (Status = 'SUCCESS'
245 -> ((SuccessMsg \= [] ; UncheckedMsg \= [])
246 -> format(Stream,' <div class="rule-header pointer green" onclick="openDetails(\'~w\')">~n',[Rule])
247 ; format(Stream,' <div class="rule-header green">~n',[]))
248 ; Status = 'FAIL'
249 -> format(Stream,' <div class="rule-header pointer red" onclick="openDetails(\'~w\')">~n',[Rule]),
250 format(Stream,' <span class="icon">⚠</span>~n',[])
251 ; Status = 'DISABLED' -> format(Stream,' <div class="rule-header grey">~n',[])
252 ; Status = 'NOT_CHECKED'
253 -> ((FailDep \= [] ; NotExecDep \= [])
254 -> (FailDep \= [] -> C = 'orange' ; C = 'lightgrey'), % FAIL dependencies: orange, else grey
255 P = 'pointer'
256 ; C = 'white', P = '' % no conflicts with dependencies
257 ),
258 format(Stream,' <div class="rule-header ~w ~w" onclick="openDetails(\'~w\')">~n',[P,C,Rule]),
259 (C = 'orange' -> format(Stream,' <span class="icon">⚠</span>~n',[]) ; true)
260 ; format(Stream,' <div class="rule-header">~n',[])
261 ),
262 format(Stream,' ~w',[Rule]),
263 (rule_id(Rule,RuleId)
264 -> format(Stream,' [~w]~n',[RuleId])
265 ; format(Stream,'~n',[])),
266 (tags(Rule,Tags)
267 -> format(Stream,' ~n',[]),
268 forall(member(Tag,Tags), format(Stream,' <div class="tag">~w</div>~n',[Tag])),
269 format(Stream,' ~n',[])
270 ; true),
271 format(Stream,' <b>~w</b>~n',[Status]),
272 (member(list([Rule,_,WT,_,_,_,_]),ProfileList)
273 -> convert_ms_s(WT,WTPrint),
274 format(Stream,' <span style="float: right;"><em>(~w)</em></span>~n',[WTPrint])
275 ; true), % ignore if not available
276 format(Stream,' </div>~n',[]),
277 gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep),
278 fail.
279 gen_rule_result(_Stream,_,_,_).
280
281 convert_ms_s(Time,CTime) :- Time >= 1000 -> TimeSec is Time/1000, ajoin([TimeSec,' s'],CTime) ; ajoin([Time,' ms'],CTime).
282
283 gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep) :-
284 length(CounterEx,CELen),
285 length(SuccessMsg,SMLen),
286 length(UncheckedMsg,UCLen),
287 length(FailDep,FDLen),
288 length(NotExecDep,NEDLen),
289 ((CELen > 0 ; SMLen > 0 ; UCLen > 0 ; FDLen > 0 ; NEDLen > 0) % create tag only if at least one child exists
290 -> format(Stream,' <div class="rule-content" id="~w">~n',[Rule]),
291 (CELen > 0
292 -> format(Stream,' <b>~w</b> Violations found:~n',[CELen]),
293 format(Stream,' <ul>~n',[]),
294 forall(member(CE,CounterEx),gen_rule_content_list_aux(Stream,CE)),
295 format(Stream,' </ul>~n',[])
296 ; true
297 ),
298 (SMLen > 0
299 -> format(Stream,' <b>~w</b> successful checks:~n',[SMLen]),
300 format(Stream,' <ul>~n',[]),
301 forall(member(SM,SuccessMsg),gen_rule_content_list_aux(Stream,SM)),
302 format(Stream,' </ul>~n',[])
303 ; true
304 ),
305 (UCLen > 0
306 -> format(Stream,' <b>~w</b> unchecked items:~n',[UCLen]),
307 format(Stream,' <ul>~n',[]),
308 forall(member(UC,UncheckedMsg),gen_rule_content_list_aux(Stream,UC)),
309 format(Stream,' </ul>~n',[])
310 ; true
311 ),
312 (FDLen > 0
313 -> format(Stream,' Rule could not be checked due to ~w failed dependencies:~n',[FDLen]),
314 format(Stream,' <ul>~n',[]),
315 forall(member(FD,FailDep),gen_rule_content_list_aux(Stream,FD)),
316 format(Stream,' </ul>~n',[])
317 ; true
318 ),
319 (NEDLen > 0
320 -> format(Stream,' Rule could not be checked due to ~w unchecked dependencies:~n',[NEDLen]),
321 format(Stream,' <ul>~n',[]),
322 forall(member(NED,NotExecDep),gen_rule_content_list_aux(Stream,NED)),
323 format(Stream,' </ul>~n',[])
324 ; true
325 ),
326 format(Stream,' </div>~n',[])
327 ; true),
328 fail.
329 gen_rule_content_list(_,_,_,_,_,_,_).
330
331 gen_rule_content_list_aux(Stream,rule_result(ErrorCode,Message)) :- !,
332 format(Stream,' <li>(~w) ~w</li>~n',[ErrorCode,Message]).
333 gen_rule_content_list_aux(Stream,Dependency) :-
334 format(Stream,' <li>~w</li>~n',[Dependency]).
335
336 % TODO:
337 % Violations cannot be enumerated (infinitely many).
338 % Successful checks cannot be enumerated (infinitely many).
339 %%%%%%%%% END HTML REPORT %%%%%%%%%%
340
341 %%%%%%%%% BEGIN DEPENDENCY GRAPH %%%%%%%%%
342 % TODO: tooltip with counterexample?
343 :- use_module(probsrc(state_space),[current_expression/2]).
344 :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3,use_new_dot_attr_pred/7]).
345 generate_dependency_graph(File) :-
346 (animation_minor_mode(rules_dsl) -> true
347 ; b_get_main_filename(BFile),
348 add_error(rule_validation,'Cannot create rule dependency graph, is not a rules machine (.rmch): ',BFile),
349 fail),
350 current_state_id(CurID),
351 get_variables_for_export(CurID,VarState),
352 gen_dot_graph(File,
353 use_new_dot_attr_pred(rule_validation:rule_graph_node_predicate(VarState)),
354 use_new_dot_attr_pred(rule_validation:rule_graph_trans_predicate(VarState))).
355
356 rule_graph_node_predicate(State,OpName,none,[style/'filled',label/OpName,tooltip/OpName|Attr]) :-
357 dependencies(OpName,_), % all relevant operations
358 get_node_attributes(State,OpName,Attr).
359
360 get_node_attributes(State,OpName,[shape/RShape,fillcolor/StatusColor,tooltip/Tooltip]) :-
361 get_simple_rule_status(State,OpName,Status), !,
362 get_preference(rule_graph_shape,RShape),
363 (Status = 'FAIL' -> get_preference(failed_rule_colour,StatusColor) ;
364 Status = 'SUCCESS' -> get_preference(successful_rule_colour,StatusColor) ;
365 Status = 'DISABLED' -> get_preference(disabled_rule_colour,StatusColor) ;
366 get_preference(not_checked_rule_colour,StatusColor)), % NOT_CHECKED, TODO: maybe UNCHECKED
367 ajoin(['Rule: ',OpName,', Status: ',Status],Tooltip).
368 get_node_attributes(State,OpName,[shape/CompShape,fillcolor/StatusColor,tooltip/Tooltip]) :-
369 get_simple_computation_status(State,OpName,Status), !,
370 get_preference(computation_graph_shape,CompShape),
371 (Status = 'EXECUTED' -> get_preference(executed_computation_colour,StatusColor) ;
372 Status = 'COMPUTATION_DISABLED' -> get_preference(disabled_computation_colour,StatusColor) ;
373 get_preference(not_executed_computation_colour,StatusColor)), % NOT_EXECUTED
374 ajoin(['Computation: ',OpName,', Status: ',Status],Tooltip).
375
376 rule_graph_trans_predicate(State,NodeID,SuccID,[label/''|Attr]) :-
377 dependencies(NodeID,Deps),
378 member(SuccID,Deps),
379 get_trans_attributes(State,SuccID,Attr).
380
381 get_trans_attributes(State,DepName,[color/StatusColor,tooltip/Tooltip]) :-
382 get_simple_rule_status(State,DepName,Status), !,
383 ((Status = 'FAIL' ; Status = 'DISABLED')
384 -> get_preference(failed_dependency_colour,StatusColor), TTStatus = ' is not available.' ;
385 Status = 'SUCCESS' -> get_preference(succeeded_dependency_colour,StatusColor), TTStatus = ' is available.' ;
386 get_preference(normal_dependency_colour,StatusColor), TTStatus = ' is available.'), % NOT_CHECKED
387 ajoin(['Required rule ',DepName,' with status ',Status,TTStatus],Tooltip).
388 get_trans_attributes(State,DepName,[color/StatusColor,tooltip/Tooltip]) :-
389 get_simple_computation_status(State,DepName,Status), !,
390 (Status = 'COMPUTATION_DISABLED' -> get_preference(failed_dependency_colour,StatusColor), TTStatus = ' is not available.' ;
391 get_preference(normal_dependency_colour,StatusColor), TTStatus = ' is available.'),
392 ajoin(['Required computation ',DepName,' with status ',Status,TTStatus],Tooltip).
393 %%%%%%%%% END DEPENDENCY GRAPH %%%%%%%%%