| 1 | | % (c) 2009-2023 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 | | |