| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2025-2026 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_report/1, generate_report/2, generate_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, split_filename/3]). | |
| 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 REPORT %%%%%%%%%% | |
| 152 | generate_report(File) :- generate_report(File,[]). % /1 default (for current state) | |
| 153 | generate_report(File,Options) :- % /2 current state with options | |
| 154 | current_state_id(ID), | |
| 155 | generate_report(ID,File,Options). | |
| 156 | generate_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 | (get_preference(prob_profiling_on,true) | |
| 163 | -> tcltk_get_operations_profile_info(list(ProfileList)), | |
| 164 | get_total_walltime(ProfileList,TotalWT) | |
| 165 | ; ProfileList = [], | |
| 166 | (member(checktime(TotalWT),Options) -> true ; TotalWT = -1) % option to provide checktime from ProB2 if profiling is off | |
| 167 | ), | |
| 168 | safe_open_file(File,write,Stream,[encoding(utf8)]), | |
| 169 | split_filename(File,_Base,Ext), % infer report mode from file extension | |
| 170 | (Ext=html -> generate_html_to_stream(Stream,VarState,Options,TotalWT,ProfileList) ; | |
| 171 | Ext=xml -> generate_xml_to_stream(Stream,VarState,Options,TotalWT,ProfileList) ; | |
| 172 | add_error(rule_validation,'unsupported output type for rule validation report: ',Ext)), | |
| 173 | close(Stream), | |
| 174 | formatsilent('% created rule validation report at ~w.~n',[File]). | |
| 175 | ||
| 176 | %%%%%%%%% BEGIN HTML REPORT %%%%%%%%%% | |
| 177 | :- use_module(probsrc(runtime_profiler),[tcltk_get_operations_profile_info/1]). | |
| 178 | :- use_module(library(system),[datime/1]). | |
| 179 | :- use_module(probsrc(bmachine),[b_get_operation_description/2]). | |
| 180 | :- use_module(probsrc(tools),[html_escape/2]). | |
| 181 | :- use_module(probsrc(tools_strings),[number_codes_min_length/3]). | |
| 182 | :- use_module(probsrc(version),[version_str/1,revision/1]). | |
| 183 | generate_html_to_stream(Stream,State,_Options,TotalWT,ProfileList) :- | |
| 184 | write_rule_report_template('validation_report_header.html',Stream), | |
| 185 | get_rules(Rules), | |
| 186 | gen_report_infos(Stream,Rules,State), | |
| 187 | forall(classification(CName,OpList),gen_classifications(Stream,CName,OpList,State,ProfileList)), | |
| 188 | format(Stream,' <div class="rule-list normal">~n',[]), | |
| 189 | forall((member(Rule,Rules), \+ (classification(_,OpList), member(Rule,OpList))), % all rules w/o classification | |
| 190 | gen_rule_result(Stream,Rule,State,ProfileList)), | |
| 191 | format(Stream,' </div>~n',[]), | |
| 192 | (TotalWT > 0 -> convert_ms_s(TotalWT,WTPrint), format(Stream,' Check finished after: ~w~n',[WTPrint]) ; true), | |
| 193 | version_str(VStr), revision(VRev), | |
| 194 | format(Stream,' <br>ProB Version: ~w (~w)~n',[VStr,VRev]), | |
| 195 | datime_min_length_codes(datime(Yr,Mon,Day,Hr,Min,_Sec)), | |
| 196 | format(Stream,' <br>Generated on ~s/~s/~s at ~s:~s~n',[Day,Mon,Yr,Hr,Min]), | |
| 197 | write_rule_report_template('validation_report_footer.html',Stream). | |
| 198 | ||
| 199 | datime_min_length_codes(datime(YrC,MonC,DC,HC,MC,SC)) :- | |
| 200 | datime(datime(Yr,Mon,Day,Hr,Min,Sec)), | |
| 201 | number_codes_min_length(Yr,4,YrC), | |
| 202 | number_codes_min_length(Mon,2,MonC), | |
| 203 | number_codes_min_length(Day,2,DC), | |
| 204 | number_codes_min_length(Hr,2,HC), | |
| 205 | number_codes_min_length(Min,2,MC), | |
| 206 | number_codes_min_length(Sec,2,SC). | |
| 207 | ||
| 208 | gen_report_infos(Stream,Rules,BState) :- | |
| 209 | length(Rules,NrRules), | |
| 210 | precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD), | |
| 211 | b_get_main_filename(Filename), | |
| 212 | get_tail_filename(Filename,MName), | |
| 213 | format(Stream,' Checked machine: <b>~w</b>~n',[MName]), | |
| 214 | (b_get_definition_string_from_machine('RULE_REPORT_CONTEXT',RepCtx) | |
| 215 | -> format(Stream,' <br>With context: <b>~w</b>~n',[RepCtx]) | |
| 216 | ; true), | |
| 217 | format(Stream,' <div style="line-height:25px;">~n',[]), | |
| 218 | format(Stream,' <br>Total number of rules: <b>~w</b>~n',[NrRules]), | |
| 219 | format(Stream,' <br>Number of checked rules: <b>~w</b>~n',[NrC]), | |
| 220 | format(Stream,' <br>Number of successful rules: <b>~w</b>~n',[NrS]), | |
| 221 | format(Stream,' <br>Number of failed rules: <b>~w</b>~n',[NrF]), | |
| 222 | format(Stream,' <br>Number of disabled rules: <b>~w</b>~n',[NrD]), | |
| 223 | format(Stream,' </div>~n',[]), | |
| 224 | format(Stream,' <br>~n',[]). | |
| 225 | ||
| 226 | get_total_walltime([_|T],WT) :- get_total_walltime1(T,WT). % ignore table legend | |
| 227 | get_total_walltime1([],0). | |
| 228 | get_total_walltime1([list([_,_,WT0,_,_,_,_])|T],WT) :- | |
| 229 | get_total_walltime1(T,WT1), | |
| 230 | WT is WT0+WT1. | |
| 231 | ||
| 232 | precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD) :- | |
| 233 | maplist(get_simple_rule_status(BState), Rules, Statuses), | |
| 234 | count_statuses(Statuses,NrS,NrF,NrD), | |
| 235 | NrC is NrS+NrF. | |
| 236 | ||
| 237 | count_statuses([],0,0,0). | |
| 238 | count_statuses([Status|T],NrS,NrF,NrD) :- | |
| 239 | count_statuses(T,S,F,D), | |
| 240 | (Status = 'SUCCESS' -> NrS is S+1 ; NrS = S), | |
| 241 | (Status = 'FAIL' -> NrF is F+1 ; NrF = F), | |
| 242 | (Status = 'DISABLED' -> NrD is D+1 ; NrD = D). | |
| 243 | ||
| 244 | gen_classifications(Stream,CName,OpList,BState,ProfileList) :- | |
| 245 | count_rule_status(BState,OpList,NrSuccess,NrFail,NrUncheck), | |
| 246 | (NrFail \= 0 -> CColour = cred ; NrUncheck \= 0 -> CColour = '' ; CColour = cgreen), | |
| 247 | format(Stream,' <div class="classification-list">~n',[]), | |
| 248 | format(Stream,' <div class="classification-header ~w" onclick="openDetails(\'classification_~w\')">~n',[CColour,CName]), | |
| 249 | length(OpList,NrOps), | |
| 250 | P is round(NrSuccess*1000 / NrOps), | |
| 251 | Percentage is P/10, | |
| 252 | format(Stream,' <b>~w</b> ~w % (~w/~w)~n',[CName,Percentage,NrSuccess,NrOps]), | |
| 253 | format(Stream,' </div>~n',[]), | |
| 254 | format(Stream,' <div class="rule-list classification" id="classification_~w">~n',[CName]), | |
| 255 | forall(member(Rule,OpList), gen_rule_result(Stream,Rule,BState,ProfileList)), | |
| 256 | format(Stream,' </div>~n',[]), | |
| 257 | format(Stream,' </div>~n',[]), | |
| 258 | format(Stream,' </div>~n',[]). | |
| 259 | ||
| 260 | count_rule_status(_,[],0,0,0). | |
| 261 | count_rule_status(BState,[Op|TOp],NewSuccess,NewFail,NewUncheck) :- | |
| 262 | get_rule_status(BState,Op,Status,_,_,_,_,_), | |
| 263 | ( Status = 'SUCCESS' -> | |
| 264 | S1 = 1, F1 = 0, U1 = 0 | |
| 265 | ; Status = 'FAIL' -> | |
| 266 | S1 = 0, F1 = 1, U1 = 0 | |
| 267 | ; % DISABLED / NOT_CHECKED | |
| 268 | S1 = 0, F1 = 0, U1 = 1 | |
| 269 | ), | |
| 270 | count_rule_status(BState,TOp,S2,F2,U2), | |
| 271 | NewSuccess is S1 + S2, | |
| 272 | NewFail is F1 + F2, | |
| 273 | NewUncheck is U1 + U2. | |
| 274 | ||
| 275 | gen_rule_result(Stream,Rule,BState,ProfileList) :- | |
| 276 | get_rule_status(BState,Rule,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep), | |
| 277 | (Status = 'SUCCESS' | |
| 278 | -> ((SuccessMsg \= [] ; UncheckedMsg \= []) | |
| 279 | -> format(Stream,' <div class="rule-header pointer green" onclick="openDetails(\'~w\')">~n',[Rule]) | |
| 280 | ; format(Stream,' <div class="rule-header green">~n',[])) | |
| 281 | ; Status = 'FAIL' | |
| 282 | -> format(Stream,' <div class="rule-header pointer red" onclick="openDetails(\'~w\')">~n',[Rule]), | |
| 283 | format(Stream,' <span class="icon">⚠</span>~n',[]) | |
| 284 | ; Status = 'DISABLED' -> format(Stream,' <div class="rule-header grey">~n',[]) | |
| 285 | ; Status = 'NOT_CHECKED' | |
| 286 | -> ((FailDep \= [] ; NotExecDep \= []) | |
| 287 | -> (FailDep \= [] -> C = 'orange' ; C = 'lightgrey'), % FAIL dependencies: orange, else grey | |
| 288 | P = 'pointer' | |
| 289 | ; C = 'white', P = '' % no conflicts with dependencies | |
| 290 | ), | |
| 291 | format(Stream,' <div class="rule-header ~w ~w" onclick="openDetails(\'~w\')">~n',[P,C,Rule]), | |
| 292 | (C = 'orange' -> format(Stream,' <span class="icon">⚠</span>~n',[]) ; true) | |
| 293 | ; format(Stream,' <div class="rule-header">~n',[]) | |
| 294 | ), | |
| 295 | format(Stream,' ~w',[Rule]), | |
| 296 | (rule_id(Rule,RuleId) | |
| 297 | -> format(Stream,' [~w]~n',[RuleId]) | |
| 298 | ; format(Stream,'~n',[])), | |
| 299 | (tags(Rule,Tags) | |
| 300 | -> format(Stream,' ~n',[]), | |
| 301 | forall(member(Tag,Tags), format(Stream,' <div class="tag">~w</div>~n',[Tag])), | |
| 302 | format(Stream,' ~n',[]) | |
| 303 | ; true), | |
| 304 | format(Stream,' <b>~w</b>~n',[Status]), | |
| 305 | (b_get_operation_description(Rule,Desc) | |
| 306 | -> format(Stream,' <span class="tooltip-trigger">?</span>~n',[]), | |
| 307 | html_escape(Desc,EDesc), | |
| 308 | format(Stream,' <span class="tooltip">~w</span>~n',[EDesc]) | |
| 309 | ; true), | |
| 310 | (member(list([Rule,_,WT,_,_,_,_]),ProfileList) | |
| 311 | -> convert_ms_s(WT,WTPrint), | |
| 312 | format(Stream,' <span style="float: right;"><em>(~w)</em></span>~n',[WTPrint]) | |
| 313 | ; true), % ignore if not available | |
| 314 | format(Stream,' </div>~n',[]), | |
| 315 | gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep), | |
| 316 | fail. | |
| 317 | gen_rule_result(_Stream,_,_,_). | |
| 318 | ||
| 319 | convert_ms_s(Time,CTime) :- Time >= 1000 -> TimeSec is Time/1000, ajoin([TimeSec,' s'],CTime) ; ajoin([Time,' ms'],CTime). | |
| 320 | ||
| 321 | gen_rule_content_list(Stream,Rule,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep) :- | |
| 322 | length(CounterEx,CELen), | |
| 323 | length(SuccessMsg,SMLen), | |
| 324 | length(UncheckedMsg,UCLen), | |
| 325 | length(FailDep,FDLen), | |
| 326 | length(NotExecDep,NEDLen), | |
| 327 | ((CELen > 0 ; SMLen > 0 ; UCLen > 0 ; FDLen > 0 ; NEDLen > 0) % create tag only if at least one child exists | |
| 328 | -> format(Stream,' <div class="rule-content" id="~w">~n',[Rule]), | |
| 329 | (CELen > 0 | |
| 330 | -> format(Stream,' <b>~w</b> Violations found:~n',[CELen]), | |
| 331 | format(Stream,' <ul>~n',[]), | |
| 332 | forall(member(CE,CounterEx),gen_rule_content_list_aux(Stream,CE)), | |
| 333 | format(Stream,' </ul>~n',[]) | |
| 334 | ; true | |
| 335 | ), | |
| 336 | (SMLen > 0 | |
| 337 | -> format(Stream,' <b>~w</b> successful checks:~n',[SMLen]), | |
| 338 | format(Stream,' <ul>~n',[]), | |
| 339 | forall(member(SM,SuccessMsg),gen_rule_content_list_aux(Stream,SM)), | |
| 340 | format(Stream,' </ul>~n',[]) | |
| 341 | ; true | |
| 342 | ), | |
| 343 | (UCLen > 0 | |
| 344 | -> format(Stream,' <b>~w</b> unchecked items:~n',[UCLen]), | |
| 345 | format(Stream,' <ul>~n',[]), | |
| 346 | forall(member(UC,UncheckedMsg),gen_rule_content_list_aux(Stream,UC)), | |
| 347 | format(Stream,' </ul>~n',[]) | |
| 348 | ; true | |
| 349 | ), | |
| 350 | (FDLen > 0 | |
| 351 | -> format(Stream,' Rule could not be checked due to ~w failed dependencies:~n',[FDLen]), | |
| 352 | format(Stream,' <ul>~n',[]), | |
| 353 | forall(member(FD,FailDep),gen_rule_content_list_aux(Stream,FD)), | |
| 354 | format(Stream,' </ul>~n',[]) | |
| 355 | ; true | |
| 356 | ), | |
| 357 | (NEDLen > 0 | |
| 358 | -> format(Stream,' Rule could not be checked due to ~w unchecked dependencies:~n',[NEDLen]), | |
| 359 | format(Stream,' <ul>~n',[]), | |
| 360 | forall(member(NED,NotExecDep),gen_rule_content_list_aux(Stream,NED)), | |
| 361 | format(Stream,' </ul>~n',[]) | |
| 362 | ; true | |
| 363 | ), | |
| 364 | format(Stream,' </div>~n',[]) | |
| 365 | ; true), | |
| 366 | fail. | |
| 367 | gen_rule_content_list(_,_,_,_,_,_,_). | |
| 368 | ||
| 369 | gen_rule_content_list_aux(Stream,rule_result(ErrorCode,Message)) :- !, | |
| 370 | format(Stream,' <li>(~w) ~w</li>~n',[ErrorCode,Message]). | |
| 371 | gen_rule_content_list_aux(Stream,Dependency) :- | |
| 372 | format(Stream,' <li>~w</li>~n',[Dependency]). | |
| 373 | ||
| 374 | % TODO: | |
| 375 | % Violations cannot be enumerated (infinitely many). | |
| 376 | % Successful checks cannot be enumerated (infinitely many). | |
| 377 | %%%%%%%%% END HTML REPORT %%%%%%%%%% | |
| 378 | ||
| 379 | %%%%%%%%% BEGIN XML REPORT %%%%%%%%% | |
| 380 | generate_xml_to_stream(Stream,State,_Options,TotalWT,ProfileList) :- | |
| 381 | get_rules(Rules), | |
| 382 | format(Stream,'<ruleValidationReport>~n',[]), | |
| 383 | gen_xml_report_statistics(Stream,Rules,State,TotalWT), | |
| 384 | forall(classification(CName,OpList),gen_xml_classifications(Stream,CName,OpList,State,ProfileList)), | |
| 385 | forall((member(Rule,Rules), \+ (classification(_,OpList), member(Rule,OpList))), % all rules w/o classification | |
| 386 | gen_xml_rule_result(Stream,Rule,State,ProfileList)), | |
| 387 | format(Stream,'</ruleValidationReport>~n',[]). | |
| 388 | ||
| 389 | gen_xml_report_statistics(Stream,Rules,BState,TotalWT) :- | |
| 390 | length(Rules,NrRules), | |
| 391 | precollect_statuses(Rules,BState,NrC,NrS,NrF,NrD), | |
| 392 | format(Stream,' <statistics>~n',[]), | |
| 393 | b_get_main_filename(Filename), | |
| 394 | get_tail_filename(Filename,MName), | |
| 395 | format(Stream,' <checkedMachine>~w</checkedMachine>~n',[MName]), | |
| 396 | (b_get_definition_string_from_machine('RULE_REPORT_CONTEXT',RepCtx) | |
| 397 | -> format(Stream,' <context>~w</context>~n',[RepCtx]) | |
| 398 | ; true), | |
| 399 | format(Stream,' <totalNumber>~w</totalNumber>~n',[NrRules]), | |
| 400 | format(Stream,' <checked>~w</checked>~n',[NrC]), | |
| 401 | format(Stream,' <succeeded>~w</succeeded>~n',[NrS]), | |
| 402 | format(Stream,' <failed>~w</failed>~n',[NrF]), | |
| 403 | format(Stream,' <disabled>~w</disabled>~n',[NrD]), | |
| 404 | format(Stream,' <checkTime>~w</checkTime>~n',[TotalWT]), | |
| 405 | version_str(VStr), revision(VRev), | |
| 406 | format(Stream,' <proBVersion>~w (~w)</proBVersion>~n',[VStr,VRev]), | |
| 407 | datime_min_length_codes(datime(Yr,Mon,Day,Hr,Min,Sec)), | |
| 408 | format(Stream,' <date>~s-~s-~sT~s:~s:~s</date>~n',[Yr,Mon,Day,Hr,Min,Sec]), | |
| 409 | format(Stream,' </statistics>~n',[]). | |
| 410 | ||
| 411 | gen_xml_classifications(Stream,CName,OpList,BState,ProfileList) :- | |
| 412 | length(OpList,NrOps), | |
| 413 | format(Stream,' <classification name="~w" nrRules="~w">~n',[CName,NrOps]), | |
| 414 | forall(member(Rule,OpList), gen_xml_rule_result(Stream,Rule,BState,ProfileList)), | |
| 415 | format(Stream,' </classification>~n',[]). | |
| 416 | ||
| 417 | gen_xml_rule_result(Stream,Rule,BState,ProfileList) :- | |
| 418 | get_rule_status(BState,Rule,Status,CounterEx,SuccessMsg,UncheckedMsg,FailDep,NotExecDep), | |
| 419 | (rule_id(Rule,RID) | |
| 420 | -> format(Stream,' <rule name="~w" status="~w" id="~w">~n',[Rule,Status,RID]) | |
| 421 | ; format(Stream,' <rule name="~w" status="~w">~n',[Rule,Status])), | |
| 422 | (b_get_operation_description(Rule,Desc) | |
| 423 | -> html_escape(Desc,EDesc), | |
| 424 | format(Stream,' <description>~w</description>~n',[EDesc]) | |
| 425 | ; true), | |
| 426 | (tags(Rule,Tags) | |
| 427 | -> forall(member(Tag,Tags), format(Stream,' <tag>~w</tag>~n',[Tag])) | |
| 428 | ; true), | |
| 429 | forall(member(rule_result(ErrId,Msg),CounterEx), format(Stream,' <counterExample errorType="~w">~w</counterExample>~n',[ErrId,Msg])), | |
| 430 | forall(member(rule_result(BodyId,Msg),SuccessMsg), format(Stream,' <successMessage ruleBody="~w">~w</successMessage>~n',[BodyId,Msg])), | |
| 431 | forall(member(rule_result(BodyId,Msg),UncheckedMsg), format(Stream,' <uncheckedMessage ruleBody="~w">~w</uncheckedMessage>~n',[BodyId,Msg])), | |
| 432 | forall(member(FD,FailDep), format(Stream,' <failedDependency>~w</failedDependency>~n',[FD])), | |
| 433 | forall(member(NED,NotExecDep), format(Stream,' <notCheckedDependency>~w</notCheckedDependency>~n',[NED])), | |
| 434 | (member(list([Rule,_,WT,_,_,_,_]),ProfileList) | |
| 435 | -> format(Stream,' <walltime>~w</walltime>~n',[WT]) | |
| 436 | ; true), % ignore if not available | |
| 437 | format(Stream,' </rule>~n',[]), | |
| 438 | fail. | |
| 439 | gen_xml_rule_result(_Stream,_,_,_). | |
| 440 | %%%%%%%%% END XML REPORT %%%%%%%%%% | |
| 441 | %%%%%%%%% END REPORT %%%%%%%%%%%%%% | |
| 442 | ||
| 443 | %%%%%%%%% BEGIN DEPENDENCY GRAPH %%%%%%%%% | |
| 444 | % TODO: tooltip with counterexample? | |
| 445 | :- use_module(probsrc(state_space),[current_expression/2]). | |
| 446 | :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3,use_new_dot_attr_pred/7]). | |
| 447 | generate_dependency_graph(File) :- | |
| 448 | (animation_minor_mode(rules_dsl) -> true | |
| 449 | ; b_get_main_filename(BFile), | |
| 450 | add_error(rule_validation,'Cannot create rule dependency graph, is not a rules machine (.rmch): ',BFile), | |
| 451 | fail), | |
| 452 | current_state_id(CurID), | |
| 453 | get_variables_for_export(CurID,VarState), | |
| 454 | gen_dot_graph(File, | |
| 455 | use_new_dot_attr_pred(rule_validation:rule_graph_node_predicate(VarState)), | |
| 456 | use_new_dot_attr_pred(rule_validation:rule_graph_trans_predicate(VarState))). | |
| 457 | ||
| 458 | :- public rule_graph_node_predicate/4. | |
| 459 | rule_graph_node_predicate(State,OpName,none,[style/'filled',label/OpName,tooltip/OpName|Attr]) :- | |
| 460 | dependencies(OpName,_), % all relevant operations | |
| 461 | get_node_attributes(State,OpName,Attr). | |
| 462 | ||
| 463 | get_node_attributes(State,OpName,[shape/RShape,fillcolor/StatusColor,tooltip/Tooltip]) :- | |
| 464 | get_simple_rule_status(State,OpName,Status), !, | |
| 465 | get_preference(rule_graph_shape,RShape), | |
| 466 | (Status = 'FAIL' -> get_preference(failed_rule_colour,StatusColor) ; | |
| 467 | Status = 'SUCCESS' -> get_preference(successful_rule_colour,StatusColor) ; | |
| 468 | Status = 'DISABLED' -> get_preference(disabled_rule_colour,StatusColor) ; | |
| 469 | get_preference(not_checked_rule_colour,StatusColor)), % NOT_CHECKED, TODO: maybe UNCHECKED | |
| 470 | ajoin(['Rule: ',OpName,', Status: ',Status],Tooltip). | |
| 471 | get_node_attributes(State,OpName,[shape/CompShape,fillcolor/StatusColor,tooltip/Tooltip]) :- | |
| 472 | get_simple_computation_status(State,OpName,Status), !, | |
| 473 | get_preference(computation_graph_shape,CompShape), | |
| 474 | (Status = 'EXECUTED' -> get_preference(executed_computation_colour,StatusColor) ; | |
| 475 | Status = 'COMPUTATION_DISABLED' -> get_preference(disabled_computation_colour,StatusColor) ; | |
| 476 | get_preference(not_executed_computation_colour,StatusColor)), % NOT_EXECUTED | |
| 477 | ajoin(['Computation: ',OpName,', Status: ',Status],Tooltip). | |
| 478 | ||
| 479 | :- public rule_graph_trans_predicate/4. | |
| 480 | rule_graph_trans_predicate(State,NodeID,SuccID,[label/''|Attr]) :- | |
| 481 | dependencies(NodeID,Deps), | |
| 482 | member(SuccID,Deps), | |
| 483 | get_trans_attributes(State,SuccID,Attr). | |
| 484 | ||
| 485 | get_trans_attributes(State,DepName,[color/StatusColor,tooltip/Tooltip]) :- | |
| 486 | get_simple_rule_status(State,DepName,Status), !, | |
| 487 | ((Status = 'FAIL' ; Status = 'DISABLED') | |
| 488 | -> get_preference(failed_dependency_colour,StatusColor), TTStatus = ' is not available.' ; | |
| 489 | Status = 'SUCCESS' -> get_preference(succeeded_dependency_colour,StatusColor), TTStatus = ' is available.' ; | |
| 490 | get_preference(normal_dependency_colour,StatusColor), TTStatus = ' is available.'), % NOT_CHECKED | |
| 491 | ajoin(['Required rule ',DepName,' with status ',Status,TTStatus],Tooltip). | |
| 492 | get_trans_attributes(State,DepName,[color/StatusColor,tooltip/Tooltip]) :- | |
| 493 | get_simple_computation_status(State,DepName,Status), !, | |
| 494 | (Status = 'COMPUTATION_DISABLED' -> get_preference(failed_dependency_colour,StatusColor), TTStatus = ' is not available.' ; | |
| 495 | get_preference(normal_dependency_colour,StatusColor), TTStatus = ' is available.'), | |
| 496 | ajoin(['Required computation ',DepName,' with status ',Status,TTStatus],Tooltip). | |
| 497 | %%%%%%%%% END DEPENDENCY GRAPH %%%%%%%%% |