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