| 1 | % (c) 2014-2015 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(before_after_predicates, [tcltk_before_after_predicate_for_operation/2, | |
| 6 | before_after_predicate_for_operation/2, | |
| 7 | before_after_predicate_with_equalities/3, | |
| 8 | before_after_predicate_list_conjunct_with_equalities/3, | |
| 9 | before_after_predicate_list_disjunct_with_equalities/3, | |
| 10 | list_renamings_to_primed_vars/2]). | |
| 11 | ||
| 12 | :- use_module(library(lists)). | |
| 13 | ||
| 14 | :- use_module(bsyntaxtree, [get_texpr_expr/2, | |
| 15 | get_texpr_id/2, | |
| 16 | is_truth/1, | |
| 17 | safe_create_texpr/3, | |
| 18 | get_texpr_type/2, | |
| 19 | conjunct_predicates/2, | |
| 20 | conjunction_to_list/2, | |
| 21 | create_implication/3, | |
| 22 | create_couple/3, | |
| 23 | disjunct_predicates/2, | |
| 24 | find_typed_identifier_uses/2, | |
| 25 | remove_all_infos/2, | |
| 26 | rename_bt/3, | |
| 27 | create_exists/3, | |
| 28 | create_negation/2]). | |
| 29 | :- use_module(error_manager, [add_error_fail/3]). | |
| 30 | :- use_module(bmachine_eventb, [prime_variable/2, | |
| 31 | prime_variables/2, | |
| 32 | is_primed_id/1]). | |
| 33 | :- use_module(bmachine,[b_get_machine_operation/4, | |
| 34 | b_get_machine_variables/1, | |
| 35 | b_get_machine_constants/1]). | |
| 36 | %:- use_module(specfile,[animation_minor_mode/1]). | |
| 37 | :- use_module(translate,[translate_bexpression/2]). | |
| 38 | ||
| 39 | :- use_module(module_information,[module_info/2]). | |
| 40 | :- module_info(group,misc). | |
| 41 | :- module_info(description,'This module computes before-after-predicates of B and Event-B actions.'). | |
| 42 | ||
| 43 | tcltk_before_after_predicate_for_operation(OpName,list(Res)) :- | |
| 44 | before_after_predicate_for_operation(OpName,BAPredicate), | |
| 45 | %translate:print_bexpr(BAPredicate),nl, | |
| 46 | conjunction_to_list(BAPredicate,LP), | |
| 47 | maplist(translate:translate_bexpression,LP,Res). | |
| 48 | ||
| 49 | before_after_predicate_for_operation(OpName,BAPredicate) :- | |
| 50 | b_get_machine_operation(OpName,_Results,_Parameters,OpBody), | |
| 51 | %print(op(OpName)),nl, | |
| 52 | b_get_machine_variables(Variables), | |
| 53 | b_get_machine_constants(Constants), | |
| 54 | append(Variables,Constants,VarsAndConsts), | |
| 55 | before_after_predicate_with_equalities(OpBody,VarsAndConsts,BAPredicate). | |
| 56 | ||
| 57 | :- mode before_after_predicate_with_equalities(+Action,+AllIdentifiers,-Predicate). | |
| 58 | % these add missing y' = y equalities for unchanged variables | |
| 59 | before_after_predicate_with_equalities(Action,AllIdentifiers,Predicate) :- | |
| 60 | before_after_predicate_list_conjunct_with_equalities([Action],AllIdentifiers,Predicate). | |
| 61 | before_after_predicate_list_conjunct_with_equalities(Actions,AllIdentifiers,BAPredicateWithEq) :- | |
| 62 | maplist(before_after_predicate_no_equalities_tl(top_level),Actions,AllPredicates), | |
| 63 | conjunct_predicates(AllPredicates,BAPredicate), | |
| 64 | add_missing_equalities(AllIdentifiers,BAPredicate,BAPredicateWithEq). | |
| 65 | before_after_predicate_list_disjunct_with_equalities(Actions,AllIdentifiers,BAPredicate) :- | |
| 66 | maplist(before_after_predicate_no_equalities_tl(top_level),Actions,AllPredicates), | |
| 67 | maplist(add_missing_equalities(AllIdentifiers),AllPredicates,BAPredicates), | |
| 68 | disjunct_predicates(BAPredicates,BAPredicate). | |
| 69 | ||
| 70 | % does not add missing y' = y equalities for unchanged variables | |
| 71 | % top-level version: has a special rule for PRE | |
| 72 | before_after_predicate_no_equalities_tl(TopLevel,Action,Predicate) :- | |
| 73 | get_texpr_expr(Action,Expr), | |
| 74 | before_after_predicate_no_equalities_top_level_aux(Expr,Predicate,TopLevel). | |
| 75 | ||
| 76 | :- use_module(preferences,[get_preference/2]). | |
| 77 | before_after_predicate_no_equalities_top_level_aux(precondition(Pre,Body),Predicate,top_level) :- | |
| 78 | get_preference(treat_outermost_pre_as_select,true), | |
| 79 | !, | |
| 80 | before_after_predicate_no_equalities(Body,BABody,_), | |
| 81 | conjunct_predicates([Pre,BABody],Predicate). % May sometimes have to be an implication (depending on how BA-predicate is used) ! | |
| 82 | before_after_predicate_no_equalities_top_level_aux(Expr,Pred,_) :- | |
| 83 | before_after_predicate_no_equalities_aux(Expr,Pred,_). | |
| 84 | ||
| 85 | % does not add missing y' = y equalities for unchanged variables | |
| 86 | before_after_predicate_no_equalities(Action,Predicate,ChangedIDs) :- | |
| 87 | get_texpr_expr(Action,Expr), | |
| 88 | before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs). | |
| 89 | ||
| 90 | get_changed_id(b(function(FUN,_),_,_),ID) :- !, get_changed_id(FUN,ID). | |
| 91 | get_changed_id(ID,ID). | |
| 92 | ||
| 93 | before_after_predicate_no_equalities_aux(assign_single_id(Id,Pred),Predicate,ChangedIDs) :- !, | |
| 94 | before_after_predicate_no_equalities_aux(assign([Id],[Pred]),Predicate,ChangedIDs). | |
| 95 | before_after_predicate_no_equalities_aux(assign(Ids,Preds),Predicate,ChangedIds) :- !, | |
| 96 | maplist(get_changed_id,Ids,ChangedIds), | |
| 97 | maplist(ba_predicate_equal,Ids,Preds,Predicates), | |
| 98 | conjunct_predicates(Predicates,Predicate). | |
| 99 | before_after_predicate_no_equalities_aux(becomes_element_of(Ids,Set),Predicate,Ids) :- !, | |
| 100 | maplist(ba_predicate_member(Set),Ids,Predicates), | |
| 101 | conjunct_predicates(Predicates,Predicate). % should we generate Set /= {} => Predicate | |
| 102 | before_after_predicate_no_equalities_aux(becomes_such(Ids,Pred),Predicate,Ids) :- !, | |
| 103 | ba_predicate_becomes_such(Ids,Pred,Predicate). | |
| 104 | before_after_predicate_no_equalities_aux(choice(Choices),Predicate,ChangedIDs) :- !, | |
| 105 | maplist(before_after_predicate_no_equalities,Choices,BAChoices,Changes), | |
| 106 | append(Changes,ChangedIDs), | |
| 107 | maplist(add_missing_equalities(ChangedIDs),BAChoices,BAChoicesWithEqualities), | |
| 108 | disjunct_predicates(BAChoicesWithEqualities,Predicate). | |
| 109 | before_after_predicate_no_equalities_aux(precondition(Pre,Body),Predicate,ChangedIDs) :- !, | |
| 110 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 111 | create_implication(Pre,BABody,Predicate). | |
| 112 | before_after_predicate_no_equalities_aux(assertion(Pre,Body),Predicate,ChangedIDs) :- | |
| 113 | !, | |
| 114 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 115 | create_implication(Pre,BABody,Predicate1), | |
| 116 | create_negation(Pre,NotPre), | |
| 117 | add_missing_equalities(ChangedIDs,b(truth,pred,[]),NotPrePredicate), | |
| 118 | create_implication(NotPre,NotPrePredicate,Predicate2), | |
| 119 | conjunct_predicates([Predicate1,Predicate2],Predicate). | |
| 120 | before_after_predicate_no_equalities_aux(select_when(Pre,Body),Predicate,ChangedIDs) :- !, | |
| 121 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 122 | conjunct_predicates([Pre,BABody],Predicate). | |
| 123 | before_after_predicate_no_equalities_aux(select(Whens),Predicate,ChangedIDs) :- !, | |
| 124 | maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes), | |
| 125 | append(Changes,ChangedIDs), | |
| 126 | maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities), | |
| 127 | disjunct_predicates(WhensPredicatesWithEqualities,Predicate). | |
| 128 | before_after_predicate_no_equalities_aux(select(Whens,Else),Predicate,ChangedIDs) :- !, | |
| 129 | maplist(before_after_predicate_no_equalities,Whens,WhensPredicates,Changes), | |
| 130 | maplist(add_missing_equalities(ChangedIDs),WhensPredicates,WhensPredicatesWithEqualities), | |
| 131 | maplist(get_select_conditions,Whens,SelectConditions), | |
| 132 | disjunct_predicates(SelectConditions,ElseTemp), | |
| 133 | create_negation(ElseTemp,ElseLHS), | |
| 134 | before_after_predicate_no_equalities(Else,ElseRHS,ElseChangedIDs), | |
| 135 | append([ElseChangedIDs|Changes],ChangedIDs), | |
| 136 | conjunct_predicates([ElseLHS,ElseRHS],ElsePred), | |
| 137 | add_missing_equalities(ChangedIDs,ElsePred,ElsePredWithEqualities), | |
| 138 | disjunct_predicates([ElsePredWithEqualities|WhensPredicatesWithEqualities],Predicate). | |
| 139 | % TODO: case, handle while | |
| 140 | before_after_predicate_no_equalities_aux(sequence(ListOfSteps),Predicate,ChangedIDs) :- !, | |
| 141 | ba_predicate_sequence(ListOfSteps,Predicate,ChangedIDs). | |
| 142 | before_after_predicate_no_equalities_aux(if(IfList),Predicate,ChangedIDs) :- !, | |
| 143 | ba_predicate_if(IfList,Predicate,ChangedIDs). | |
| 144 | before_after_predicate_no_equalities_aux(let(P,D,B),Predicate,ChangedIDs) :- !, | |
| 145 | before_after_predicate_no_equalities_aux(any(P,D,B),Predicate,ChangedIDs). | |
| 146 | before_after_predicate_no_equalities_aux(any(Parameters,PreCond,Body),Predicate,ChangedIDs) :- !, | |
| 147 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 148 | conjunct_predicates([PreCond,BABody],Inner), | |
| 149 | create_exists(Parameters,Inner,Predicate). | |
| 150 | before_after_predicate_no_equalities_aux(parallel(P),Predicate,ChangedIDs) :- !, | |
| 151 | maplist(before_after_predicate_no_equalities,P,Preds,Changes), | |
| 152 | append(Changes,ChangedIDs), | |
| 153 | conjunct_predicates(Preds,Predicate). | |
| 154 | before_after_predicate_no_equalities_aux(skip,Predicate,[]) :- !, | |
| 155 | Predicate = b(truth,pred,[]). | |
| 156 | before_after_predicate_no_equalities_aux(var(Parameters,Body),Predicate,ChangedIDs) :- !, | |
| 157 | before_after_predicate_no_equalities(Body,BABody,ChangedIDs), | |
| 158 | create_exists(Parameters,BABody,Predicate). | |
| 159 | before_after_predicate_no_equalities_aux(rlevent(_Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents),Predicate,ChangedIDs) :- !, | |
| 160 | maplist(before_after_predicate_no_equalities,Actions,BAActions,Changes), | |
| 161 | append(Changes,ChangedIDs), | |
| 162 | conjunct_predicates([Guards|BAActions],Predicate). % should probably be an implication? see precondition. | |
| 163 | before_after_predicate_no_equalities_aux(operation_call(OpId,[],[]),Predicate,ChangedIDs) :- !, | |
| 164 | get_texpr_id(OpId,op(OpName)), | |
| 165 | b_get_machine_operation(OpName,[],[],OpBody), | |
| 166 | before_after_predicate_no_equalities(OpBody,Predicate,ChangedIDs). | |
| 167 | before_after_predicate_no_equalities_aux(Expr,Predicate,ChangedIDs) :- | |
| 168 | add_error_fail(before_after_predicate,'before-after-predicate implementation missing: ',[Expr,Predicate,ChangedIDs]). | |
| 169 | ||
| 170 | get_select_conditions(b(select_when(Condition,_),_,_),Condition). | |
| 171 | ||
| 172 | ba_predicate_equal(LHS,RHS,Res) :- | |
| 173 | % LHS := RHS trace, | |
| 174 | get_override(LHS,RHS,TPred), !, | |
| 175 | %nl,translate:print_bexpr(TPred),nl, | |
| 176 | Res=TPred. | |
| 177 | ||
| 178 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
| 179 | % get override Term for f(X)(Y)... := RHS | |
| 180 | get_override(b(function(FUN,ARG),Type,_Info),ExprSoFar,Res) :- !, % FUN(ARG) := RHS | |
| 181 | %print(fun(FUN)),nl, translate:print_bexpr(ExprSoFar),nl, | |
| 182 | create_couple(ARG,ExprSoFar,Update), % ARG|-> ExprSoFar | |
| 183 | safe_create_texpr(set_extension([Update]),Type,UpdateSET), % {ARG|->ExprSoFar} | |
| 184 | construct_override(FUN,UpdateSET,Override), % FUN <+ {ARG |-> {...}} | |
| 185 | get_override(FUN,Override,Res). % Pass Override as new RHS in case FUN itself is a function application | |
| 186 | get_override(FUNID,OverrideExpr,TPred) :- | |
| 187 | get_texpr_id(FUNID,_ID), %print(base(ID)),nl, | |
| 188 | prime_variable(FUNID,FUNPrimeId), | |
| 189 | safe_create_texpr(equal(FUNPrimeId,OverrideExpr),pred,TPred). % FUN' = FUN <+ {ARG |-> RHS} | |
| 190 | get_override(FUNID,OverrideExpr,TPred) :- | |
| 191 | add_internal_error('Cannot compute override: ',get_override(FUNID,OverrideExpr,TPred)),fail. | |
| 192 | ||
| 193 | construct_override(FunID,Update,Override) :- | |
| 194 | get_texpr_type(Update,Type), | |
| 195 | Override = b(overwrite(FunID,Update),Type,[]). | |
| 196 | ||
| 197 | ba_predicate_member(Set,Id,TPred) :- | |
| 198 | % prime identifiers on the lhs | |
| 199 | prime_variable(Id,PrimedId), | |
| 200 | safe_create_texpr(member(PrimedId,Set),pred,TPred). | |
| 201 | ||
| 202 | ba_predicate_becomes_such(Ids,Pred,Predicate) :- | |
| 203 | list_renamings_to_primed_vars(Ids,RenamingList), | |
| 204 | rename_bt(Pred,RenamingList,Predicate). | |
| 205 | ||
| 206 | list_renamings_to_primed_vars([],[]). | |
| 207 | list_renamings_to_primed_vars([Var|Vars],[rename(VarId,PrimedId)|T]) :- | |
| 208 | get_texpr_id(Var,VarId), | |
| 209 | atom_concat(VarId,'\'',PrimedId), | |
| 210 | list_renamings_to_primed_vars(Vars,T). | |
| 211 | ||
| 212 | add_missing_equalities(AllVariables,PredWithoutEqualities,PredWithEqualities) :- | |
| 213 | find_typed_identifier_uses(PredWithoutEqualities,UsedIdentifiers), | |
| 214 | exclude(primed_var_is_used(UsedIdentifiers),AllVariables,VariablesNotOccuringPrimed), | |
| 215 | maplist(ba_predicate_equal,VariablesNotOccuringPrimed,VariablesNotOccuringPrimed,EqualityPredicates), | |
| 216 | conjunct_predicates([PredWithoutEqualities|EqualityPredicates],PredWithEqualities). | |
| 217 | ||
| 218 | primed_var_is_used(UsedIdentifiers,Identifier) :- | |
| 219 | prime_variable(Identifier,PrimedIdentifier), | |
| 220 | remove_all_infos(PrimedIdentifier,PrimedIdentifierWithoutInfos), | |
| 221 | member(PrimedIdentifierWithoutInfos,UsedIdentifiers). | |
| 222 | ||
| 223 | add_else_if_missing([],[DefaultElse]) :- | |
| 224 | safe_create_texpr(if_elsif(b(truth,pred,[]),b(skip,subst,[])),subst,DefaultElse). | |
| 225 | add_else_if_missing([If|Ifs],[If|Ifs]) :- | |
| 226 | get_texpr_expr(If,if_elsif(Test,_)), | |
| 227 | is_truth(Test), !. | |
| 228 | add_else_if_missing([If|Ifs],[If|MoreIfs]) :- | |
| 229 | add_else_if_missing(Ifs,MoreIfs). | |
| 230 | ||
| 231 | ba_predicate_if(IF,BA,AllChangedIDs) :- | |
| 232 | add_else_if_missing(IF,IFWithElse), | |
| 233 | maplist(ba_predicate_if_aux,IFWithElse,BAPreds,ChangedIDs), | |
| 234 | append(ChangedIDs,AllChangedIDs), | |
| 235 | ba_predicate_if(IFWithElse,BAPreds,AllChangedIDs,BA). | |
| 236 | ||
| 237 | ba_predicate_if([IF|IFs],[BAPred|BAPreds],IDs,BA) :- | |
| 238 | get_texpr_expr(IF,if_elsif(Test,_)), | |
| 239 | % if-part | |
| 240 | add_missing_equalities(IDs,BAPred,InnerBAPredIf), | |
| 241 | (is_truth(Test) | |
| 242 | -> InnerBAPredIf = BAPredIf | |
| 243 | ; safe_create_texpr(implication(Test,InnerBAPredIf),pred,BAPredIf)), | |
| 244 | % if there are further else/elseif parts, create pos | |
| 245 | (ba_predicate_if(IFs,BAPreds,IDs,ElsePred) | |
| 246 | -> create_negation(Test,NegTest), | |
| 247 | safe_create_texpr(implication(NegTest,ElsePred),pred,BAPredElse), | |
| 248 | conjunct_predicates([BAPredIf,BAPredElse],BA) | |
| 249 | ; BA = BAPredIf). | |
| 250 | ||
| 251 | ba_predicate_if_aux(IF,BAPred,ChangedIDs) :- | |
| 252 | get_texpr_expr(IF,if_elsif(_,Body)), | |
| 253 | before_after_predicate_no_equalities(Body,BAPred,ChangedIDs). | |
| 254 | ||
| 255 | ba_predicate_sequence([Last],Predicate,ChangedIDs) :- !, | |
| 256 | before_after_predicate_no_equalities(Last,Predicate,ChangedIDs). | |
| 257 | ba_predicate_sequence([First|SomeMore],Predicate,ChangedIDs) :- | |
| 258 | before_after_predicate_no_equalities(First,FirstPred,ChangesFirst), | |
| 259 | find_typed_identifier_uses(FirstPred,Identifiers), | |
| 260 | include(is_primed,Identifiers,PrimedIdentifiers), | |
| 261 | list_renamings_to_primed_vars(PrimedIdentifiers,RenamingToTwicePrimedIDs), | |
| 262 | rename_bt(FirstPred,RenamingToTwicePrimedIDs,FirstPredAfterReplacement), | |
| 263 | ||
| 264 | ba_predicate_sequence(SomeMore,SecondPred,FurtherChanges), | |
| 265 | list_renamings_remove_prime(PrimedIdentifiers,RenamingToNotPrimed), | |
| 266 | rename_bt(SecondPred,RenamingToNotPrimed,SecondPredAfterReplacement), | |
| 267 | ||
| 268 | conjunct_predicates([FirstPredAfterReplacement,SecondPredAfterReplacement],FullPred), | |
| 269 | ||
| 270 | prime_variables(PrimedIdentifiers,TwicePrimedIdentifiers), | |
| 271 | create_exists(TwicePrimedIdentifiers,FullPred,Predicate), | |
| 272 | append(ChangesFirst,FurtherChanges,ChangedIDs). | |
| 273 | ||
| 274 | is_primed(TExpr) :- | |
| 275 | get_texpr_id(TExpr,ID), | |
| 276 | is_primed_id(ID). | |
| 277 | ||
| 278 | list_renamings_remove_prime([],[]). | |
| 279 | list_renamings_remove_prime([Var|Vars],[rename(VarId,NonPrimedID)|T]) :- | |
| 280 | get_texpr_id(Var,VarId), | |
| 281 | atom_concat(NonPrimedID,'\'',VarId), | |
| 282 | list_renamings_remove_prime(Vars,T). |