| 1 | % (c) 2009-2025 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 | :- module(predicate_evaluator,[tcltk_analyse_goal/1, tcltk_analyse_goal/2, | |
| 6 | tcltk_analyse_invariant/2, | |
| 7 | tcltk_analyse_assertions/2, tcltk_analyse_assertions/3, | |
| 8 | tcltk_analyse_properties/2, check_summary_all_true/1, | |
| 9 | tcltk_analyse_deadlock/2, | |
| 10 | %get_analyse_error_span_linecol/4, | |
| 11 | ||
| 12 | % a way to customize what is done with false/unknown conjuncts | |
| 13 | reset_conjunct_error_hook/0, register_conjunct_error_hook/1, | |
| 14 | register_conjunct_register_error_span/0 % conjuncts which are not true are registered as error spans | |
| 15 | ]). | |
| 16 | ||
| 17 | % a simple textual analysis of the conjuncts of a predicate | |
| 18 | ||
| 19 | :- meta_predicate register_conjunct_error_hook(5). | |
| 20 | :- meta_predicate analyse_quick_time_out(0). | |
| 21 | :- meta_predicate call_residue_check(0). | |
| 22 | :- meta_predicate time_out_and_catch_errors(0,*,*). | |
| 23 | ||
| 24 | :- use_module(tools). | |
| 25 | ||
| 26 | :- use_module(module_information,[module_info/2]). | |
| 27 | :- module_info(group,misc). | |
| 28 | :- module_info(description,'Various tools to analyse conjunctions of predicates textually (along with statistics).'). | |
| 29 | ||
| 30 | :- use_module(bmachine). | |
| 31 | :- use_module(error_manager). | |
| 32 | :- use_module(translate). | |
| 33 | :- use_module(debug). | |
| 34 | :- use_module(preferences,[get_computed_preference/2,get_preference/2,get_time_out_preference_with_factor/2]). | |
| 35 | :- use_module(state_space,[current_state_corresponds_to_setup_constants_b_machine/0, | |
| 36 | current_state_corresponds_to_fully_setup_b_machine/0]). | |
| 37 | ||
| 38 | ||
| 39 | ||
| 40 | current_b_state_with_all_constants_valued :- | |
| 41 | (current_state_corresponds_to_setup_constants_b_machine -> true | |
| 42 | ; \+ b_machine_has_constants). % also allow analysis if we have no constants (but possibly properties) | |
| 43 | ||
| 44 | :- use_module(xtl_interface,[xtl_invariant_violated/1, xtl_goal_found/1]). | |
| 45 | :- use_module(state_space,[current_expression/2]). | |
| 46 | :- use_module(specfile,[xtl_mode/0]). | |
| 47 | tcltk_analyse_goal(List) :- tcltk_analyse_goal(List,_). | |
| 48 | tcltk_analyse_goal(list(List),Summary) :- | |
| 49 | current_b_state_with_all_constants_valued, | |
| 50 | b_get_machine_goal(Goal),!, | |
| 51 | b_analyse_boolean_expression(Goal,'GOAL',false,List,Summary). | |
| 52 | tcltk_analyse_goal(list(List),Summary) :- | |
| 53 | xtl_mode,!, List = [Res], Summary = [total/1, false/Nr], | |
| 54 | current_expression(_ID,State), | |
| 55 | (xtl_goal_found(State) -> Nr=0, Res = 'XTL GOAL found (goal property holds)' | |
| 56 | ; Nr=1, Res = 'goal property does not hold'). | |
| 57 | tcltk_analyse_goal(list(['Cannot evaluate GOAL yet.\nSetup constants first.\n\n'|List]),Summary) :- | |
| 58 | b_get_machine_goal(Goal),!, | |
| 59 | get_conjuncts(Goal,List,undefined), unknown_summary(1,Summary). | |
| 60 | tcltk_analyse_goal(list(['Cannot find GOAL DEFINITION (must be a predicate).\n']),Summary) :- | |
| 61 | unknown_summary(1,Summary). | |
| 62 | ||
| 63 | tcltk_analyse_invariant(list(List),Summary) :- | |
| 64 | current_state_corresponds_to_fully_setup_b_machine,!, | |
| 65 | b_get_invariant_from_machine(Invariant), | |
| 66 | get_preference(partition_predicates,Partition), | |
| 67 | b_analyse_boolean_expression(Invariant,'INVARIANT',Partition,List,Summary). | |
| 68 | tcltk_analyse_invariant(list(List),Summary) :- | |
| 69 | xtl_mode,!, List = [Res], Summary = [total/1,false/Nr], | |
| 70 | current_expression(_ID,State), | |
| 71 | (xtl_invariant_violated(State) -> Nr=1, Res = 'XTL Invariant Violated (unsafe property holds)' | |
| 72 | ; Nr=0, Res = 'OK (unsafe cannot be derived)'). | |
| 73 | tcltk_analyse_invariant(list(['Cannot evaluate invariant yet.\nInitialise machine first.\n\n'|List]),Summary) :- | |
| 74 | b_get_invariant_from_machine(Invariant), | |
| 75 | get_conjuncts(Invariant,List,undefined), | |
| 76 | length(List,TL), unknown_summary(TL,Summary). | |
| 77 | ||
| 78 | :- use_module(specfile,[animation_mode/1, csp_with_bz_mode/0]). | |
| 79 | tcltk_analyse_assertions(List,Summary) :- tcltk_analyse_assertions(all,List,Summary). | |
| 80 | tcltk_analyse_assertions(_ALL,list(['CSP Assertions'|CA]),TSummary) :- | |
| 81 | (animation_mode(cspm) ; csp_with_bz_mode),!, | |
| 82 | statistics(walltime,[CurTime,_]), /* get current time in ms */ | |
| 83 | tcltk_interface:tcltk_check_csp_assertions(CA,Summary), | |
| 84 | statistics(walltime,[CurTime2,_]), /* get current time in ms */ | |
| 85 | Delta is CurTime2-CurTime, | |
| 86 | TSummary = [runtime/Delta|Summary], | |
| 87 | format('% CSP Assertion Checks Completed: ~w~n',[CA]). | |
| 88 | tcltk_analyse_assertions(all,list(['This Machine has no ASSERTIONS.']),Summ) :- | |
| 89 | b_get_dynamic_assertions_from_machine([]),b_get_static_assertions_from_machine([]),!,empty_summary(Summ). | |
| 90 | tcltk_analyse_assertions(main,list(['The Main Machine has no ASSERTIONS.']),Summ) :- | |
| 91 | b_main_machine_has_no_assertions, | |
| 92 | !,empty_summary(Summ). | |
| 93 | tcltk_analyse_assertions(ALL,list(List),Summary) :- | |
| 94 | current_state_corresponds_to_fully_setup_b_machine,!, | |
| 95 | %conjunct_predicates(Ass,BExpr) | |
| 96 | ? | b_get_assertions(ALL,static,SAss), |
| 97 | println_silent('Checking Static Assertions'), | |
| 98 | % translate:nested_print_bexpr(SAss), | |
| 99 | b_analyse_boolean_expression(SAss,'ASSERTIONS (static)',false,SList,SSummary), | |
| 100 | b_get_assertions(ALL,dynamic,DAss), | |
| 101 | println_silent('Checking Dynamic Assertions'), | |
| 102 | b_analyse_boolean_expression(DAss,'ASSERTIONS (dynamic)',false,DList,DSummary), | |
| 103 | combine_summary(SSummary,DSummary,Summary), | |
| 104 | ? | combine_static_dynamic_result(SList,DList,List). |
| 105 | tcltk_analyse_assertions(ALL,list(ListRes),Summary) :- | |
| 106 | current_b_state_with_all_constants_valued, | |
| 107 | b_get_assertions(ALL,static,Ass),Ass\=[],!, | |
| 108 | b_analyse_boolean_expression(Ass,'ASSERTIONS',false,SList,SSummary), | |
| 109 | b_get_assertions(ALL,dynamic,DynAss), | |
| 110 | (DynAss=[] -> ListRes = List, Summary = SSummary | |
| 111 | ; ListRes = ['Only evaluating STATIC ASSERTIONS.\nInitialise machine to evaluate other ASSERTIONS.\n\n'|List], | |
| 112 | (length(DynAss,Len) -> true ; Len=1), | |
| 113 | unknown_summary(Len,US),combine_summary(US,SSummary,Summary) | |
| 114 | ), | |
| 115 | get_assertions_as_undefined(ALL,dynamic,DList), | |
| 116 | combine_static_dynamic_result(SList,DList,List). | |
| 117 | tcltk_analyse_assertions(ALL,list(['Cannot evaluate assertions yet.\nInitialise machine first.\n\n'|List]),Summary) :- | |
| 118 | print('*** Cannot evaluate ASSERTIONS\nSPECIFICATION not initialised.'),nl, | |
| 119 | get_assertions_as_undefined(ALL,static,SList), | |
| 120 | get_assertions_as_undefined(ALL,dynamic,DList), | |
| 121 | length(SList,SL), length(DList,DL), TL is SL+DL, unknown_summary(TL,Summary), | |
| 122 | combine_static_dynamic_result(SList,DList,List). | |
| 123 | ||
| 124 | :- use_module(library(lists),[maplist/3]). | |
| 125 | get_assertions_as_undefined(ALL,SD,List) :- | |
| 126 | b_get_assertions(ALL,SD,Ass), | |
| 127 | flatten_conjunction(Ass,FAss,[]), | |
| 128 | maplist(get_as_undefined,FAss,List). | |
| 129 | % (Ass=[] -> List=[] ; conjunct_predicates(Ass,BExpr),get_conjuncts(BExpr,List,undefined)). | |
| 130 | ||
| 131 | get_as_undefined(Conjunct,Translation) :- translate_conj_status(Conjunct,undefined,false,Translation). | |
| 132 | ||
| 133 | combine_static_dynamic_result([],L,L). | |
| 134 | combine_static_dynamic_result(L,[],L). | |
| 135 | combine_static_dynamic_result(S,D,List) :- | |
| 136 | List = ['STATIC ASSERTIONS:\n'|List0], | |
| 137 | append(S,['DYNAMIC ASSERTIONS:\n'|D],List0). | |
| 138 | ||
| 139 | unknown_summary(Nr,[total/Nr,unknown/Nr,unknown_after_expansion/Nr]). | |
| 140 | combine_summary([],S,S). | |
| 141 | combine_summary([K/V|T],S,R) :- update(S,K,V,S2), combine_summary(T,S2,R). | |
| 142 | update([],K,V,[K/V]). | |
| 143 | update([K1/V1|T],K1,V2,[K1/NV|T]) :- !,NV is V1+V2. | |
| 144 | update([K1/V1|T],K,V,[K1/V1|NT]) :- update(T,K,V,NT). | |
| 145 | ||
| 146 | :- use_module(b_state_model_check,[get_unsorted_all_guards_false_pred/1]). | |
| 147 | tcltk_analyse_deadlock(list(List),Summary) :- current_state_corresponds_to_fully_setup_b_machine,!, | |
| 148 | get_unsorted_all_guards_false_pred(BExpr), | |
| 149 | b_analyse_boolean_expression(BExpr,'DEADLOCK (guard disjunction)',false,List,Summary). | |
| 150 | tcltk_analyse_deadlock(list(['Cannot evaluate deadlock yet.\nInitialise machine first.\n\n'|List]),[]) :- | |
| 151 | get_unsorted_all_guards_false_pred(BExpr), | |
| 152 | get_conjuncts(BExpr,List,undefined). | |
| 153 | ||
| 154 | tcltk_analyse_properties(list([Res]),[]) :- | |
| 155 | b_get_properties_from_machine(b(truth,_,_)),!, | |
| 156 | (b_machine_has_constants | |
| 157 | -> Res = 'This Machine has only typing information in the PROPERTIES.' | |
| 158 | ; Res = 'This Machine has no PROPERTIES clause.' | |
| 159 | ). | |
| 160 | tcltk_analyse_properties(list(List),Summary) :- | |
| 161 | current_b_state_with_all_constants_valued, | |
| 162 | !, | |
| 163 | b_get_properties_from_machine(Prop), | |
| 164 | get_preference(partition_predicates,Partition), | |
| 165 | b_analyse_boolean_expression(Prop,'PROPERTIES',Partition,List,Summary). | |
| 166 | tcltk_analyse_properties(list(['Cannot evaluate properties yet.\nSet up constants first.\n\n'|List]),Summary) :- | |
| 167 | b_get_properties_from_machine(Prop), | |
| 168 | (get_preference(partition_predicates,false) | |
| 169 | -> get_conjuncts(Prop,List,undefined), length(List,NrConjuncts) | |
| 170 | ; bsyntaxtree:predicate_components(Prop,Components), | |
| 171 | findall(CList, | |
| 172 | (member(component(CP,_CompVars),Components), | |
| 173 | get_conjuncts(CP,CList,undefined)), CCList), | |
| 174 | flatten_comp(CCList,List,NrConjuncts) | |
| 175 | ), | |
| 176 | unknown_summary(NrConjuncts,Summary). | |
| 177 | ||
| 178 | flatten_comp([],[],0). | |
| 179 | flatten_comp([H|T],['COMPONENT:\n'|Res],NrConjuncts) :- | |
| 180 | flatten_comp(T,TR,TNr), | |
| 181 | length(H,LH), NrConjuncts is LH+TNr, | |
| 182 | append(H,TR,Res). | |
| 183 | ||
| 184 | ||
| 185 | %:- dynamic conj_nr/1. | |
| 186 | %conj_nr(1). | |
| 187 | %get_and_inc_conj_nr(X) :- retract(conj_nr(X)), X1 is X+1, assertz(conj_nr(X1)). | |
| 188 | %reset_conj_nr :- retractall(conj_nr(_)), assertz(conj_nr(1)). | |
| 189 | ||
| 190 | ||
| 191 | % check if a summary report is all true | |
| 192 | check_summary_all_true(L) :- | |
| 193 | member(total_after_expansion/Nr,L), member(true_after_expansion/Nr,L), | |
| 194 | member(false/0,L), member(unknown/0,L), member(timeout/0,L). | |
| 195 | ||
| 196 | empty_summary([total/0, total_after_expansion/0, | |
| 197 | true/0, true_after_expansion/0, false/0, false_after_expansion/0, | |
| 198 | unknown/0, unknown_after_expansion/0, timeout/0, runtime/0, enum_warning/0]). | |
| 199 | :- use_module(specfile, [current_b_expression/1]). | |
| 200 | :- use_module(state_space, [current_state_id/1]). | |
| 201 | get_current_b_expression(S) :- | |
| 202 | (current_b_expression(S) -> true | |
| 203 | ; current_state_id(root), \+ b_machine_has_constants -> S = [] | |
| 204 | ; add_internal_error('Could not get B state for analysis',get_current_b_expression(S)),S=[] | |
| 205 | ). | |
| 206 | b_analyse_boolean_expression(VAR,Kind,P,L,S) :- var(VAR),!, | |
| 207 | add_internal_error('Illegal call: ',b_analyse_boolean_expression(VAR,Kind,P,L,S)), | |
| 208 | S=[unknown/1]. | |
| 209 | b_analyse_boolean_expression(BExpr,Kind,Partition,List, | |
| 210 | [total/NrTotal, total_after_expansion/NrTotalExpanded, | |
| 211 | true/NrTrue, true_after_expansion/NrTrueExpanded, | |
| 212 | false/NrFalse, false_after_expansion/NrFalseExpanded, | |
| 213 | unknown/NrUnknown, unknown_after_expansion/NrUnknownExpanded, | |
| 214 | timeout/NrTimeout, runtime/TotalTime, enum_warning/NrEnumWarning]) :- | |
| 215 | get_current_b_expression(RealCurState), | |
| 216 | %reset_conj_nr, | |
| 217 | statistics(walltime,[CurTime,_]), /* get current time in ms */ | |
| 218 | b_analyze_all_sub_conjuncts(Kind,Partition,BExpr, RealCurState, CList), | |
| 219 | statistics(walltime,[CurTime2,_]), /* get current time in ms */ | |
| 220 | formatsilent('~N=======~NSUMMARY (~w)~N=======~N',[Kind]), | |
| 221 | new_counter(Counter0), | |
| 222 | l_translate_conjunct_analysis_result(CList,List,none/true,'$_no_model'(none),Counter0,ResCounter), | |
| 223 | %print_counter(ResCounter), | |
| 224 | get_counter(total,ResCounter,NrTotal), get_counter(total_after_expansion,ResCounter,NrTotalExpanded), | |
| 225 | get_counter(true,ResCounter,NrTrue), get_counter(true_after_expansion,ResCounter,NrTrueExpanded), | |
| 226 | get_counter(false,ResCounter,NrFalse), get_counter(false_after_expansion,ResCounter,NrFalseExpanded), | |
| 227 | get_counter(unknown,ResCounter,NrUnknown), get_counter(unknown_after_expansion,ResCounter,NrUnknownExpanded), | |
| 228 | get_counter(timeout,ResCounter,NrTimeout), get_counter(enum_warning,ResCounter,NrEnumWarning), | |
| 229 | (silent_mode(on),NrFalse==0,NrUnknown==0 -> true | |
| 230 | ; NrTotal=NrTotalExpanded | |
| 231 | -> format('~p predicates: ~p TRUE, ~p FALSE, ~p UNKNOWN (~p timeouts)~N',[NrTotal,NrTrue,NrFalse,NrUnknown,NrTimeout]) | |
| 232 | ; format('~p predicates (~p after expansion): ~p TRUE (~p after expansion), ~p FALSE (~p after expansion), ~p UNKNOWN (~p after expansion) (~p timeouts)~N',[NrTotal,NrTotalExpanded,NrTrue,NrTrueExpanded,NrFalse,NrFalseExpanded,NrUnknown,NrUnknownExpanded,NrTimeout])), | |
| 233 | TotalTime is CurTime2-CurTime, | |
| 234 | formatsilent('~w ms to analyse ~w~n',[TotalTime,Kind]). | |
| 235 | ||
| 236 | :- use_module(bsyntaxtree). | |
| 237 | ||
| 238 | b_analyze_all_sub_conjuncts(Kind,true,BExpr, RealCurState, CList) :- !, | |
| 239 | bsyntaxtree:predicate_components(BExpr,Components), % Note: does not support list of conjunctions (as generated by b_get_assertions_from_machine) | |
| 240 | findall(comp_res(CCList,CompVars), | |
| 241 | (member(component(CompBExpr,CompVars),Components), | |
| 242 | analyze_all_conjuncts2(Kind,CompBExpr, RealCurState, CCList)),CompRes), | |
| 243 | flatten_comp_res(CompRes,CList). | |
| 244 | b_analyze_all_sub_conjuncts(Kind,_Partition,BExpr, RealCurState, CList) :- | |
| 245 | analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList). | |
| 246 | ||
| 247 | flatten_comp_res([],[]). | |
| 248 | flatten_comp_res([comp_res(CCList,Vars)|T],Res) :- | |
| 249 | flatten_comp_res(T,FT), | |
| 250 | append([vars(Vars)|CCList],FT,Res). | |
| 251 | ||
| 252 | analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList) :- | |
| 253 | findall(conj(Nr,Conjunct,Status,EnumWarning,IsExpanded), | |
| 254 | (%get_and_inc_conj_nr(Nr), print(analysing_conjunct(Nr)),nl, | |
| 255 | b_analyse_conjunction(Kind,BExpr,[],RealCurState,Nr,Conjunct,Status,EnumWarning,IsExpanded) | |
| 256 | ), | |
| 257 | CList). | |
| 258 | ||
| 259 | %:- use_module(library(codesio)). | |
| 260 | :- use_module(tools_meta,[translate_term_into_atom/2]). | |
| 261 | l_translate_conjunct_analysis_result([],[],CurConjNr/CurStatus,_LastModel,Acc,ResAcc) :- | |
| 262 | flush_cur_status(CurConjNr,CurStatus,Acc,ResAcc). | |
| 263 | l_translate_conjunct_analysis_result([vars(Vars)|T],Res,CurConjNr/CurStatus,_LastModel,Acc,CRes) :- | |
| 264 | flush_cur_status(CurConjNr,CurStatus,Acc,Acc1), | |
| 265 | (Vars=[] -> Res = ['** ISOLATED CONJUNCT **\n'|TT] | |
| 266 | ; Res = [CS,CV,' **\n'|TT], CS = '** CONJUNCTS OVER IDENTIFIERS:'), | |
| 267 | translate_term_into_atom(Vars,CV), | |
| 268 | l_translate_conjunct_analysis_result(T,TT,none/true,'$_no_model'(none),Acc1,CRes). | |
| 269 | l_translate_conjunct_analysis_result([conj(NextNr,Conjunct,Status,EnumWarning,IsExpanded)|T],TranslationResult,CurConjNr/CurStatus,LastModel,Acc,CRes) :- | |
| 270 | translate_conjunct(Conjunct,Status,EnumWarning,CS), | |
| 271 | inc_counter(total_after_expansion,Acc,AA), | |
| 272 | (EnumWarning==true -> inc_counter(enum_warning,AA,A1) ; AA=A1), | |
| 273 | ( Status = 'TRUE' -> inc_counter(true_after_expansion,A1,NewAcc) | |
| 274 | ; Status = timeout_true -> inc_counter(true_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) | |
| 275 | ; Status = false -> inc_counter(false_after_expansion,A1,NewAcc) | |
| 276 | ; Status = timeout_false -> inc_counter(false_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) | |
| 277 | ; Status = both_true_false -> inc_counter(unknown_after_expansion,A1,NewAcc) | |
| 278 | ; Status = wd_error_true -> inc_counter(unknown_after_expansion,A1,NewAcc) | |
| 279 | ; Status = wd_error_false -> inc_counter(unknown_after_expansion,A1,NewAcc) | |
| 280 | ; inc_counter(unknown_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) | |
| 281 | ), | |
| 282 | (call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS) -> true | |
| 283 | ; add_internal_error('Conjunct error hook failed: ', | |
| 284 | call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS))), | |
| 285 | (CurConjNr==NextNr | |
| 286 | -> combine_status(CurStatus,Status,NewStatus), NewAcc=NewAcc2 % still the same conjunct; combine status | |
| 287 | ; flush_cur_status(CurConjNr,CurStatus,NewAcc,NewAcc2), | |
| 288 | convert_status(Status,NewStatus)), | |
| 289 | ((get_rodin_model_name(Conjunct,NewModel), NewModel \= LastModel) | |
| 290 | -> TranslationResult = [' * MODEL: ',NewModel,'\n',CS|TT] % show from which model the conjuncts come from | |
| 291 | ; NewModel = LastModel, TranslationResult = [CS|TT]), | |
| 292 | l_translate_conjunct_analysis_result(T,TT,NextNr/NewStatus,NewModel,NewAcc2,CRes). | |
| 293 | ||
| 294 | flush_cur_status(CurConjNr,CurStatus,Acc,NewAcc2) :- | |
| 295 | (CurConjNr==none -> Acc=NewAcc2 | |
| 296 | ; inc_counter(total,Acc,NewAcc1), | |
| 297 | (CurStatus = true -> inc_counter(true,NewAcc1,NewAcc2) | |
| 298 | ; CurStatus = false -> inc_counter(false,NewAcc1,NewAcc2) | |
| 299 | ; inc_counter(unknown,NewAcc1,NewAcc2)) ). | |
| 300 | ||
| 301 | combine_status(true,X,R) :- convert_status(X,R). | |
| 302 | combine_status(false,_,false). | |
| 303 | combine_status(unknown,false,R) :- !,R=false. | |
| 304 | combine_status(unknown,_,unknown). | |
| 305 | ||
| 306 | convert_status('TRUE',true) :- !. | |
| 307 | convert_status(timeout_true,true) :- !. | |
| 308 | convert_status(false,false) :- !. | |
| 309 | convert_status(timeout_false,false) :- !. | |
| 310 | convert_status(_,unknown). | |
| 311 | ||
| 312 | :- dynamic conjunct_error_hook_pred/1. | |
| 313 | conjunct_error_hook_pred(default_hook). | |
| 314 | call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, TranslatedConjunct) :- | |
| 315 | convert_status(Status,ConvStatus), | |
| 316 | conjunct_error_hook_pred(Pred), | |
| 317 | call(Pred,Conjunct,ConvStatus,EnumWarning,IsExpanded, TranslatedConjunct). | |
| 318 | :- public default_hook/5. | |
| 319 | default_hook(_,_Status,_,_, _CS). | |
| 320 | %((Status='TRUE' ; Status = timeout_true) -> print(CS),nl ; true). | |
| 321 | ||
| 322 | :- use_module(error_manager,[register_error_span/2]). | |
| 323 | register_span_hook(Conjunct,ConvStatus,_EnumWarning,_IsExpanded, _TranslatedConjunct) :- | |
| 324 | %print(status(ConvStatus)),nl, | |
| 325 | (ConvStatus=true -> true ; register_error_span(predicate_evaluator,Conjunct)). % store positions for Tcl/Tk | |
| 326 | ||
| 327 | reset_conjunct_error_hook :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(default_hook)). | |
| 328 | ||
| 329 | register_conjunct_error_hook(Pred) :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(Pred)). | |
| 330 | ||
| 331 | register_conjunct_register_error_span :- register_conjunct_error_hook(register_span_hook). | |
| 332 | ||
| 333 | ||
| 334 | % some utilities to count occurences of certain things: | |
| 335 | :- use_module(library(assoc)). | |
| 336 | new_counter(C) :- empty_assoc(C). | |
| 337 | %reset_counter(Key,C,NC) :- put_assoc(Key,C,0,NC). | |
| 338 | inc_counter(Key,C,NC) :- (get_assoc(Key,C,Val) -> NewVal is Val+1 ; NewVal =1), | |
| 339 | put_assoc(Key,C,NewVal,NC). | |
| 340 | %cond_inc_counter(true,Key,C,NC) :- !, inc_counter(Key,C,NC). | |
| 341 | %cond_inc_counter(_,_,C,C). | |
| 342 | get_counter(Key,C,Val) :- (get_assoc(Key,C,Val) -> true ; Val =0). | |
| 343 | %print_counter(C) :- portray_assoc(C),nl. | |
| 344 | %get_counter_list(C,L) :- assoc_to_list(C,L). | |
| 345 | ||
| 346 | :- use_module(b_interpreter). | |
| 347 | :- use_module(bsyntaxtree,[is_a_conjunct/3]). | |
| 348 | ||
| 349 | % conjunct_ | |
| 350 | %b_analyse_conjunction(C, LocalState,State,Conjunct,Status,EnumWarning) :- tools_printing:print_term_summary(C),nl,fail. | |
| 351 | ||
| 352 | :- use_module(library(lists),[nth1/3]). | |
| 353 | b_analyse_conjunction(Kind,Conj, LocalState,State,Nr,EvConjunct,Status,EnumWarning,IsExpanded) :- | |
| 354 | flatten_conjunction(Conj,ConjList,[]), | |
| 355 | ? | nth1(Nr, ConjList, Conjunct), |
| 356 | ? | b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded). |
| 357 | ||
| 358 | flatten_conjunction([]) --> !, []. | |
| 359 | flatten_conjunction([H|T]) --> !, flatten_conjunction(H),flatten_conjunction(T). | |
| 360 | flatten_conjunction(C) --> {is_a_conjunct(C,LHS,RHS)}, | |
| 361 | {\+ do_not_decompose(C)}, % otherwise the user wants to group it | |
| 362 | !, | |
| 363 | flatten_conjunction(LHS), flatten_conjunction(RHS). | |
| 364 | flatten_conjunction(C) --> [C]. | |
| 365 | ||
| 366 | % maybe provide option to always decompose for precision/performance/forall expansion | |
| 367 | do_not_decompose(C) :- bsyntaxtree:get_texpr_labels(C,_),!. % otherwise the user wants to group it | |
| 368 | do_not_decompose(C) :- get_texpr_info(C,Infos), | |
| 369 | member(generated_conjunct,Infos). % the conjunct has been generated, e.g., by b_ast_cleanup | |
| 370 | ||
| 371 | :- use_module(tools_meta,[safe_time_out/3]). | |
| 372 | analyse_quick_time_out(Call) :- | |
| 373 | get_time_out_preference_with_factor(0.05,DTimeOut), | |
| 374 | (DTimeOut > 400 -> TO = 400 ; TO = DTimeOut), | |
| 375 | on_enumeration_warning( | |
| 376 | safe_time_out(Call,TO,Res), | |
| 377 | fail), % in case of enumeration warnings: we could not compute all elements of domain | |
| 378 | \+ is_time_out_result(Res). | |
| 379 | %analyse_time_out(Call) :- | |
| 380 | % preferences:get_computed_preference(debug_time_out,DTimeOut), | |
| 381 | % time_out_with_enum_warning_one_solution(Call,DTimeOut,Res), | |
| 382 | % \+ is_time_out_result(Res). | |
| 383 | ||
| 384 | ||
| 385 | :- use_module(b_interpreter,[b_generate_for_all_list_domain_nolwf/8]). | |
| 386 | :- use_module(kernel_waitflags,[ground_wait_flags/1,init_wait_flags/2]). | |
| 387 | ||
| 388 | b_analyse_conjunction_nr(Kind,Nr,b(forall(Parameters,LHS,RHS),pred,Info),LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :- | |
| 389 | IsExpanded=true, | |
| 390 | get_preference(expand_forall_upto,MaxLenForEpxansion), | |
| 391 | MaxLenForEpxansion>0, | |
| 392 | % print(generating_for_all_domain(Parameters)),nl, | |
| 393 | analyse_quick_time_out(( | |
| 394 | kernel_waitflags:init_wait_flags_with_call_stack(WF,[prob_command_context(analyse_quick_time_out,Info)]), | |
| 395 | b_interpreter:b_generate_for_all_list_domain_nolwf(Parameters,LHS,RHS,LocalState,State,AllSols,NewRHS,WF), | |
| 396 | kernel_waitflags:ground_wait_flags(WF))), | |
| 397 | length(AllSols,Len), Len>0, Len=<MaxLenForEpxansion,!, | |
| 398 | (silent_mode(on) -> true ; print('FORALL domain computed: '), translate:print_bexpr(LHS),nl), | |
| 399 | ? | member(ParResult,AllSols), |
| 400 | set_up_equality(Parameters,ParResult,EqList), | |
| 401 | conjunct_predicates(EqList,EqPred), | |
| 402 | EvConjunct = b(forall(Parameters,EqPred,RHS),pred,Info), | |
| 403 | (debug_mode(on) -> print('Testing: '), print_bexpr(EvConjunct),nl ; true), | |
| 404 | set_up_typed_localstate(Parameters,ParResult,_,LocalState,NewLocalState,positive), | |
| 405 | b_analyse_individual_conjunct(Kind,Nr,NewRHS,NewLocalState,State,_,Status,EnumWarning). | |
| 406 | b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :- | |
| 407 | %debug:debug_println(9,analysing_conjunct_in_component(Nr)), | |
| 408 | IsExpanded=false, | |
| 409 | b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning). | |
| 410 | ||
| 411 | set_up_equality([],[],[]). | |
| 412 | set_up_equality([Identifier|IR],[Val|VR],[b(equal(Identifier,b(value(Val),IDType,[])),pred,[])|TE]) :- | |
| 413 | get_texpr_type(Identifier,IDType), | |
| 414 | set_up_equality(IR,VR,TE). | |
| 415 | ||
| 416 | ||
| 417 | ||
| 418 | :- use_module(tools_printing,[print_goal/1]). | |
| 419 | :- use_module(tools_meta,[safe_time_out/3,call_residue/2]). | |
| 420 | ||
| 421 | call_residue_check(Call) :- | |
| 422 | ? | call_residue(Call,Residue), |
| 423 | (Residue = [] -> true | |
| 424 | ; add_internal_error('Call had residue: ',residue(Residue)/call(Call)), | |
| 425 | print_goal(Residue),nl | |
| 426 | ). | |
| 427 | ||
| 428 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). | |
| 429 | % very similar to time_out_with_enum_warning, adds catch_clpfd_overflow_call1 | |
| 430 | time_out_and_catch_errors(Call,TimeOut,Result) :- | |
| 431 | ? | catch( |
| 432 | safe_time_out(catch_clpfd_overflow_call1(call_residue_check(Call)),TimeOut,Result), | |
| 433 | enumeration_warning(_,_,_,_,_), | |
| 434 | (print('Treating enumeration warning as TIMEOUT !'),nl, | |
| 435 | Result=time_out)). | |
| 436 | ||
| 437 | :- use_module(tools_printing,[print_red/1, print_green/1]). | |
| 438 | b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,Conjunct,Status,EnumWarning) :- | |
| 439 | ||
| 440 | get_computed_preference(debug_time_out,DTimeOut), | |
| 441 | ||
| 442 | (silent_mode(on) -> true | |
| 443 | ; nl,print('==> '),translate:print_bexpr(Conjunct),nl), | |
| 444 | %translate:print_bexpr_with_limit(Conjunct,250),nl, | |
| 445 | statistics(walltime,[T1,_]), | |
| 446 | enter_new_error_scope(ScopeID,b_analyse_individual_conjunct), | |
| 447 | ? | (time_out_and_catch_errors(b_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr), |
| 448 | DTimeOut,TimeOutRes) -> | |
| 449 | /* PREDICATE TRUE */ | |
| 450 | statistics(walltime,[T2,_]),check_enum_warning(positive,EnumWarning), | |
| 451 | exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_true), % Warning: if strict_raise_warnings is set to true we also get the warnings as errors here !! | |
| 452 | (TimeOutRes=time_out | |
| 453 | -> print_red('TIMEOUT'),nl,Status=timeout | |
| 454 | ; ErrOcc=true -> (get_preference(strict_raise_warnings,true) -> print('POSSIBLY ') ; true), | |
| 455 | print_red('NOT-WELL-DEFINED (TRUE)'),nl, Status = wd_error_true | |
| 456 | ; print_true, | |
| 457 | enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_true), | |
| 458 | ((get_preference(double_evaluation_when_analysing,true), | |
| 459 | time_out_and_catch_errors(b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr), | |
| 460 | DTimeOut,TimeOutRes2)) | |
| 461 | -> (TimeOutRes2==time_out -> Status = timeout_true | |
| 462 | ; Status = both_true_false, | |
| 463 | add_error(predicate_evaluator,'Conjunct is both true and false: ',Conjunct,Conjunct) | |
| 464 | ) | |
| 465 | ; Status = 'TRUE' ), | |
| 466 | check_enum_warning(_,_NegEnumWarning), | |
| 467 | exit_error_scope(NegScopeID,_NegTErrorOccurred,b_analyse_double_evaluation_true) % Should we also report those errors ? + NegEnumWarning ? | |
| 468 | ) | |
| 469 | ; /* PREDICATE FALSE */ | |
| 470 | statistics(walltime,[T2,_]), check_enum_warning(negative,EnumWarning), | |
| 471 | exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_false), | |
| 472 | (ErrOcc=true | |
| 473 | -> print_red('NOT-WELL-DEFINED (FALSE)'),nl, Status = wd_error_false | |
| 474 | ; (EnumWarning=true -> print_red('UNKNOWN'),nl | |
| 475 | ; print_false), | |
| 476 | enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_false), | |
| 477 | ((get_preference(double_evaluation_when_analysing,false) ; | |
| 478 | time_out_and_catch_errors( | |
| 479 | b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr), | |
| 480 | DTimeOut,TimeOutRes2)) | |
| 481 | -> (TimeOutRes2==time_out -> Status = timeout_false ; Status = false) | |
| 482 | ; Status = unknown), | |
| 483 | exit_error_scope(NegScopeID,_NegFErrorOccurred,b_analyse_double_evaluation_false) % Should we also report those errors ? + NegEnumWarning ? | |
| 484 | ) | |
| 485 | ), | |
| 486 | statistics(walltime,[T3,_]), | |
| 487 | Time1 is T2-T1, Time2 is T3-T2, Time is T3-T1, | |
| 488 | (silent_mode(on) -> true | |
| 489 | ; format('~w (~w ms + ~w ms = ~w ms)',[Status,Time1,Time2,Time]), | |
| 490 | (Status = 'TRUE' -> true | |
| 491 | ; translate:translate_span(Conjunct,SpanS), SpanS \= '' -> print(' '),print(SpanS) | |
| 492 | ; true),nl | |
| 493 | ). | |
| 494 | ||
| 495 | print_true :- silent_mode(on),!. | |
| 496 | print_true :- print_green('TRUE'),nl. | |
| 497 | print_false :- silent_mode(on),!. | |
| 498 | print_false :- print_red('FALSE'),nl. | |
| 499 | ||
| 500 | ||
| 501 | check_enum_warning(positive,EnumWarning) :- !, | |
| 502 | (enumeration_warning_occured_in_error_scope | |
| 503 | -> print('### Enumeration warnings not critical (solution found)'),nl %, error_manager:trace_if_user_wants_it %% | |
| 504 | ; true), EnumWarning = false. | |
| 505 | check_enum_warning(_,EnumWarning) :- | |
| 506 | \+ critical_enumeration_warning_occured_in_error_scope,!, | |
| 507 | EnumWarning = false. | |
| 508 | check_enum_warning(_,EnumWarning) :- | |
| 509 | (event_occurred_in_error_scope(enumeration_warning(enumerating(_),_,_,_,_)) | |
| 510 | -> print('### Warning: infinite types were enumerated'),nl, E1=true | |
| 511 | ; true), | |
| 512 | (event_occurred_in_error_scope(enumeration_warning(checking_finite_closure,_,_,_,_)) | |
| 513 | -> print('### Warning: finiteness of comprehension sets could not be determined'),nl, E2=true | |
| 514 | ; true), | |
| 515 | (var(E1),var(E2) | |
| 516 | -> print('### Unknown enumeration warning occurred !') | |
| 517 | ; true), | |
| 518 | EnumWarning = true. | |
| 519 | ||
| 520 | translate_conjunct([],_Status,_EnumWarning,'EmptyInvariant') :- !. | |
| 521 | /* translate_conjunct(Conjunct,true,true) :- !. */ /* do not show true conjuncts */ | |
| 522 | translate_conjunct(Conjunct,Status,EnumWarning,Translation) :- | |
| 523 | translate_conj_status(Conjunct,Status,EnumWarning,Translation). | |
| 524 | ||
| 525 | ||
| 526 | get_conjuncts(BoolExpr,Conjuncts,Status) :- findall(C,get_conjunct(BoolExpr,C,Status),Conjuncts). | |
| 527 | get_conjunct(C,Conjunct,Status) :- is_a_conjunct(C,LHS,RHS),!, | |
| 528 | (get_conjuncts(LHS,Conjunct,Status) ; get_conjuncts(RHS,Conjunct,Status)). | |
| 529 | get_conjunct(Conjunct,Translation,Status) :- | |
| 530 | translate_conj_status(Conjunct,Status,false,Translation). | |
| 531 | ||
| 532 | translate_conj_status(Conjunct,Status,EnumWarning,Translation) :- | |
| 533 | translate_bexpression_with_limit(Conjunct,500,TC), | |
| 534 | (EnumWarning=true -> | |
| 535 | ajoin([TC,'\n == ',Status,' (#### infinite set expanded ####)\n\n'],Translation) | |
| 536 | ; ajoin([TC,'\n == ',Status,'\n\n'],Translation)). | |
| 537 |