| 1 | % (c) 2009-2019 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(enabling_analysis,[reset_enabling_analysis/0, | |
| 6 | tcltk_cbc_cfg_analysis/1, tcltk_dot_cfg_analysis/1, | |
| 7 | tcltk_cbc_enabling_analysis/1, tcltk_cbc_enabling_analysis/2, | |
| 8 | tcltk_cbc_enabling_relations_for_operation/3, | |
| 9 | tcltk_cbc_enabling_relations_after_operation/3, compute_cbc_enable_rel/4, | |
| 10 | tcltk_cbc_simultaneous_enabling_analysis/1, | |
| 11 | tcltk_cbc_dependence_analysis/1, print_enable_table/1, | |
| 12 | eop_node_predicate/6,init_or_op/1, | |
| 13 | feasible_operation/2, feasible_operation_with_timeout/3, | |
| 14 | check_if_feasible_operation/5, | |
| 15 | feasible_operation_cache/2,infeasible_operation/1, infeasible_operation_cache/1, | |
| 16 | cbc_enable_analysis/4, | |
| 17 | is_timeout_enabling_result/1, | |
| 18 | translate_enable_res/6, | |
| 19 | operation_sequence_possible/3, operation_can_be_enabled_by/3, | |
| 20 | ||
| 21 | cbc_enable_analysis_cache/4 % for prologTasks | |
| 22 | ]). | |
| 23 | ||
| 24 | :- use_module(module_information,[module_info/2]). | |
| 25 | :- module_info(group,cbc). | |
| 26 | :- module_info(description,'This module computes enabling relations for B operations.'). | |
| 27 | % -------------- | |
| 28 | ||
| 29 | :- use_module(probporsrc(static_analysis),[action_dependent_to_itself/4, get_conj_inv_predicate/3, is_timeout/1]). | |
| 30 | :- use_module(bmachine, [b_top_level_operation/1]). | |
| 31 | :- use_module(b_state_model_check, [get_negated_guard/3,get_negated_guard/4]). | |
| 32 | :- use_module(sap). | |
| 33 | :- use_module(library(ordsets)). | |
| 34 | :- use_module(library(lists)). | |
| 35 | :- use_module(error_manager). | |
| 36 | :- use_module(debug). | |
| 37 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2]). | |
| 38 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
| 39 | :- use_module(probsrc(b_read_write_info), [b_get_read_write/3,b_get_read_write_vars/5, b_get_operation_read_guard_vars/3]). | |
| 40 | ||
| 41 | % -------------------- BINARY STATIC ANALYSIS ------------------------- | |
| 42 | ||
| 43 | % certain static analyses used by CBC Test case generation | |
| 44 | ||
| 45 | % check if OpName1 can influence the truth value of the guard of OpName2 by looking at read/write info | |
| 46 | activation_dependent(OpName1,OpName2) :- | |
| 47 | b_top_level_operation(OpName1), | |
| 48 | b_get_read_write(OpName1,_,Writes1), | |
| 49 | b_top_level_operation(OpName2), | |
| 50 | b_get_operation_read_guard_vars(OpName2,true,GuardReads2), | |
| 51 | (my_ord_intersect(Writes1,GuardReads2) -> true | |
| 52 | ; %print(indep(OpName1,Writes1,OpName2,GuardReads2)),nl, | |
| 53 | fail | |
| 54 | ). | |
| 55 | ||
| 56 | % a version of ord_intersect(ion) which deals with the '$all' term | |
| 57 | my_ord_intersect('$all',_) :- !. | |
| 58 | my_ord_intersect(_,'$all') :- !. | |
| 59 | my_ord_intersect(A,B) :- ord_intersect(A,B). | |
| 60 | ||
| 61 | ||
| 62 | % return Res=impossible if from Invariant we can never execute OpName1 followed by OpName2 | |
| 63 | % is used by sap:check_operation_sequence_possible | |
| 64 | operation_sequence_possible(OpName1,OpName2,Res) :- | |
| 65 | \+ activation_dependent(OpName1,OpName2), | |
| 66 | !, | |
| 67 | Res = activation_independent. | |
| 68 | operation_sequence_possible(OpName1,OpName2,Res) :- | |
| 69 | % we assume OpName2 is feasible on its own | |
| 70 | get_negated_guard(OpName2,PosGuard2,_NegGuard2), | |
| 71 | Timeout1 = 200, | |
| 72 | % print('Guard: '),translate:print_bexpr(PosGuard2),nl, | |
| 73 | (testcase_path_timeout_catch(invariant,Timeout1,[OpName1],PosGuard2,_Csts,_Ops,_TestS,_TI,Res) | |
| 74 | -> true | |
| 75 | ; Res = impossible | |
| 76 | ). | |
| 77 | ||
| 78 | ||
| 79 | % return whether OpName1 can enable a previously disabled OpName2 | |
| 80 | operation_can_be_enabled_by(OpName1,OpName2,Res) :- | |
| 81 | b_top_level_operation(OpName1), | |
| 82 | b_get_read_write(OpName1,_Reads1,Writes1), | |
| 83 | b_top_level_operation(OpName2), | |
| 84 | formatsilent("~nCHECKING if ~w (~w) can enable ~w~n",[OpName1,Writes1,OpName2]), | |
| 85 | get_negated_guard(OpName2,PosGuard2,_NegGuard2), | |
| 86 | filter_predicate(PosGuard2,Writes1,FilteredPosGuard2), | |
| 87 | create_negation(FilteredPosGuard2,FilteredNegGuard2), | |
| 88 | TIMEOUT = 500, | |
| 89 | % print('Before: '), translate:print_bexpr(FilteredNegGuard2),nl,print('After: '), translate:print_bexpr(PosGuard2),nl, | |
| 90 | testcase_path_timeout_catch(pred(FilteredNegGuard2),TIMEOUT,[OpName1],PosGuard2,_,_,_,_,Res), | |
| 91 | println_silent(result(Res)). | |
| 92 | ||
| 93 | ||
| 94 | ||
| 95 | % -------------------- CFG ANALYSIS ------------------------- | |
| 96 | :-use_module(dot_graph_generator,[gen_dot_graph/6]). | |
| 97 | tcltk_dot_cfg_analysis(File) :- | |
| 98 | gen_dot_graph(File,enabling_analysis,eop_node_predicate,cfg_trans_predicate,none,none). | |
| 99 | ||
| 100 | :- use_module(tools,[ajoin/2]). | |
| 101 | :- use_module(preferences,[get_preference/2]). | |
| 102 | op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- | |
| 103 | get_preference(dot_enabling_show_readwrites,false), !, | |
| 104 | SubGraph=none, Shape=box, Style=none, | |
| 105 | b_top_level_operation(Op), NodeID = Op, NodeDesc=Op, Color=blue. | |
| 106 | op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none, | |
| 107 | Shape=record, Style=none, | |
| 108 | b_top_level_operation(Op), NodeID = Op, | |
| 109 | %NodeDesc = NodeID, | |
| 110 | b_get_read_write(Op,Reads2,Writes1), | |
| 111 | b_get_operation_read_guard_vars(Op,false,ReadsGrd), | |
| 112 | insert_commas(ReadsGrd,0,R1), insert_commas(Reads2,0,R2), insert_commas(Writes1,0,W1), | |
| 113 | append(W1,['}|'],W2), | |
| 114 | append(R1,['\\n|reads: '|R2],Reads), | |
| 115 | append(Reads,['\\n|writes: '|W2],As), | |
| 116 | ajoin(['|{',Op,'\\n|reads (guard): '|As],NodeDesc), | |
| 117 | Color=blue. | |
| 118 | ||
| 119 | insert_commas('$all',_,['ALL']). | |
| 120 | insert_commas([],_,[]). | |
| 121 | insert_commas([H],_,R) :- !, R=[H]. | |
| 122 | insert_commas([H|T],N,[H,Sep|IT]) :- | |
| 123 | (N>5 -> N1=0, Sep=',\\n' ; N1 is N+1, Sep=', '), | |
| 124 | insert_commas(T,N1,IT). | |
| 125 | ||
| 126 | :- public cfg_trans_predicate/5. | |
| 127 | cfg_trans_predicate(NodeID,Label,SuccID,Color,Style) :- | |
| 128 | cbc_quick_cfg_analysis(NodeID,SuccID,Res), | |
| 129 | translate_res(Res,NodeID,SuccID,Label,Color,Style). | |
| 130 | ||
| 131 | translate_res(cannot_enable,_,_,_,_,_) :- !, fail. | |
| 132 | translate_res(syntactic_independent,X,Y,'independent',yellow,bold) :- !,X=Y. % only show if source & dest identical | |
| 133 | translate_res(race_dependent,X,Y,'race_independent',lightgray,bold) :- !,X=Y. % only show if source & dest identical | |
| 134 | translate_res(possible,_,_,'',black,solid) :- !. | |
| 135 | translate_res(timeout_possible,_,_,'',tomato,solid) :- !. | |
| 136 | translate_res(X,_,_,X,red,dashed). | |
| 137 | ||
| 138 | % compute a Control Flow Graph very quickly | |
| 139 | % ideal when we have program counter style variables | |
| 140 | tcltk_cbc_cfg_analysis(list([list(['Origin'|SOps])|Result])) :- | |
| 141 | findall(Op, b_top_level_operation(Op), Ops), sort(Ops,SOps), | |
| 142 | findall(list([OpName1|EnableList]), | |
| 143 | (b_get_sorted_op(OpName1), | |
| 144 | findall(Possible,cbc_quick_cfg_analysis(OpName1,_OpName2,Possible),EnableList)), | |
| 145 | Result), | |
| 146 | print_enable_table([list(['Origin'|Ops])|Result]). | |
| 147 | ||
| 148 | /* TO DO: complete into a determinacy analysis ? | |
| 149 | cbc_quick_det_analysis(OpName1,OpName2,Res) :- | |
| 150 | b_top_level_operation(OpName1), % top_level | |
| 151 | ((b_get_sorted_op(OpName2), OpName2 \= OpName1, | |
| 152 | % get_negated_guard(OpName1,PosGuard1,NegGuard1), | |
| 153 | get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 154 | sap:testcase_path_timeout(pred(PosGuard2),1200,[OpName1],b(truth,pred,[]),_,_,_,_,Res)) | |
| 155 | -> format(user_output,'Operation ~w can be simultaneously enabled with ~w (~w).~n',[OpName1,OpName2,Res]) | |
| 156 | ; format(user_output,'Operation ~w cannot be simultanously enabled with another operation.~n',[OpName1]), Res=det | |
| 157 | ). | |
| 158 | */ | |
| 159 | ||
| 160 | cbc_quick_cfg_analysis(OpName1,OpName2,Res) :- | |
| 161 | OpName1='INITIALISATION', | |
| 162 | b_top_level_operation(OpName2), | |
| 163 | b_get_read_write(OpName2,Reads2,Writes2), | |
| 164 | formatsilent(user_output,"COMPUTING CFG: INITIALISATION --> ~w r:~w / w:~w~n~n", | |
| 165 | [OpName2,Reads2,Writes2]), | |
| 166 | ( testcase_path_timeout_catch(init,250,[OpName2],b(truth,pred,[]),_Constants,_Ops,_TestS,_TI,R1) | |
| 167 | -> formatsilent(user_output," ~w can be enabled by ~w (~w)!~n",[OpName2,OpName1,R1]), | |
| 168 | (is_timeout(R1) -> Res=timeout_possible; Res = possible) | |
| 169 | ; formatsilent(user_output," ~w cannot be enabled by ~w!~n",[OpName2,OpName1]), | |
| 170 | Res = cannot_enable | |
| 171 | ). | |
| 172 | cbc_quick_cfg_analysis(OpName1,OpName2,Res) :- | |
| 173 | b_top_level_operation(OpName1), % top_level | |
| 174 | b_get_read_write(OpName1,Reads1,Writes1), | |
| 175 | %get_negated_guard(OpName1,PosGuard1,NegGuard1), | |
| 176 | b_get_sorted_op(OpName2), | |
| 177 | (b_get_read_write(OpName2,Reads2,Writes2), | |
| 178 | formatsilent(user_output,"COMPUTING CFG: ~w r:~w / w:~w --> ~w r:~w / w:~w~n~n", | |
| 179 | [OpName1,Reads1,Writes1,OpName2,Reads2,Writes2]), | |
| 180 | (\+ my_ord_intersect(Writes1,Reads2) | |
| 181 | -> (my_ord_intersect(Writes1,Writes2) | |
| 182 | -> Res = race_dependent, formatsilent(user_output," ~w cannot be enabled/disabled by ~w!~n",[OpName2,OpName1]) | |
| 183 | ; Res = syntactic_independent, formatsilent(user_output," ~w cannot be enabled/disabled/modified by ~w!~n",[OpName2,OpName1]) | |
| 184 | ) | |
| 185 | ; get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 186 | garbage_collect, | |
| 187 | print('Guard: '), translate:print_bexpr(PosGuard2),nl, | |
| 188 | ((testcase_path_timeout_catch(typing(NegGuard2),60,[OpName1],PosGuard2,_,_,_,_,_R0), % quick check without invariants & properties | |
| 189 | % TO DO: project constants, variables onto the ones really needed | |
| 190 | testcase_path_timeout_catch(pred(NegGuard2),250,[OpName1],PosGuard2,_Constants,_Ops,_TestS,_TI,R1)) | |
| 191 | -> formatsilent(user_output," ~w can be enabled by ~w (~w)!~n",[OpName2,OpName1,R1]), | |
| 192 | (is_timeout(R1) -> Res=timeout_possible; Res = possible) | |
| 193 | ; formatsilent(user_output," ~w cannot be enabled by ~w!~n",[OpName2,OpName1]), | |
| 194 | Res = cannot_enable) | |
| 195 | ) | |
| 196 | ). | |
| 197 | ||
| 198 | %use_module(enabling_analysis),enabling_analysis:cbc_quick_cfg_analysis('SEQUENCER2','SEQUENCER3',Res). | |
| 199 | %use_module(sap),use_module(enabling_analysis),enabling_analysis:cbc_quick_cfg_analysis('COMPUTE_SDDBs_points','prop_COMPUTE_0',Res). | |
| 200 | %use_module(sap),use_module(enabling_analysis),enabling_analysis:cbc_quick_cfg_analysis('COMPUTE_SDDBs_points','COMPUTE_SDDBs_length',Res). | |
| 201 | ||
| 202 | % -------------------- DEPENDENCE ANALYSIS ---------------------- | |
| 203 | /* | |
| 204 | ||
| 205 | Independency between two actions in a B/Event-B model can be expressed also by means of LTL-formulas: | |
| 206 | 1. Two actions a and b are independent if the following LTL-formula is satisfied by the model: | |
| 207 | "G ((e(b) & [a] => X e(b)) & (e(a) & [b] => X e(a)))" (ind) | |
| 208 | 2. If (ind) is violated by the model then a and b are dependent actions. | |
| 209 | ||
| 210 | Note: The race_dependent condition cannot be covered by the above LTL-formula. If two actions are race dependent, but never simultaniously enabled in a state | |
| 211 | from the state space, then (ind) will be satisfied. | |
| 212 | ||
| 213 | */ | |
| 214 | ||
| 215 | tcltk_cbc_dependence_analysis(list([list(['Origin'|SOps])|Result])) :- | |
| 216 | %findall(Op, b_get_machine_operation(Op,_,_,_), Ops), sort(Ops,SOps), | |
| 217 | findall(Op, b_top_level_operation(Op), Ops), sort(Ops,SOps), | |
| 218 | findall(list([OpName1|EnableList]), | |
| 219 | (b_get_sorted_op(OpName1), | |
| 220 | findall(Enable,cbc_dependence_analysis(OpName1,_OpName2,Enable),EnableList)), | |
| 221 | Result). | |
| 222 | %,print_enable_table([list(['Origin'|Ops])|Result]). | |
| 223 | ||
| 224 | b_get_sorted_op(Op) :- findall(Op, b_top_level_operation(Op), Ops), | |
| 225 | sort(Ops,SOps), member(Op,SOps). | |
| 226 | ||
| 227 | cbc_dependence_analysis(OpName1,OpName2,Res) :- | |
| 228 | b_top_level_operation(OpName1), | |
| 229 | b_get_read_write_vars(OpName1,GReads1,AReads1,Reads1,Writes1), | |
| 230 | b_get_sorted_op(OpName2), | |
| 231 | (OpName1=OpName2 -> action_dependent_to_itself(OpName1,GReads1,Writes1,Res) % TO DO: check if it is possible that for two different parameter values of the same event there is dependence | |
| 232 | ; OpName2 @< OpName1 -> Res = '-' % our checking is symmetric; only check one pair | |
| 233 | ; otherwise -> | |
| 234 | b_get_read_write_vars(OpName2,GReads2,AReads2,Reads2,Writes2), | |
| 235 | formatsilent("CHECKING DEPENDENCE: ~w gr:~w / ar:~w / w:~w <--> ~w gr:~w / ar:~w / w:~w~n",[OpName1,GReads1,AReads1,Writes1,OpName2,GReads2,AReads2,Writes2]), | |
| 236 | ( syntactical_independence(Reads1,Writes1,Reads2,Writes2) -> Res = syntactic_independent | |
| 237 | ; my_ord_intersect(Writes1,Writes2) -> Res = race_dependent | |
| 238 | ; (my_ord_intersect(AReads1,Writes2);my_ord_intersect(AReads2,Writes1)) -> Res = race_dependent | |
| 239 | % TO DO: in this case check if there is indeed a race dependence (e.g. in scheduler new and ready_active are actually independent !) | |
| 240 | % Set up [OpName1,OpName2], [OpName2,OpName1] and see if for ord_intersect(Writes1,Writes2) we can find different values | |
| 241 | ; otherwise -> | |
| 242 | % get constraints for G_{Op_1} \leadsto{Op_2} not(G_{Op_1}) | |
| 243 | get_negated_guard(OpName1,PosGuard1,NegGuard1), | |
| 244 | get_conj_inv_predicate([NegGuard1],1,NegGuard1_Inv), | |
| 245 | % get constraints for G_{Op_2} \leadsto{Op_1} not(G_{Op_2}) | |
| 246 | get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 247 | get_conj_inv_predicate([NegGuard2],1,NegGuard2_Inv), | |
| 248 | conjunct_predicates([PosGuard1,PosGuard2],GuardsConj), | |
| 249 | ((my_ord_intersect(GReads1,Writes2),testcase_path_timeout_catch(pred(GuardsConj),500,[OpName2],NegGuard1_Inv,_Constants,_Ops,_TestS,_TI,R1)) | |
| 250 | -> formatsilent(" ~w may disable ~w (~w)!~n",[OpName2,OpName1,R1]), | |
| 251 | (is_timeout(R1) -> Res=timeout_dependent; Res = dependent) | |
| 252 | ; (my_ord_intersect(GReads2,Writes1),testcase_path_timeout_catch(pred(GuardsConj),500,[OpName1],NegGuard2_Inv,_,_,_,_,R2)) | |
| 253 | -> formatsilent(" ~w may disable ~w (~w)!~n",[OpName1,OpName2,R2]), | |
| 254 | (is_timeout(R2) -> Res=timeout_dependent; Res = dependent) | |
| 255 | ; Res = independent))). | |
| 256 | ||
| 257 | syntactical_independence(Reads1,Writes1,Reads2,Writes2) :- | |
| 258 | \+ my_ord_intersect(Writes1,Reads2), % op1 does not modify guard/effect of op2 | |
| 259 | \+ my_ord_intersect(Writes2,Reads1), % op2 does not modify guard/effect of op1 | |
| 260 | \+ my_ord_intersect(Writes1,Writes2). % no race condition | |
| 261 | ||
| 262 | % -------------- ENABLING ANALYSIS -------------- | |
| 263 | ||
| 264 | :- dynamic cbc_enable_analysis_cache/4. | |
| 265 | ||
| 266 | % check which operations can be enabled after executing another operation | |
| 267 | % to do: move maybe to another module; provide proper CSV export using Sebastian's modules | |
| 268 | cbc_enable_analysis(OpName1,OpName2,Enable,ExtraTimeout) :- | |
| 269 | init_or_op(OpName1), | |
| 270 | if(cbc_enable_analysis_cache(OpName1,OpName2,Result,ExtraTimeout), | |
| 271 | Result = Enable, % already computed | |
| 272 | (% now compute all enablings form OpName1 | |
| 273 | cbc_enable_analysis_calc(OpName1,Op2,R,ExtraTimeout), | |
| 274 | assert(cbc_enable_analysis_cache(OpName1,Op2,R,ExtraTimeout)), | |
| 275 | fail | |
| 276 | ; | |
| 277 | % now look up: | |
| 278 | cbc_enable_analysis_cache(OpName1,OpName2,Enable,ExtraTimeout) | |
| 279 | )). | |
| 280 | ||
| 281 | ||
| 282 | cbc_enable_analysis_calc(OpName1,OpName2,Enable,ExtraTimeout) :- | |
| 283 | OpName1='INITIALISATION',printsilent('CHECKING ENABLING AFTER INITIALISATION'),nls, | |
| 284 | b_top_level_operation(OpName2), | |
| 285 | printsilent('INITIALISATION'), printsilent(' ---> '), printsilent(OpName2), printsilent(' :: '), | |
| 286 | add_time_outs(ExtraTimeout,200,Timeout), | |
| 287 | ( testcase_path_timeout_catch(init,Timeout,[OpName2],b(truth,pred,[]),_Constants,_Ops,_TestS,_TI,R) | |
| 288 | -> printsilent(R), printsilent(' : '), | |
| 289 | get_negated_guard(OpName2,_,NegGuard), | |
| 290 | (testcase_path_timeout_catch(init,Timeout,[],NegGuard,_Constants2,_Ops2,_TestS2,_TI2,R2) | |
| 291 | -> printsilent(R2), printsilent(' : '),Enable=possible | |
| 292 | ; Enable=guaranteed) | |
| 293 | ; Enable=impossible), | |
| 294 | printsilent(Enable),nls. | |
| 295 | cbc_enable_analysis_calc(OpName1,OpName2,Enable,ExtraTimeout) :- | |
| 296 | b_top_level_operation(OpName1), | |
| 297 | b_get_operation_read_guard_vars(OpName1,true,Reads1), | |
| 298 | %get_negated_guard(OpName1,PosGuard1,_NegGuard1), | |
| 299 | formatsilent("CHECKING ENABLING AFTER: ~w r:~w / w:~w~n",[OpName1,Reads1,Writes1]), | |
| 300 | b_top_level_operation(OpName2), | |
| 301 | formatsilent('~w ---> ~w :: ',[OpName1,OpName2]), | |
| 302 | cbc_enable_calc_aux(OpName1,Writes1,OpName2,Enable,ExtraTimeout), | |
| 303 | formatsilent('Enable=~w~n',[Enable]). | |
| 304 | ||
| 305 | :- use_module(probporsrc(static_analysis),[syntactic_independence/3]). | |
| 306 | cbc_enable_calc_aux(OpName1,_Writes1,_OpName2,Enable,ExtraTimeout) :- | |
| 307 | (ExtraTimeout>500 -> infeasible_operation(OpName1) | |
| 308 | ; infeasible_operation_cache(OpName1)), % only check cached version | |
| 309 | !, | |
| 310 | Enable=infeasible. | |
| 311 | cbc_enable_calc_aux(_OpName1,_Writes1,OpName2,Enable,ExtraTimeout) :- | |
| 312 | (ExtraTimeout>500 -> infeasible_operation(OpName2) | |
| 313 | ; infeasible_operation_cache(OpName2)), % only check cached version | |
| 314 | !, | |
| 315 | Enable=impossible_infeasible. | |
| 316 | cbc_enable_calc_aux(OpName1,_Writes1,OpName2,Enable,_) :- | |
| 317 | % first check if we can syntactically determine independence | |
| 318 | syntactic_independence(OpName1,OpName2,Res), | |
| 319 | !, | |
| 320 | Enable=Res. | |
| 321 | cbc_enable_calc_aux(OpName1,Writes1,OpName2,Enable,ExtraTimeout) :- | |
| 322 | % now we do the semantic checks | |
| 323 | add_time_outs(ExtraTimeout,200,Timeout1), | |
| 324 | add_time_outs(ExtraTimeout,300,Timeout2), | |
| 325 | ||
| 326 | get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 327 | filter_predicate(PosGuard2,Writes1,FilteredPosGuard2), | |
| 328 | create_negation(FilteredPosGuard2,FilteredNegGuard2), | |
| 329 | cbc_enable_calc_aux2(OpName1,OpName2,Enable,Timeout1,Timeout2,PosGuard2,NegGuard2,FilteredNegGuard2). | |
| 330 | % TO DO: return timeout results and compute timeout info here | |
| 331 | ||
| 332 | ||
| 333 | cbc_enable_calc_aux2(OpName1,OpName2,Enable,Timeout1,Timeout2,PosGuard2,NegGuard2,FilteredNegGuard2) :- | |
| 334 | %format('Check if ~w can be enabled after ~w ~n',[OpName2,OpName1]), | |
| 335 | %print(' Pos Guard: '),translate:print_bexpr(PosGuard2),nl, | |
| 336 | %((OpName1=winc,OpName2=winc) -> trace ; true), | |
| 337 | testcase_path_timeout_catch(invariant,Timeout1,[OpName1],PosGuard2,_Csts,_Ops,_TestS,_TI,R), % advantage over version with [OpName1,OpName2] : one less state to setup and enumerate; but inner guards may not be checked | |
| 338 | !, | |
| 339 | printsilent(can_be_enabled_after(R)), printsilent(' : '), | |
| 340 | % print('Neg Guard: '),translate:print_bexpr(NegGuard2),nl, | |
| 341 | % TO DO: first check whether OpName2 can be disabled given Invariant ? | |
| 342 | (testcase_path_timeout_catch(invariant,Timeout1,[OpName1],NegGuard2,_Csts2,_Ops2,_TestS2,_TI2,R2) | |
| 343 | -> printsilent(can_be_disabled_after(R2)), printsilent(' : '), | |
| 344 | % TO DO: test if NegGuard2 holds initially it is possible to execute [OpName1,OpName2]; if not: OpName1 cannot enable OpName2, only keep it -> Enable=keep_possible | |
| 345 | % then we could check if OpName1 can disable OpName2: PosGuard2,[OpName1],NegGuard2 | |
| 346 | ((OpName1\=OpName2, % otherwise OpName2 must be enabled if [OpName1] can be executed | |
| 347 | %testcase_path_timeout_catch(pred(NegGuard2),Timeout2,[OpName1,OpName2],b(truth,pred,[]),_,_,_,_,R3) | |
| 348 | testcase_path_timeout_catch(pred(NegGuard2),Timeout2,[OpName1],PosGuard2,_,_,_,_,R3)) | |
| 349 | -> printsilent(can_enable(R3)), printsilent(' : '), | |
| 350 | %nl, translate:print_bexpr(PosGuard2),nl,print(OpName1),nl,translate:print_bexpr(NegGuard2),nl, | |
| 351 | %print('FILTERED: '), translate:print_bexpr(FilteredNegGuard2),nl, | |
| 352 | (testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4) | |
| 353 | -> printsilent(can_disable(R4)), printsilent(' : '), | |
| 354 | (contains_timeout([R,R2,R3,R4]) -> Enable=timeout_possible ; Enable=possible) | |
| 355 | ; (contains_timeout([R,R2,R3]) -> Enable=timeout_possible_enable ; Enable=possible_enable) /* Opname cannot disable OpName2; only enable it */ | |
| 356 | ) | |
| 357 | ; /* OpName1 cannot enable OpName2; only preserve it */ | |
| 358 | (testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4) | |
| 359 | -> printsilent(can_disable(R4)), printsilent(' : '), | |
| 360 | (contains_timeout([R,R2,R4]) -> Enable=timeout_possible_disable; Enable=possible_disable) | |
| 361 | ; (contains_timeout([R,R2]) -> Enable=timeout_keep; Enable=keep) /* Opname cannot enable or disable */ | |
| 362 | ) | |
| 363 | ) | |
| 364 | ; (is_timeout(R) -> Enable=timeout_guaranteed; Enable=guaranteed) | |
| 365 | ). | |
| 366 | cbc_enable_calc_aux2(OpName1,_OpName2,Enable,_Timeout1,Timeout2,PosGuard2,_NegGuard2,FilteredNegGuard2) :- | |
| 367 | % OpName2 can never be enabled after OpName1; check whether it can be enabled before | |
| 368 | % Note: we could replace FilteredNegGuard2 by truth | |
| 369 | testcase_path_timeout_catch(pred(PosGuard2),Timeout2,[OpName1],FilteredNegGuard2,_,_,_,_,R4), | |
| 370 | !, | |
| 371 | printsilent(can_disable(R4)), printsilent(' : '), | |
| 372 | (is_timeout(R4) -> Enable=timeout_impossible; Enable=impossible). | |
| 373 | cbc_enable_calc_aux2(_OpName1,_OpName2,Enable,_,_,_PosGuard2,_NegGuard2,_FilteredNegGuard2) :- | |
| 374 | % OpName2 can never ben enabled after nor before | |
| 375 | Enable=impossible_keep. | |
| 376 | ||
| 377 | ||
| 378 | % check if contains timeout or similar result | |
| 379 | contains_timeout(List) :- (member(timeout,List) -> true ; member(clpfd_overflow,List) -> true). | |
| 380 | ||
| 381 | ||
| 382 | :- use_module(bsyntaxtree,[conjunction_to_list/2,some_id_occurs_in_expr/2,create_negation/2]). | |
| 383 | % remove all predicates which are not modified | |
| 384 | filter_predicate(Pred,ModifiedVars,FilteredPred) :- partition_predicate(Pred,ModifiedVars,FilteredPred,_). | |
| 385 | ||
| 386 | % partition all predicates into those which are not modified and those that can be | |
| 387 | partition_predicate(Pred,'$all',FilteredPred,Rest) :- !, FilteredPred=Pred, Rest=b(truth,pred,[]). | |
| 388 | partition_predicate(Pred,ModifiedVars,FilteredPred,Rest) :- | |
| 389 | conjunction_to_list(Pred,List), | |
| 390 | partition(can_be_modified(ModifiedVars),List,FilteredList,[],UnFilteredList), | |
| 391 | conjunct_predicates(FilteredList,FilteredPred), | |
| 392 | conjunct_predicates(UnFilteredList,Rest). | |
| 393 | ||
| 394 | can_be_modified(ModifiedVars,Pred,Res) :- | |
| 395 | some_id_occurs_in_expr(ModifiedVars,Pred),!, Res='<'. | |
| 396 | can_be_modified(_,_,'>'). | |
| 397 | ||
| 398 | %predicate_modified_by_write_vars(_Pred,'$all') :- !. | |
| 399 | %predicate_modified_by_write_vars(Pred,SortedWriteVars) :- some_id_occurs_in_expr(SortedWriteVars,Pred). | |
| 400 | ||
| 401 | ||
| 402 | :- use_module(preferences,[get_time_out_preference_with_factor/2, add_time_outs/3]). | |
| 403 | tcltk_cbc_enabling_analysis(L) :- | |
| 404 | get_time_out_preference_with_factor(0.1,TOF), | |
| 405 | (TOF > 250 -> ExtraTO is TOF-250 ; ExtraTO = 0), | |
| 406 | tcltk_cbc_enabling_analysis(ExtraTO,L). | |
| 407 | tcltk_cbc_enabling_analysis(ExtraTimeout,list([list(['Origin'|Ops])|Result])) :- | |
| 408 | findall(Op, b_top_level_operation(Op), Ops), | |
| 409 | %statistics(walltime,[WT1,_]), | |
| 410 | findall(list([OpName1|EnableList]), | |
| 411 | (init_or_op(OpName1), | |
| 412 | findall(Enable,cbc_enable_analysis(OpName1,_OpName2,Enable,ExtraTimeout),EnableList)), | |
| 413 | Result). | |
| 414 | %statistics(walltime,[WT2,_]), Time is WT2-WT1, | |
| 415 | %format('Runtime for enabling analysis: ~w ms~n',[Time]) | |
| 416 | %,print_enable_table([list(['Origin'|Ops])|Result]). | |
| 417 | ||
| 418 | % ----------------- | |
| 419 | % compute the four edges of the enable relation for a particular operation | |
| 420 | tcltk_cbc_enabling_relations_for_operation(OpName2,ExtraTimeout, | |
| 421 | list([list(['Event','Enable','KeepEnabled','Disable','KeepDisabled'])|Results])) :- | |
| 422 | findall(list([OpName1|ResOp2]), | |
| 423 | compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,ResOp2), Results). | |
| 424 | tcltk_cbc_enabling_relations_after_operation(OpName1,ExtraTimeout, | |
| 425 | list([list(['Event','Enable','KeepEnabled','Disable','KeepDisabled'])|Results])) :- | |
| 426 | findall(list([OpName2|ResOp2]), | |
| 427 | compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,ResOp2), Results). | |
| 428 | ||
| 429 | % compute the four edges of the enable relation for a pair of events: | |
| 430 | compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]) :- | |
| 431 | b_top_level_operation(OpName1), | |
| 432 | b_get_operation_read_guard_vars(OpName1,true,Reads1), | |
| 433 | formatsilent("CHECKING ENABLING AFTER: ~w r:~w / w:~w~n",[OpName1,Reads1,Writes1]), | |
| 434 | b_top_level_operation(OpName2), | |
| 435 | get_negated_guard(OpName2,PosGuard2,_NegGuard2), | |
| 436 | partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2), | |
| 437 | create_negation(FilteredPosGuard2,FilteredNegGuard2), | |
| 438 | Timeout1 is 300+ExtraTimeout, | |
| 439 | formatsilent('~w ---> ~w :: ',[OpName1,OpName2]), | |
| 440 | %print(' FPOS: '),translate:print_bexpr(FilteredPosGuard2),nl, | |
| 441 | %print('Neg Guard: '),translate:print_bexpr(NegGuard2),nl, | |
| 442 | %print(' Filtered: '),translate:print_bexpr(FilteredNegGuard2),nl, | |
| 443 | % TO DO: use syntactic conditions | |
| 444 | my_testcase_path_timeout(pred(PosGuard2),Timeout1,[OpName1],FilteredPosGuard2,KeepEnabled), | |
| 445 | my_testcase_path_timeout(pred(PosGuard2),Timeout1,[OpName1],FilteredNegGuard2,Disable), | |
| 446 | (OpName1==OpName2 -> KeepDisabled=false, Enable=false | |
| 447 | ; conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2), % as StaticPosGuard2 must be same before after: it must be true before to be true after | |
| 448 | my_testcase_path_timeout(pred(NegEnableGuard2),Timeout1,[OpName1],FilteredPosGuard2,Enable), | |
| 449 | % this is the unoptimised call: | |
| 450 | %my_testcase_path_timeout(pred(NegGuard2),Timeout1,[OpName1],NegGuard2,KeepDisabled), | |
| 451 | % we do two calls for KeepDisabled: pred(NegStaticGuard2) true after, or StaticGuard2 & NegFiltered -> NegFiltered | |
| 452 | create_negation(StaticPosGuard2,StaticNegGuard2), | |
| 453 | my_testcase_path_timeout(pred(StaticNegGuard2),Timeout1,[OpName1],b(truth,pred,[]),KeepDisabled1), | |
| 454 | (KeepDisabled1 = ok -> KeepDisabled=ok | |
| 455 | ; my_testcase_path_timeout(pred(NegEnableGuard2),Timeout1,[OpName1],FilteredNegGuard2,KeepDisabled) | |
| 456 | ), | |
| 457 | formatsilent(' KeepEnabled=~w, Disable=~w, Enable=~w, KeepDisabled=~w~n', | |
| 458 | [KeepEnabled,Disable,Enable,KeepDisabled]) | |
| 459 | ). | |
| 460 | ||
| 461 | my_testcase_path_timeout(Before,Timeout,Path,After,Result) :- | |
| 462 | (testcase_path_timeout_catch(Before,Timeout,Path,After,_,_,_,_,Result) -> true | |
| 463 | ; Result = false). | |
| 464 | ||
| 465 | % ---------------------------------------------- | |
| 466 | ||
| 467 | % copy of predicat ein static_analysis to avoid meta_predicate error in Spider: | |
| 468 | :- meta_predicate catch_enumeration_warning(0,0). | |
| 469 | catch_enumeration_warning(Call,Handler) :- | |
| 470 | % throw/1 predicate raises instantiation_error | |
| 471 | on_exception(enumeration_warning(enumerating(_),_Type,_,_,critical),Call,call(Handler)). | |
| 472 | ||
| 473 | :- use_module(sap,[testcase_path_timeout/9]). | |
| 474 | testcase_path_timeout_catch(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res) :- | |
| 475 | catch_enumeration_warning(sap:testcase_path_timeout(Pred,TIMEOUT,Seq,P2,Csts,Ops,TestS,TI,Res), | |
| 476 | Res=virtual_time_out). | |
| 477 | ||
| 478 | init_or_op('INITIALISATION'). | |
| 479 | init_or_op(OpName1) :- b_top_level_operation(OpName1). %b_get_machine_operation(OpName1,_,_,_). | |
| 480 | ||
| 481 | % print table in CSV format | |
| 482 | print_enable_table(R) :- print_enable_table_list(R). | |
| 483 | print_enable_table_list([]) :- nl,nl. | |
| 484 | print_enable_table_list([list(L)|T]) :- | |
| 485 | print_csv_list(L), print_enable_table_list(T). | |
| 486 | print_csv_list([]) :- !,nl. | |
| 487 | print_csv_list([H]) :- !,print(H),nl. | |
| 488 | print_csv_list([H|T]) :- !,print(H), print(','), print_csv_list2(T). | |
| 489 | print_csv_list(X) :- print(illegal_list(X)),nl, add_internal_error('Illegal list: ', print_csv_list(X)). | |
| 490 | ||
| 491 | print_csv_list2([H]) :- !,print_enable_info(H),nl. | |
| 492 | print_csv_list2([H|T]) :- !,print_enable_info(H), print(','), print_csv_list2(T). | |
| 493 | print_csv_list2(X) :- print(illegal_list(X)),nl, add_internal_error('Illegal list: ', print_csv_list(X)). | |
| 494 | ||
| 495 | print_enable_info(I) :- (translate_enable_info(I,TI) -> print(TI) ; print_for_csv(I)). | |
| 496 | % simplify result further for output to CSV; reason: also testing (e.g., test 1360 which sometimes causes overflow on Mac, and time_out on Linux) | |
| 497 | translate_enable_info(timeout,unknown). | |
| 498 | translate_enable_info(time_out,unknown). | |
| 499 | translate_enable_info(overflow,unknown). | |
| 500 | translate_enable_info(virtual_time_out,unknown). | |
| 501 | ||
| 502 | print_for_csv([]) :- !, print('{}'). | |
| 503 | print_for_csv([H|T]) :- !, % print list without commas , | |
| 504 | format('{~w',[H]), maplist(print_csv_el,T), print('}'). | |
| 505 | print_for_csv(Term) :- print(Term). | |
| 506 | print_csv_el(H) :- format(' ~w',[H]). | |
| 507 | ||
| 508 | ||
| 509 | % ---------- create enable graph ------------------ | |
| 510 | ||
| 511 | eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,black) :- | |
| 512 | op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,_Color). | |
| 513 | eop_node_predicate('INITIALISATION',SubGraph,'INITIALISATION',Shape,Style,Color) :- SubGraph=none, | |
| 514 | Shape=hexagon, Style=none, Color=olivedrab2. | |
| 515 | ||
| 516 | translate_enable_res(Rel,_,_,'impossible',red,_) :- impossible(Rel),!, fail. | |
| 517 | translate_enable_res(guaranteed,_,_,'guaranteed',olivedrab2,solid) :- !. | |
| 518 | translate_enable_res(Rel,X,Y,TransRel,TCol,bold) :- independent(Rel,Col), | |
| 519 | !,X=Y, % only show if source & dest identical | |
| 520 | TransRel=Rel,TCol=Col. | |
| 521 | translate_enable_res(possible,_,_,'possible',black,solid) :- !. | |
| 522 | translate_enable_res(keep,_,_,'keep',lightgray,solid) :- !. | |
| 523 | translate_enable_res(possible_enable,_,_,'(enable)',black,solid) :- !. | |
| 524 | translate_enable_res(possible_disable,_,_,'(disable)',lightblue,solid) :- !. | |
| 525 | translate_enable_res(timeout_keep,_,_,'keep?',tomato,dashed) :- !. | |
| 526 | translate_enable_res(timeout_possible,_,_,'possible?',tomato,dashed) :- !. | |
| 527 | translate_enable_res(timeout_possible_disable,_,_,'(disable?)',tomato,dashed) :- !. | |
| 528 | translate_enable_res(timeout_possible_enable,_,_,'(enable?)',tomato,dashed) :- !. | |
| 529 | translate_enable_res(pred(Expr),_,_,String,black,dashed) :- !, | |
| 530 | translate_bexpression(Expr,String). | |
| 531 | translate_enable_res(predicate(Expr),_,_,String,black,dashed) :- !, | |
| 532 | translate_bexpression(Expr,String). | |
| 533 | translate_enable_res(dependent,_,_,dependent,green,solid) :- !. | |
| 534 | translate_enable_res(race_dependent,_,_,race_dependent,green,solid) :- !. | |
| 535 | translate_enable_res(X,_,_,'independent',lightgray,solid) :- | |
| 536 | memberchk(X,[independent,syntactic_independent,syntactic_fully_independent,syntactic_unchanged]),!. | |
| 537 | translate_enable_res(X,_,_,X,red,solid). | |
| 538 | ||
| 539 | impossible(impossible). | |
| 540 | impossible(impossible_keep). | |
| 541 | impossible(impossible_disable). | |
| 542 | impossible(impossible_infeasible). | |
| 543 | impossible(infeasible). | |
| 544 | ||
| 545 | independent(independent,yellow). | |
| 546 | independent(syntactic_keep,lightgray). | |
| 547 | independent(syntactic_independent,lightgray). | |
| 548 | independent(syntactic_fully_independent,lightgray). | |
| 549 | independent(syntactic_unchanged,lightgray). | |
| 550 | independent(activation_indepdendent,lightgray). | |
| 551 | ||
| 552 | is_timeout_enabling_result(timeout_keep). | |
| 553 | is_timeout_enabling_result(timeout_possible). | |
| 554 | is_timeout_enabling_result(timeout_possible_disable). | |
| 555 | is_timeout_enabling_result(timeout_possible_enable). | |
| 556 | is_timeout_enabling_result(timeout). | |
| 557 | is_timeout_enabling_result(timeout_dependent). | |
| 558 | is_timeout_enabling_result(timeout_guaranteed). | |
| 559 | is_timeout_enabling_result(timeout_impossible). | |
| 560 | ||
| 561 | % Simultaneous Enabling Analysis | |
| 562 | % Find events which cannot be enabled simultaneously | |
| 563 | % Usage: | |
| 564 | % a) if one event is known to be enabled we do not need to check the impossible ones | |
| 565 | % b) if one event is known to be disabled we do not need check events which guarantee it | |
| 566 | ||
| 567 | % use_module(enabling_analysis), tcltk_cbc_simultaneous_enabling_analysis(R). | |
| 568 | ||
| 569 | tcltk_cbc_simultaneous_enabling_analysis(list([list(['Origin'|SOps])|Result])) :- | |
| 570 | findall(Op, b_top_level_operation(Op), Ops), | |
| 571 | sort(Ops,SOps), % sort operations to ensure nice triangular display | |
| 572 | statistics(walltime,[WT1,_]), | |
| 573 | findall(list([OpName1|EnableList]), | |
| 574 | (member(OpName1,SOps), | |
| 575 | findall(SimulRes,tcltk_simult(OpName1,SOps,SimulRes),EnableList)), | |
| 576 | Result), | |
| 577 | statistics(walltime,[WT2,_]), Time is WT2-WT1, | |
| 578 | formatsilent('Runtime for simultaneous enabling analysis: ~w ms~n',[Time]) | |
| 579 | . %,print_enable_table([list(['Origin'|Ops])|Result]). | |
| 580 | ||
| 581 | tcltk_simult(Op1,SOps,Res) :- member(Op2,SOps),tcltk_simult2(Op1,Op2,Res). | |
| 582 | tcltk_simult2(Op1,Op2,Res) :- | |
| 583 | Op1 = Op2, % Op2 @=< Op1, % the simultaneous impossible analysis is symmetric: TO DO: do not compute/display info twice | |
| 584 | !, | |
| 585 | Res = '-'. | |
| 586 | tcltk_simult2(Op1,Op2,TRes) :- | |
| 587 | simult_enable_analysis(Op1,Op2,1,fixed_time_out(150),TRes). | |
| 588 | ||
| 589 | simult_enable_analysis(OpName1,OpName2,UseInvariant,TimeoutFactor,Res) :- | |
| 590 | b_top_level_operation(OpName1), | |
| 591 | b_top_level_operation(OpName2), | |
| 592 | %OpName2 @>OpName1, | |
| 593 | get_negated_guard(OpName1,PosGuard1,_NegGuard1), | |
| 594 | get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 595 | get_conj_inv_predicate([PosGuard1,PosGuard2],UseInvariant,Pred), | |
| 596 | %print(checking_simultaneous(OpName1,OpName2)),nl, | |
| 597 | (solve_predicate_with_chr(Pred,_State,TimeoutFactor,[],RR) | |
| 598 | -> %print(state(_State)),nl, print(result(RR)),nl, | |
| 599 | ((RR = contradiction_found ; RR = no_solution_found(unfixed_deferred_sets)) | |
| 600 | -> Res = impossible % we do not compute PosGuard1,NegGuard2 in this case: otherwise this would mean that Operation 1 can never fire ! | |
| 601 | ; get_conj_inv_predicate([PosGuard1,NegGuard2],UseInvariant,Pred2), | |
| 602 | solve_predicate_with_chr(Pred2,_State2,TimeoutFactor,[],RR2), | |
| 603 | combine_simult_result(RR,RR2,Res)) | |
| 604 | ; print('********* ERROR ***********'),nl,fail). | |
| 605 | ||
| 606 | combine_simult_result(solution(_),solution(_),R) :- !,R=possible. | |
| 607 | combine_simult_result(solution(_),B,R) :- | |
| 608 | (B = contradiction_found ; B = no_solution_found(unfixed_deferred_sets)), !, | |
| 609 | R=guaranteed. | |
| 610 | combine_simult_result(A,B,Res) :- functor(A,FA,_), functor(B,FB,_), | |
| 611 | ajoin([FA,'_',FB],Res). | |
| 612 | ||
| 613 | % --------------------------------------------------- | |
| 614 | ||
| 615 | :- use_module(eventhandling,[register_event_listener/3]). | |
| 616 | :- register_event_listener(specification_initialised,reset_enabling_analysis, | |
| 617 | 'Initialise module enabling analysis.'). | |
| 618 | ||
| 619 | :- dynamic feasible_operation_cache/2. | |
| 620 | reset_enabling_analysis :- | |
| 621 | %retractall(disable_graph(_)), | |
| 622 | retractall(feasible_operation_cache(_,_)), | |
| 623 | retractall(cbc_enable_analysis_cache(_,_,_,_)). | |
| 624 | ||
| 625 | % in principle you should only call this for Op with operation_name_not_yet_covered(Op) | |
| 626 | feasible_operation(Op,Res) :- feasible_operation_cache(Op,CR),!,Res=CR. | |
| 627 | feasible_operation(Op,Res) :- UseInvariant=1, | |
| 628 | check_if_feasible_operation(Op,UseInvariant,fixed_time_out(500),CR,_), | |
| 629 | assert(feasible_operation_cache(Op,CR)), | |
| 630 | Res=CR. | |
| 631 | ||
| 632 | feasible_operation_with_timeout(Op,TimeOut,Res) :- feasible_operation_cache(Op,CR), | |
| 633 | (CR \= unknown ; TimeOut =< 500), !, Res=CR. | |
| 634 | feasible_operation_with_timeout(Op,TimeOut,Res) :- check_if_feasible_operation(Op,1,fixed_time_out(TimeOut),CR,_), | |
| 635 | retractall(feasible_operation_cache(Op,_)), % must be unknown if it was asserted before | |
| 636 | assert(feasible_operation_cache(Op,CR)), | |
| 637 | Res=CR. | |
| 638 | ||
| 639 | ||
| 640 | :- use_module(state_space,[operation_not_yet_covered/1]). | |
| 641 | infeasible_operation(Op) :- feasible_operation_cache(Op,CR),!, CR=impossible. | |
| 642 | infeasible_operation(Op) :- operation_not_yet_covered(Op), | |
| 643 | feasible_operation(Op,impossible). % will also assert feasible_operation_cache | |
| 644 | ||
| 645 | infeasible_operation_cache(Op) :- feasible_operation_cache(Op,impossible). | |
| 646 | ||
| 647 | :- use_module(solver_interface, [solve_predicate/5]). | |
| 648 | solve_predicate_with_chr(Pred,State,TimeoutFactor,Options,RR) :- | |
| 649 | solve_predicate(Pred,State,TimeoutFactor,['CHR','CLPFD','SMT'|Options],RR). | |
| 650 | ||
| 651 | :- use_module(debug, [debug_mode/1]). | |
| 652 | :- use_module(store,[normalise_store/2]). | |
| 653 | % check if an operation is feasible | |
| 654 | % UseInvariant = 1 : assume invariant | |
| 655 | check_if_feasible_operation(OpName1,UseInvariant,TimeoutFactor,Res,NormalisedResultState) :- | |
| 656 | b_top_level_operation(OpName1), | |
| 657 | (debug_mode(on) | |
| 658 | -> print(checking_feasibility(OpName1)),nl,tools:start_ms_timer(TIMER) ; true), | |
| 659 | if(check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,State),true, | |
| 660 | (add_internal_error('Failed:',check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,State)),fail)), | |
| 661 | % TO DO: add missing variables and put into order | |
| 662 | if(normalise_store(State,NormalisedResultState),true, | |
| 663 | NormalisedResultState=State), | |
| 664 | %b_interpreter:sort_variable_binding(NormalisedResultState,SortedStore), | |
| 665 | (debug_mode(on) -> tools:stop_ms_timer_with_msg(TIMER,feasible(OpName1)) ; true). | |
| 666 | ||
| 667 | ||
| 668 | :- use_module(tools_timeout,[get_time_out_with_factor/2]). | |
| 669 | check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,ResultState) :- | |
| 670 | get_negated_guard(OpName1,PosGuard1,_NegGuard1,Precise), | |
| 671 | % format('Guard is ~w for ~w~n',[Precise,OpName1]), | |
| 672 | Precise = precise, | |
| 673 | !, | |
| 674 | % Warning: guard is under approximation for sequential composition, while loops, ... | |
| 675 | get_conj_inv_predicate([PosGuard1],UseInvariant,Pred), | |
| 676 | (debug_mode(on) -> translate:nested_print_bexpr(Pred),nl ; true), | |
| 677 | % visualize_graph:print_predicate_dependency_as_graph_for_dot(Pred,'~/Desktop/out.dot'), | |
| 678 | (solve_predicate_with_chr(Pred,State,TimeoutFactor,[full_machine_state],RR) | |
| 679 | -> %print(state(_State)),nl, print(result(RR)),nl, | |
| 680 | ((RR=no_solution_found(unfixed_deferred_sets) ; RR = contradiction_found) | |
| 681 | -> Res = impossible, ResultState = '$UNKNOWN_STATE' | |
| 682 | %,format('Computing unsat core for infeasible ~w~n',[OpName1]),unsat_cores:unsat_core(Pred,Core),print('CORE: '),nl,translate:nested_print_bexpr_as_classicalb(Core),nl | |
| 683 | ; RR=solution(_) -> Res = possible, | |
| 684 | (debug_mode(on) -> print('SOLUTION: '),translate:print_bstate(State),nl ; true), | |
| 685 | ResultState = State | |
| 686 | ; simplify_for_output(RR,Res), ResultState = '$UNKNOWN_STATE' ) | |
| 687 | ; add_internal_error('Failed to compute feasibility for: ',OpName1), | |
| 688 | translate:print_bexpr(Pred),nl, | |
| 689 | Res = internal_error, ResultState = '$UNKNOWN_STATE'). | |
| 690 | check_if_feasible_operation2(OpName1,UseInvariant,TimeoutFactor,Res,ResultState) :- | |
| 691 | formatsilent('Guard computation is imprecise for ~w. Not using predicate solver (but B interpreter).~n',[OpName1]), | |
| 692 | % this version uses sap:testcase_path: this works for things like sequential composition and WHILE loops better | |
| 693 | get_time_out_with_factor(TimeoutFactor,TO), | |
| 694 | (UseInvariant=1 -> INV=invariant ; INV=typing), | |
| 695 | (testcase_path_timeout_catch(INV,TO,[OpName1],b(truth,pred,[]),_Constants,Ops,StateSequence,_TI,R1) | |
| 696 | -> (is_timeout(R1) -> Res=timeout ; Res = possible), | |
| 697 | (nonvar(StateSequence),StateSequence=[ResultState|_] -> true ; ResultState = '$UNKNOWN_STATE'), | |
| 698 | (debug_mode(off) -> true | |
| 699 | ; print(feasibility_result(OpName1,R1,Ops)),nl, | |
| 700 | (ResultState = '$UNKNOWN_STATE' -> true | |
| 701 | ; print('SOLUTION: '),translate:print_bstate(ResultState),nl) | |
| 702 | ) | |
| 703 | ; Res=impossible,ResultState = '$UNKNOWN_STATE'). | |
| 704 | ||
| 705 | ||
| 706 | simplify_for_output(no_solution_found(enumeration_warning(_,_,_,_,_)),virtual_time_out). | |
| 707 | simplify_for_output(no_solution_found(clpfd_overflow),overflow). | |
| 708 | simplify_for_output(time_out,time_out). | |
| 709 |