| 1 | % (c) 2009-2026 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(b_operation_guards,[ | |
| 6 | ||
| 7 | get_quantified_operation_enabling_condition/5, % unsimplified or simplified, fully quantified | |
| 8 | get_operation_enabling_condition/7, | |
| 9 | get_unsimplified_operation_guard/2, | |
| 10 | get_unsimplified_operation_enabling_condition/5, | |
| 11 | get_simplified_operation_enabling_condition/5, | |
| 12 | ||
| 13 | get_operation_propositional_guards/3, | |
| 14 | get_operation_propositional_guards/6, | |
| 15 | ||
| 16 | get_substitution_enabling_condition/4 % get the enabling condition of a particular substitution | |
| 17 | ]). | |
| 18 | ||
| 19 | :- use_module(module_information,[module_info/2]). | |
| 20 | :- module_info(group,ast). | |
| 21 | :- module_info(description,'Compute guard predicates of operations.'). | |
| 22 | ||
| 23 | ||
| 24 | :- use_module(tools). | |
| 25 | :- use_module(bsyntaxtree). | |
| 26 | :- use_module(bmachine,[b_top_level_operation/1, | |
| 27 | b_get_machine_operation_for_animation/6, b_get_machine_operation_for_animation/4, | |
| 28 | b_get_machine_operation/6, bmachine_is_precompiled/0]). | |
| 29 | :- use_module(b_interpreter_components,[construct_optimized_exists/3,construct_optimized_exists/4]). | |
| 30 | :- use_module(specfile,[animation_minor_mode/1]). | |
| 31 | :- use_module(external_functions,[external_subst_enabling_condition/3]). | |
| 32 | :- use_module(b_ast_cleanup, [clean_up/3]). | |
| 33 | :- use_module(debug). | |
| 34 | :- use_module(error_manager). | |
| 35 | ||
| 36 | :- use_module(library(lists)). | |
| 37 | :- use_module(library(ordsets)). | |
| 38 | ||
| 39 | ||
| 40 | ||
| 41 | :- dynamic obtain_action_enabling_conditions/0, simplify_enabling_condition/1. | |
| 42 | simplify_enabling_condition(true). | |
| 43 | set_simplify_enabling_condition(X) :- retractall(simplify_enabling_condition(_)), | |
| 44 | assertz(simplify_enabling_condition(X)). | |
| 45 | ||
| 46 | obtain_action_enabling_conditions. | |
| 47 | set_obtain_action_enabling_conditions(auto_obtain) :- !, | |
| 48 | (animation_minor_mode(eventb) -> GetFromAction=false | |
| 49 | ; GetFromAction=true), set_obtain_action_enabling_conditions(GetFromAction). | |
| 50 | set_obtain_action_enabling_conditions(true) :- !, | |
| 51 | (obtain_action_enabling_conditions -> true ; assertz(obtain_action_enabling_conditions)). | |
| 52 | set_obtain_action_enabling_conditions(_) :- retractall(obtain_action_enabling_conditions). | |
| 53 | ||
| 54 | ||
| 55 | get_unsimplified_operation_guard(OpName,Guard) :- | |
| 56 | get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise), | |
| 57 | construct_optimized_exists(Parameters,EnablingCondition,Guard). | |
| 58 | ||
| 59 | get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :- | |
| 60 | Simplify=false, | |
| 61 | ? | get_operation_enabling_condition(OpName,Parameters,EnablingCondition, |
| 62 | BecomesSuchVars,Precise,auto_obtain,Simplify). | |
| 63 | ||
| 64 | get_simplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :- | |
| 65 | Simplify=true, | |
| 66 | get_operation_enabling_condition(OpName,Parameters,EnablingCondition, | |
| 67 | BecomesSuchVars,Precise,auto_obtain,Simplify). | |
| 68 | ||
| 69 | ||
| 70 | % get a quantified predicate, Precise is either precise or imprecise | |
| 71 | get_quantified_operation_enabling_condition(OpName, BExpr, BecomesSuchVars, Precise, Simplify) :- | |
| 72 | get_operation_enabling_condition(OpName,IDs,Condition, | |
| 73 | BecomesSuchVars,Precise,auto_obtain,Simplify), | |
| 74 | create_or_merge_exists(IDs, Condition, BExpr). | |
| 75 | ||
| 76 | :- use_module(bmachine,[b_operation_reads_output_variables/3]). % ALLOW_OUTPUT_READING | |
| 77 | ||
| 78 | get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,IsPrecise,GetAct,Simplify) :- | |
| 79 | set_obtain_action_enabling_conditions(GetAct), % specify whether we want also conditions stemming from actions, such as :() or :: | |
| 80 | set_simplify_enabling_condition(Simplify), % specify whether we want to simplify the EnablingCondition if possible | |
| 81 | ? | b_get_machine_operation_for_animation(OpName,_Results,Parameters,TBody), |
| 82 | get_substitution_enabling_condition(TBody,EnablingCondition0,BecomesSuchVars,IsPreciseV), | |
| 83 | (b_operation_reads_output_variables(OpName,ReadOutputVariablesIds,_) | |
| 84 | -> debug_format(19,'Filtering guard of operation ~w which reads output variables ~w~n', | |
| 85 | [OpName,ReadOutputVariablesIds]), | |
| 86 | conjunction_to_list(EnablingCondition0,EL), | |
| 87 | exclude(guard_reads_output(ReadOutputVariablesIds),EL,EL2), | |
| 88 | (EL2=[] -> get_texpr_pos_infos(TBody,PosInfos),EnablingCondition = b(truth,pred,PosInfos) | |
| 89 | ; conjunct_predicates_with_pos_info(EL2,EnablingCondition) | |
| 90 | ), | |
| 91 | IsPrecise=imprecise | |
| 92 | ; var(IsPreciseV) -> IsPrecise = precise, EnablingCondition=EnablingCondition0 | |
| 93 | ; IsPrecise = imprecise, EnablingCondition=EnablingCondition0 | |
| 94 | ). | |
| 95 | ||
| 96 | guard_reads_output(OutputVars,Guard) :- | |
| 97 | find_identifier_uses(Guard,[],Ids), | |
| 98 | ord_intersect(Ids,OutputVars). | |
| 99 | ||
| 100 | get_substitution_enabling_condition(TBody,EnablingCondition,BecomesSuchVars,IsPrecise) :- | |
| 101 | get_texpr_expr(TBody,Body), get_texpr_pos_infos(TBody,PosInfos), | |
| 102 | ? | (get_operation_enabling_condition1(Body,PosInfos,Cond,BecomesSuchVars,IsPrecise) |
| 103 | -> (Cond = b(truth,_,_) | |
| 104 | -> create_texpr(truth,pred,PosInfos,EnablingCondition) % ensure bvisual2 will report reasonable location | |
| 105 | % otherwise we may get the location within a sequential composition within a subsidiary operation call | |
| 106 | ; EnablingCondition = Cond) | |
| 107 | ; add_internal_error('Getting enabling condition failed: ',Body), | |
| 108 | create_texpr(truth,pred,PosInfos,EnablingCondition), | |
| 109 | BecomesSuchVars=[]). | |
| 110 | ||
| 111 | get_operation_enabling_condition1(if(IfList),PosInfos,Res,BecomesSuchVars,IsPrecise) :- !, | |
| 112 | ? | maplist5(get_if_condition(IsPrecise),IfList,Tests,Conds,BecomesSuchVars1), |
| 113 | append(BecomesSuchVars1,BecomesSuchVars), | |
| 114 | ? | (member(X,Conds), \+ is_truth(X) |
| 115 | -> disjoin_ifs(Tests,Conds,[],L), | |
| 116 | conjunct_predicates_with_pos_info(L,Res) | |
| 117 | ; create_texpr(truth,pred,PosInfos,Res) % all branches have no enabling condition | |
| 118 | ). | |
| 119 | get_operation_enabling_condition1(Subst,PosInfos,Truth,[],_Prcise) :- | |
| 120 | basic_has_no_enabling_condition(Subst),!, | |
| 121 | create_texpr(truth,pred,PosInfos,Truth). | |
| 122 | get_operation_enabling_condition1(case(A,_,_),PosInfos,Truth,[],imprecise) :- !, | |
| 123 | % CASE is now translated to LET + IF-THEN-ELSE in b_ast_cleanup | |
| 124 | print('Not computing enabling for CASE: '), translate:print_bexpr(A),nl, | |
| 125 | create_texpr(truth,pred,PosInfos,Truth). | |
| 126 | get_operation_enabling_condition1(becomes_element_of(_LHS,RHS),PosInfos,Res,[],_Precise) :- | |
| 127 | obtain_action_enabling_conditions, | |
| 128 | get_texpr_expr(RHS,RHSExpr),get_texpr_type(RHS,Type),!, | |
| 129 | (simplify_enabling_condition(true), | |
| 130 | definitely_not_empty(RHSExpr,Type) | |
| 131 | -> create_texpr(truth,pred,PosInfos,Res) | |
| 132 | ; create_texpr(empty_set,Type,[],EmptySet), | |
| 133 | safe_create_texpr(not_equal(RHS,EmptySet),pred,PosInfos,Res2), | |
| 134 | clean_up(Res2,[],Res) | |
| 135 | ). | |
| 136 | get_operation_enabling_condition1(Body,_,EnablingCondition,BecomesSuchVars,IsPrecise) :- | |
| 137 | ? | get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars,IsPrecise),!. |
| 138 | get_operation_enabling_condition1(X,PosInfos,Truth,[],imprecise) :- %print(cannot_obtain(X)),nl, | |
| 139 | (obtain_action_enabling_conditions | |
| 140 | -> functor(X,F,A),debug_println(9,cannot_obtain_enabling(F/A,X)) ; true), | |
| 141 | create_texpr(truth,pred,PosInfos,Truth). | |
| 142 | ||
| 143 | /* TO DO: recursively expand the code below for more complicated SELECT,ANY,... */ | |
| 144 | get_operation_enabling_condition2(precondition(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % PRE | |
| 145 | get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise), | |
| 146 | conjunct_predicates_with_pos_info(PreCond,RC,Res). | |
| 147 | get_operation_enabling_condition2(assertion(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ASSERT | |
| 148 | get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise). | |
| 149 | get_operation_enabling_condition2(witness_then(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % WITNESS | |
| 150 | get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise). | |
| 151 | get_operation_enabling_condition2(block(TBody),Res,BecomesSuchVars,IsPrecise) :- !, % BEGIN ... END | |
| 152 | get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise). | |
| 153 | get_operation_enabling_condition2(choice(ChoiceList),Res,BecomesSuchVars,IsPrecise) :- !, % CHOICE ... OR ... | |
| 154 | get_disjunction_of_enabling_conditions(ChoiceList,Res,BecomesSuchVars,IsPrecise). | |
| 155 | get_operation_enabling_condition2(var(_Parameters,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % VAR | |
| 156 | % should the Parameters be added somewhere ? should we create an exists | |
| 157 | % In principle the enabling condition should be true, as we have a low-level construct | |
| 158 | get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise). | |
| 159 | get_operation_enabling_condition2(sequence(TSeq),Res,BecomesSuchVars,IsPrecise) :- !, % sequential composition ; | |
| 160 | get_enabling_cond_for_sequence(TSeq,Res,BecomesSuchVars,IsPrecise). | |
| 161 | get_operation_enabling_condition2(lazy_let_subst(ID,ExprOrPred,TBody),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 162 | Res = b(lazy_let_pred(ID,ExprOrPred,BodyRes),pred,[]), | |
| 163 | get_substitution_enabling_condition(TBody,BodyRes,BecomesSuchVars,IsPrecise). | |
| 164 | get_operation_enabling_condition2(let(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % LET | |
| 165 | % for the moment: treat like ANY, but we could avoid introducing existential quantifier ?! | |
| 166 | ? | get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise). |
| 167 | get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ANY | |
| 168 | get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise), | |
| 169 | conjunct_predicates_with_pos_info(PreCond,RC,Res1), | |
| 170 | simplify_enabling_condition(Simplify), | |
| 171 | ? | construct_optimized_exists(Parameters,Res1,Res,Simplify). |
| 172 | %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)]),Res,BecomesSuchVars) :- !, | |
| 173 | % get_texpr_expr(TBody,Body), | |
| 174 | % get_operation_enabling_condition2(Body,RC,BecomesSuchVars), | |
| 175 | % conjunct_predicates([PreCond,RC],Res). | |
| 176 | %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)],b(skip,_,_)),Res,BecomesSuchVars) :- !, | |
| 177 | % get_texpr_expr(TBody,Body), | |
| 178 | % get_operation_enabling_condition2(Body,RC,BecomesSuchVars), | |
| 179 | % conjunct_predicates([PreCond,RC],Res). | |
| 180 | get_operation_enabling_condition2(select_when(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 181 | get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise), | |
| 182 | conjunct_predicates_with_pos_info(PreCond,RC,Res). | |
| 183 | get_operation_enabling_condition2(select(ListOfWhens),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 184 | get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise). | |
| 185 | get_operation_enabling_condition2(select(ListOfWhens,Else),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 186 | get_texpr_exprs(ListOfWhens,ListOfSelectWhens), | |
| 187 | maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1), | |
| 188 | get_substitution_enabling_condition(Else,ResElse,ElseBecomesSuchVars,IsPrecise), | |
| 189 | disjunct_predicates([ResElse|Res1],Res), | |
| 190 | append([ElseBecomesSuchVars|BecomesSuchVars1],BecomesSuchVars). | |
| 191 | get_operation_enabling_condition2(parallel([TH|T]),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 192 | get_substitution_enabling_condition(TH,E1,BecomesSuchVarsH,IsPrecise), | |
| 193 | (T=[] -> Res=E1, BecomesSuchVarsH=BecomesSuchVars | |
| 194 | ; get_operation_enabling_condition2(parallel(T),E2,BecomesSuchVarsT,IsPrecise), | |
| 195 | append(BecomesSuchVarsH,BecomesSuchVarsT,BecomesSuchVars), | |
| 196 | conjunct_predicates_with_pos_info(E1,E2,Res) | |
| 197 | ). | |
| 198 | get_operation_enabling_condition2(becomes_such(Vars,Condition),Res,Vars,_Precise) :- % Vars : (Condition) | |
| 199 | % example x: (x$0 >= 1 & x=x$0+1) | |
| 200 | obtain_action_enabling_conditions,!, | |
| 201 | simplify_enabling_condition(Simplify), | |
| 202 | ? | construct_optimized_exists(Vars,Condition,Res1,Simplify), |
| 203 | %translate:print_bexpr(Res1),nl, | |
| 204 | % e.g, for example above we have #x.(x$0 >= 1 & x=x$0+1) -> x$0 >= 1 | |
| 205 | % now rename $0 variables to act on current state to obtain the condition: | |
| 206 | findall(rename(BeforeId,Id), | |
| 207 | (member(b(identifier(Id),_,Infos),Vars), | |
| 208 | member(before_substitution(_,BeforeId),Infos)), | |
| 209 | RenameList), | |
| 210 | rename_bt(Res1,RenameList,Res). % for example above: Res is x >= 1 | |
| 211 | get_operation_enabling_condition2(rlevent(_Name,_Section,_Status,_Params,Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),Res,BecomesSuchVars,IsPrecise) :- !, | |
| 212 | %print(actions(Actions)),nl, | |
| 213 | % TO DO: have a look at get_full_eventb_guard. Do we want to recurse through the abstractions ? | |
| 214 | (obtain_action_enabling_conditions | |
| 215 | -> get_operation_enabling_for_event_b_actions(Actions,Guard,Res,BecomesSuchVars,IsPrecise) | |
| 216 | ; Res=Guard,BecomesSuchVars=[]). | |
| 217 | get_operation_enabling_condition2(while(Cond,_,_,_),Truth,[],imprecise) :- !, | |
| 218 | debug_println(9,enabling_for_while_assumed_true), | |
| 219 | get_texpr_pos_infos(Cond,PosInfos), | |
| 220 | create_texpr(truth,pred,PosInfos,Truth). | |
| 221 | get_operation_enabling_condition2(external_subst_call(Pred,Args),Res,[],_Precise) :- | |
| 222 | external_subst_enabling_condition(Pred,Args,Cond),!, Res=Cond. | |
| 223 | get_operation_enabling_condition2(operation_call(Operation,OpCallResults,OpCallParas),Res,BecomeSuchVars,IsPrecise) :- | |
| 224 | def_get_texpr_id(Operation,op(OperationName)), TopLevel=false, | |
| 225 | b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel), | |
| 226 | bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParas,Body2), | |
| 227 | (b_operation_reads_output_variables(OperationName,[_|_],_) | |
| 228 | -> bsyntaxtree:replace_ids_by_exprs(Body2,OpResults,OpCallResults,Body3) | |
| 229 | ; Body3=Body2 | |
| 230 | ), | |
| 231 | !, | |
| 232 | %print(get_enabling_for_opcall),nl,translate:print_subst(Body2),nl, | |
| 233 | get_substitution_enabling_condition(Body3,Res,BecomeSuchVars,IsPrecise). | |
| 234 | ||
| 235 | % check if an substitution obviously has no guard/pre condition | |
| 236 | basic_has_no_enabling_condition(assign(_LHS,_RHS)). | |
| 237 | basic_has_no_enabling_condition(assign_single_id(_LHS,_RHS)). | |
| 238 | basic_has_no_enabling_condition(skip). | |
| 239 | ||
| 240 | % recursive version; also traversing other constructs | |
| 241 | has_no_enabling_condition(E) :- basic_has_no_enabling_condition(E). | |
| 242 | has_no_enabling_condition(parallel(L)) :- maplist(has_no_enabling_t_cond,L). | |
| 243 | has_no_enabling_condition(sequence(L)) :- maplist(has_no_enabling_t_cond,L). | |
| 244 | has_no_enabling_condition(choice(L)) :- maplist(has_no_enabling_t_cond,L). | |
| 245 | has_no_enabling_condition(block(T)) :- has_no_enabling_t_cond(T). | |
| 246 | has_no_enabling_condition(var(_,T)) :- has_no_enabling_t_cond(T). | |
| 247 | has_no_enabling_condition(if(L)) :- maplist(has_no_enabling_ifte_cond,L). | |
| 248 | % TODO: SELECT WITH ELSE, becomes_such with full type, certain external_subst_call, operation_call | |
| 249 | ||
| 250 | has_no_enabling_t_cond(b(E,_,_)) :- has_no_enabling_condition(E). | |
| 251 | has_no_enabling_ifte_cond(b(if_elsif(_Test,TBody),_,_)) :- has_no_enabling_condition(TBody). | |
| 252 | ||
| 253 | ||
| 254 | get_enabling_cond_for_sequence([],b(truth,pred,[]),[],_Precise). | |
| 255 | get_enabling_cond_for_sequence([b(assign_single_id(LHS,RHS),subst,_)|T],Res,BecomesSuchVars,IsPrecise) :- | |
| 256 | get_texpr_id(LHS,ID), | |
| 257 | !, % TODO: also support f(X) := ... | |
| 258 | get_enabling_cond_for_sequence(T,TRes,BecomesSuchVars,IsPrecise), | |
| 259 | replace_id_by_expr(TRes,ID,RHS,Res). | |
| 260 | get_enabling_cond_for_sequence([b(assign(LHS,RHS),subst,_)|T],Res,BecomesSuchVars,IsPrecise) :- | |
| 261 | get_texpr_ids(LHS,IDs), | |
| 262 | !, % TODO: also support f(X), := ... | |
| 263 | get_enabling_cond_for_sequence(T,TRes,BecomesSuchVars,IsPrecise), | |
| 264 | replace_ids_by_exprs(TRes,IDs,RHS,Res). | |
| 265 | get_enabling_cond_for_sequence([TBody1|Tail],Res,BecomesSuchVars,IsPrecise) :- | |
| 266 | get_substitution_enabling_condition(TBody1,Res,BecomesSuchVars,IsPrecise), | |
| 267 | (nonvar(IsPrecise) -> true | |
| 268 | ; maplist(has_no_enabling_condition,Tail) -> true | |
| 269 | ; IsPrecise = imprecise | |
| 270 | ), | |
| 271 | (debug_mode(on), nonvar(IsPrecise), Tail = [Tail1|_] | |
| 272 | -> add_message(b_operation_guards,'Ignoring potential enabling condition in sequence after: ',TBody1,Tail1) | |
| 273 | ; true). | |
| 274 | % TO DO: compute before-after predicate of TBody1 ? before_after_predicate_list_conjunct_with_equalities ? | |
| 275 | ||
| 276 | get_if_condition(IsPrecise,b(if_elsif(Test,TBody),_,_),Test,Condition,BecomesSuchVars) :- | |
| 277 | get_substitution_enabling_condition(TBody,Condition,BecomesSuchVars,IsPrecise). | |
| 278 | ||
| 279 | :- use_module(bsyntaxtree, [create_implication/3]). | |
| 280 | disjoin_ifs([],[],_,[]). | |
| 281 | disjoin_ifs([Test|TT],[EnableCond|TC],NegSoFar,[Res1|TR]) :- | |
| 282 | append(NegSoFar,[Test],L), | |
| 283 | conjunct_predicates_with_pos_info(L,BranchTest), | |
| 284 | create_implication(BranchTest,EnableCond,Res1), % ELSEIF Test THEN Body ... ---> NegSoFar & Test => EnableCond | |
| 285 | create_negation(Test,NTest), | |
| 286 | append(NegSoFar,[NTest],NegSoFar1), % add negation of test as additional test for rest | |
| 287 | disjoin_ifs(TT,TC,NegSoFar1,TR). | |
| 288 | ||
| 289 | ||
| 290 | % for a list of substitutions: get enabling conditions and disjoin them | |
| 291 | get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise) :- | |
| 292 | get_texpr_exprs(ListOfWhens,ListOfSelectWhens), | |
| 293 | maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1), | |
| 294 | disjunct_predicates(Res1,Res), | |
| 295 | append(BecomesSuchVars1,BecomesSuchVars). | |
| 296 | get_operation_enabling_condition3(Precise,Exp,Res,BV) :- get_operation_enabling_condition2(Exp,Res,BV,Precise). | |
| 297 | ||
| 298 | % see more powerful definitely_not_empty_set | |
| 299 | definitely_not_empty(bool_set,_). | |
| 300 | definitely_not_empty(integer_set(_),_). | |
| 301 | definitely_not_empty(float_set,_). | |
| 302 | definitely_not_empty(real_set,_). | |
| 303 | definitely_not_empty(identifier(X),set(global(X))). % assume no local version of X overrides global X | |
| 304 | definitely_not_empty(string_set,_). | |
| 305 | ||
| 306 | ||
| 307 | ||
| 308 | % get operation enabling condition in context of an event-b action list: | |
| 309 | get_operation_enabling_for_event_b_actions([],Res,Res,[],_Precise). | |
| 310 | get_operation_enabling_for_event_b_actions([H|T],InRes,OutRes,BecomesSuchVars,IsPrecise) :- | |
| 311 | get_substitution_enabling_condition(H,ResH,HBecomesSuchVars,IsPrecise), | |
| 312 | conjunct_predicates_with_pos_info(InRes,ResH,IntRes), | |
| 313 | get_operation_enabling_for_event_b_actions(T,IntRes,OutRes,TBecomesSuchVars,IsPrecise), | |
| 314 | append(HBecomesSuchVars,TBecomesSuchVars,BecomesSuchVars). | |
| 315 | ||
| 316 | % --------------- | |
| 317 | :- use_module(bmachine,[b_top_level_operation/1]). | |
| 318 | % LTSMIN style guards: a guard that does not depend on parameters | |
| 319 | get_operation_propositional_guards(OpName,Guards,RestBody) :- | |
| 320 | b_top_level_operation(OpName), | |
| 321 | b_get_machine_operation_for_animation(OpName,TResults,TParameters,TBody), % requires bmachine to be precompiled | |
| 322 | get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody). | |
| 323 | ||
| 324 | :- use_module(translate,[print_bexpr/1]). | |
| 325 | % the following can be called directly; does not require bmachine to be pre-compiled | |
| 326 | get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody) :- | |
| 327 | get_texpr_ids(TParameters,Ids1), | |
| 328 | get_texpr_ids(TResults,Ids2), | |
| 329 | append(Ids1,Ids2,Ids), sort(Ids,Parameters), | |
| 330 | get_operation_guards_aux(TBody,Parameters,top,Guards,RestBody), | |
| 331 | (debug_mode(off) -> true | |
| 332 | ; format('OPERATION Guard Splitting ~w (~w)~n',[OpName,Parameters]), | |
| 333 | print('LTSMin Guards: '), maplist(print_bexpr,Guards),nl, | |
| 334 | print('LTSMin Body: '), translate:print_subst(RestBody),nl,nl | |
| 335 | ). | |
| 336 | ||
| 337 | :- use_module(bsyntaxtree, [conjunction_to_list/2,find_identifier_uses/3]). | |
| 338 | ||
| 339 | ||
| 340 | get_operation_guards_aux(Subst,Parameters,Top,Guards,OpBody) :- | |
| 341 | ? | get_guards(Subst,Top,TIds,Guard,InnerBody,Infos), |
| 342 | get_texpr_ids(TIds,Ids), sort(Ids,NewIds), | |
| 343 | ord_union(Parameters,NewIds,Parameters2), | |
| 344 | !, | |
| 345 | get_parameter_independent_guards(Guard,Parameters2,Indep,Dep), | |
| 346 | (Dep = [] | |
| 347 | -> OpBody = InnerOpBody % no need to keep b | |
| 348 | ; conjunct_predicates_with_pos_info(Dep,DepCond), | |
| 349 | construct_select(TIds,DepCond,InnerOpBody,Infos,OpBody) % we always produce a SELECT; even if we had a PRE as it will no longer be innermost ! we assume treat_outermost_pre_as_select is set to true for PRE (checked below) | |
| 350 | ), | |
| 351 | get_operation_guards_aux(InnerBody,Parameters2,inner,InnerGuards,InnerOpBody), | |
| 352 | append(Indep,InnerGuards,Guards). | |
| 353 | ||
| 354 | get_operation_guards_aux(b(rlevent(Name,Sect,Status,Params,EvGuard,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info), | |
| 355 | Parameters,_,Guards,OpBody) :- !, | |
| 356 | get_parameter_independent_guards(EvGuard,Parameters,InDepGuards,Dep), | |
| 357 | (get_variant_pred(Status,VariantPred) | |
| 358 | -> %print(op_variant(_Name)),nl,translate:print_bexpr(VariantPred),nl, | |
| 359 | % we virtually include the Variant expression in the read info; ensure that LTS Min knows that this will be read by the Event-B interpreter | |
| 360 | % TO DO: check if we need to add the witnesses as well ! | |
| 361 | Guards = [VariantPred|InDepGuards] | |
| 362 | ; Guards = InDepGuards), | |
| 363 | conjunct_predicates_with_pos_info(Dep,DepG), | |
| 364 | OpBody = b(rlevent(Name,Sect,Status,Params,DepG,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info). | |
| 365 | get_operation_guards_aux(TB,_,_,[],TB). | |
| 366 | ||
| 367 | ||
| 368 | :- use_module(bsyntaxtree, [safe_create_texpr/3]). | |
| 369 | % we integrate the Variant check into the guard to ensure the correct read matrix is produced | |
| 370 | % currently the Variant is checked upon event entry and for convergent events upon exit for decrease | |
| 371 | % in principle this should be more of an assertion_predicate or assertion_expression | |
| 372 | get_variant_pred(b(Status,status,_),Res) :- get_variant_pred_aux(Status,Res). | |
| 373 | get_variant_pred_aux(anticipated(Variant),Res) :- NATURAL = b(integer_set('NATURAL'),set(integer),[]), | |
| 374 | safe_create_texpr(member(Variant,NATURAL),pred,Res). | |
| 375 | get_variant_pred_aux(convergent(Variant),Res) :- NATURAL1 = b(integer_set('NATURAL1'),set(integer),[]), | |
| 376 | safe_create_texpr(member(Variant,NATURAL1),pred,Res). | |
| 377 | ||
| 378 | ||
| 379 | get_guards(b(precondition(Guard,TBody),subst,Info), top, [],Guard, TBody, Info) :- | |
| 380 | preferences:get_preference(treat_outermost_pre_as_select,true). | |
| 381 | get_guards(b(select([b(select_when(Guard, TBody),subst,_Info1)]),subst,Info2), _, [],Guard, TBody, Info2). | |
| 382 | % TO DO: for ANY try and extract propositional parts, e.g., for ANY pp WHERE pp:1..xx & z=1/yy THEN … | |
| 383 | get_guards(b(any(TIds,Guard,TBody),subst,Info),_, TIds,Guard,TBody,Info). | |
| 384 | get_guards(b(operation_call(Operation,[],Parameters),subst,Info),_, InnerParas,Guard, TBody, Info) :- | |
| 385 | Parameters=[], % TO DO: improve, will require substituting Parameters inside OpRealBody | |
| 386 | bmachine_is_precompiled, | |
| 387 | def_get_texpr_id(Operation,op(OpName)), | |
| 388 | b_get_machine_operation(OpName,[],RealParameters,OpRealBody,_OType,_OpPos), RealParameters=[], | |
| 389 | get_guards(OpRealBody, inner, InnerParas, Guard, TBody, _ ). | |
| 390 | ||
| 391 | construct_select([],Guard,TBody, Infos, Res) :- !, | |
| 392 | Res = b(select([b(select_when(Guard, TBody),subst,Infos)]),subst,Infos). | |
| 393 | construct_select(TIds,Guard,TBody,Infos, b(any(TIds,Guard,TBody),subst,Infos)). | |
| 394 | ||
| 395 | ||
| 396 | get_parameter_independent_guards(Guard,Parameters,Indep,Dep) :- | |
| 397 | conjunction_to_list(Guard,Gs), | |
| 398 | l_get_parameter_independent_guards(Gs,Parameters,at_front,Indep,Dep). | |
| 399 | ||
| 400 | :- use_module(bsyntaxtree,[always_well_defined/1]). | |
| 401 | l_get_parameter_independent_guards([],_,_,[],[]). | |
| 402 | l_get_parameter_independent_guards([G|Gs],Parameters,AtFront,Indep,Dep) :- | |
| 403 | find_identifier_uses(G,[],Ids), | |
| 404 | ( ord_disjoint(Ids,Parameters), | |
| 405 | (AtFront=at_front -> true ; always_well_defined(G)) | |
| 406 | -> Indep=[G|I1], Dep=D1, AtFront1=AtFront | |
| 407 | ; Indep=I1, Dep=[G|D1], | |
| 408 | AtFront1=not_at_front % we have skipped one guard; the next guard is not guaranteed to be at the front (relevant for well-definedness) | |
| 409 | ), | |
| 410 | l_get_parameter_independent_guards(Gs,Parameters,AtFront1,I1,D1). | |
| 411 | ||
| 412 | % for synthesis of sequential programs | |
| 413 | % not yet used | |
| 414 | /* | |
| 415 | % find events which have common guards | |
| 416 | get_common_guards(Ev1,Ev2,Common,Rest1,Rest2) :- | |
| 417 | get_unsimplified_operation_guard(Ev1,G1), conjunction_to_list(G1,GL1), | |
| 418 | get_unsimplified_operation_guard(Ev2,G2), Ev1 @< Ev2, conjunction_to_list(G2,GL2), | |
| 419 | find_common(GL1,GL2,Common,Rest1,Rest2), | |
| 420 | format('~nCommon guard for ~w <-> ~w~n Common: ',[Ev1,Ev2]), translate:l_print_bexpr_or_subst(Common),nl, | |
| 421 | format(' Rest1: ',[]),translate:l_print_bexpr_or_subst(Rest1),nl, | |
| 422 | format(' Rest2: ',[]),translate:l_print_bexpr_or_subst(Rest2),nl. | |
| 423 | ||
| 424 | % check if abrial merge rule 15.3 from Bee-Book for if/while is applicable: | |
| 425 | get_abrial_rule(Ev1,Ev2,Common,Rest1) :- | |
| 426 | get_common_guards(Ev1,Ev2,Common,Rest1,Rest2), | |
| 427 | conjunct_predicates(Rest1,R1), | |
| 428 | conjunct_predicates(Rest2,R2), | |
| 429 | is_negated_predicate(R1,R2), | |
| 430 | format('*** Can be merged ~w <-> ~w !~n~n',[Ev1,Ev2]). | |
| 431 | ||
| 432 | find_common([],GL2,[],[],GL2). | |
| 433 | find_common([G1|T1],GL2,[G1|TCommon],Rest1,Rest2) :- | |
| 434 | select(G2,GL2,T2), % TODO: check WD | |
| 435 | same_predicate(G1,G2),!, % we could also use norm_expr | |
| 436 | find_common(T1,T2,TCommon,Rest1,Rest2). | |
| 437 | find_common([G1|T1],GL2,TCommon,[G1|Rest1],Rest2) :- | |
| 438 | find_common(T1,GL2,TCommon,Rest1,Rest2). | |
| 439 | ||
| 440 | same_predicate(G1,G2) :- bsyntaxtree:same_texpr(G1,G2). | |
| 441 | same_predicate(G1,G2) :- b_interpreter_check:norm_pred_check(G1,N1), b_interpreter_check:norm_pred_check(G2,N2), N2=N1. | |
| 442 | ||
| 443 | is_negated_predicate(G1,G2) :- bsyntaxtree:is_negation_of(G1,G2). | |
| 444 | */ | |
| 445 |