| 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(cbc_refinement_checks, [cbc_refinement_check/2]). |
| 6 | | |
| 7 | | :- use_module(probsrc(module_information),[module_info/2]). |
| 8 | | :- module_info(group,cbc). |
| 9 | | :- module_info(description,'This module provides constraint-based checking of B and Event-B refinements.'). |
| 10 | | |
| 11 | | :- use_module(library(lists)). |
| 12 | | :- use_module(library(sets), [subtract/3]). |
| 13 | | |
| 14 | | :- use_module(probsrc(solver_interface), [solve_predicate/3]). |
| 15 | | |
| 16 | | :- use_module(probsrc(specfile), [animation_minor_mode/1]). |
| 17 | | :- use_module(probsrc(bmachine), [full_b_machine/1, |
| 18 | | b_get_refined_machine/1, |
| 19 | | b_get_machine_operation/6, |
| 20 | | b_get_invariant_from_machine/1, |
| 21 | | b_get_linking_invariant_from_machine/1, |
| 22 | | b_get_properties_from_machine/1, |
| 23 | | b_get_machine_variables/1, |
| 24 | | b_get_machine_constants/1, |
| 25 | | b_machine_name/1]). |
| 26 | | |
| 27 | | :- use_module(probsrc(translate), [nested_print_bexpr/1]). |
| 28 | | :- use_module(probsrc(debug), [formatsilent/2, debug_mode/1]). |
| 29 | | :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2,get_texpr_info/2, |
| 30 | | get_texpr_id/2, |
| 31 | | get_rodin_name/2, |
| 32 | | conjunct_predicates/2, |
| 33 | | conjunction_to_list/2, |
| 34 | | create_texpr/4, safe_create_texpr/3, |
| 35 | | rename_bt/3]). |
| 36 | | :- use_module(probsrc(b_interpreter_components), [construct_optimized_exists/3]). |
| 37 | | :- use_module(probsrc(bmachine_structure), [get_section/3]). |
| 38 | | :- use_module(probsrc(btypechecker), [prime_identifiers/2]). |
| 39 | | :- use_module(probsrc(bsyntaxtree), [create_negation/2]). |
| 40 | | :- use_module(extrasrc(weakest_preconditions), [weakest_precondition/3, |
| 41 | | set_reference_machine/1, |
| 42 | | delete_reference_machine/0]). |
| 43 | | :- use_module(extrasrc(before_after_predicates), [before_after_predicate_with_equalities/3, |
| 44 | | before_after_predicate_list_conjunct_with_equalities/3, |
| 45 | | list_renamings_to_primed_vars/2]). |
| 46 | | :- use_module(probsrc(preferences),[get_preference/2]). |
| 47 | | :- use_module(probsrc(tools_strings), [ajoin/2]). |
| 48 | | |
| 49 | | cbc_refinement_check(List,ViolationFound) :- |
| 50 | | (animation_minor_mode(eventb) |
| 51 | | -> eventb_refinement_check(List,ViolationFound) |
| 52 | ? | ; classical_refinement_check(List,ViolationFound)). |
| 53 | | |
| 54 | | % ------------------------------------------- |
| 55 | | % eventb po generation |
| 56 | | % ------------------------------------------- |
| 57 | | |
| 58 | | eventb_refinement_check(ResultList,ViolationFound) :- |
| 59 | | % fetch Axioms and Invariant/properties first |
| 60 | | full_b_machine(Machine), |
| 61 | | (get_section(axioms,Machine,Axioms) -> true ; Axioms = []), |
| 62 | | b_get_invariant_from_machine(Invariant), |
| 63 | | b_get_properties_from_machine(Properties), |
| 64 | | % evt/p/WFIS |
| 65 | | witness_feasibility(Axioms,Invariant,Properties,ListWF,V1), |
| 66 | | % evt/grd/GRD proof obligations |
| 67 | | guard_strengthening(Axioms,Invariant,Properties,ListGS,V2), |
| 68 | | % evt/act/SIM |
| 69 | | action_simulation(Axioms,Invariant,Properties,ListAS,V3), |
| 70 | | append([ListWF,['\n'],ListGS,['\n'],ListAS],ResultList), |
| 71 | | merge_violation_found([V1,V2,V3],ViolationFound). |
| 72 | | |
| 73 | | witness_feasibility(Axioms,Invariant,Properties,['Witness Feasibility:'|FlatResults],ViolationFound) :- |
| 74 | | % action simulation: |
| 75 | | % A & I & J & H & W & Tau => Q_i |
| 76 | | % find all candidates for evt/act/SIM proof obligations |
| 77 | | findall(RLEVENT, |
| 78 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_OpPos), |
| 79 | | get_texpr_expr(Body,RLEVENT)), |
| 80 | | ListOfOperations), |
| 81 | | maplist(witness_feasibility_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
| 82 | | append(Results,FlatResults), |
| 83 | | merge_violation_found(SubViolationFound,ViolationFound). |
| 84 | | |
| 85 | | witness_feasibility_aux(Axioms,Invariant,Properties, |
| 86 | | rlevent(Name,_Section,_Stat,Parameters,Guards,_Thm,_Actions,_VWit,PWit,_Unmod,AbsEvents), |
| 87 | | ResultsParameters,ViolationFound) :- |
| 88 | | % feasibility for parameters - the abstract events have a parameter |
| 89 | | % that is not a parameter of the concrete events |
| 90 | | all_abstract_parameters(AbsEvents,AllAbsParameters), |
| 91 | | subtract(AllAbsParameters,Parameters,ParametersForWfisPos), |
| 92 | | |
| 93 | | conjunct_predicates([Invariant,Properties,Guards|Axioms],LHSPred), |
| 94 | | |
| 95 | | % map over all abstract events |
| 96 | | maplist(witness_feasibility_parameters(Name,LHSPred,PWit),ParametersForWfisPos,ResultsParameters,SubViolationFound), |
| 97 | | merge_violation_found(SubViolationFound,ViolationFound). |
| 98 | | |
| 99 | | witness_feasibility_parameters(Name,LHSPred,PWit,Parameter,Result,ViolationFound) :- |
| 100 | | % find matching witness - same identifier |
| 101 | | get_texpr_id(Parameter,Identifier), |
| 102 | | member(Witness,PWit), get_texpr_expr(Witness,witness(WitnessIdentifier,Pred)), |
| 103 | | get_texpr_id(WitnessIdentifier,Identifier), !, |
| 104 | | |
| 105 | | % set up PO: A & I & J & H => exists p : W_p |
| 106 | | construct_optimized_exists([Parameter],Pred,ExistsPred), |
| 107 | | create_negation(ExistsPred,NegatedExistsPred), |
| 108 | | conjunct_predicates([LHSPred,NegatedExistsPred],CounterExamplePred), |
| 109 | | |
| 110 | | solve_predicate(CounterExamplePred,State,Res), |
| 111 | | assign_violation_found(Res,ViolationFound), |
| 112 | | |
| 113 | | % result string |
| 114 | | ajoin([Name,'/',Identifier,'/WFIS: ','Counter-Example found: ', Res],Result), |
| 115 | | % print |
| 116 | | formatsilent('~w~n',[Result]), |
| 117 | | (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl). |
| 118 | | |
| 119 | | action_simulation(Axioms,Invariant,Properties,['Action Simulation:'|ResultsFlat],ViolationFound) :- |
| 120 | | % action simulation: |
| 121 | | % A & I & J & H & W & Tau => Q_i |
| 122 | | % find all candidates for evt/act/SIM proof obligations |
| 123 | | findall(RLEVENT, |
| 124 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_), |
| 125 | | get_texpr_expr(Body,RLEVENT)), |
| 126 | | ListOfOperations), |
| 127 | | maplist(action_simulation(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
| 128 | | merge_violation_found(SubViolationFound,ViolationFound), |
| 129 | | append(Results,ResultsFlat). |
| 130 | | |
| 131 | | action_simulation(Axioms,Invariant,Properties, |
| 132 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents), |
| 133 | | ResultsFlat,ViolationFound) :- |
| 134 | | % concrete before-after-predicate |
| 135 | | b_get_machine_variables(Vars), |
| 136 | | b_get_machine_constants(Consts), |
| 137 | | append(Vars,Consts,Both), |
| 138 | | before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau), |
| 139 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
| 140 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
| 141 | | append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds],LHSPreds), |
| 142 | | conjunct_predicates(LHSPreds,LHS), |
| 143 | | |
| 144 | | % map over all abstract events |
| 145 | | maplist(action_simulation2(Name,LHS),AbsEvents,Results,SubViolationFound), |
| 146 | | merge_violation_found(SubViolationFound,ViolationFound), |
| 147 | | append(Results,ResultsFlat). |
| 148 | | |
| 149 | | action_simulation2(Name,LHS,AbsEvent,Result,ViolationFound) :- |
| 150 | | get_texpr_expr(AbsEvent,rlevent(_AbsName,_Section,_Stat,_AbsParameters,_Guards,_Thm,Actions,_VWit,_PWit,_Unmod,_AbsEvents)), |
| 151 | | % map over all abstract actions |
| 152 | | maplist(action_simulation3(Name,LHS),Actions,Result,SubViolationFound), |
| 153 | | merge_violation_found(SubViolationFound,ViolationFound). |
| 154 | | |
| 155 | | action_simulation3(Name,LHS,Action,Result,ViolationFound) :- |
| 156 | ? | modifies_concrete_var(Action), !, |
| 157 | | get_rodin_name(Action,ActionName), |
| 158 | | |
| 159 | | % before after predicate of abstract action, negate, solve |
| 160 | | b_get_machine_variables(AllVars), |
| 161 | | exclude(is_concrete_var,AllVars,AbstractVars), |
| 162 | | before_after_predicate_with_equalities(Action,AbstractVars,BAPred), |
| 163 | | create_negation(BAPred,NegatedBAPred), |
| 164 | | conjunct_predicates([NegatedBAPred,LHS],Pred), |
| 165 | | |
| 166 | | solve_predicate(Pred,State,Res), |
| 167 | | assign_violation_found(Res,ViolationFound), |
| 168 | | |
| 169 | | % result string |
| 170 | | ajoin([Name,'/',ActionName,'/SIM: ','Counter-Example found: ', Res],Result), |
| 171 | | % print |
| 172 | | formatsilent('~w~n',[Result]), |
| 173 | | (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl). |
| 174 | | |
| 175 | | % abstract action does not modify a concrete variable -> no PO |
| 176 | | action_simulation3(_Name,_LHS,_Action,[],false). |
| 177 | | |
| 178 | | guard_strengthening(Axioms,Invariant,Properties,['Guard Strengthening:'|ResultsFlat],ViolationFound) :- |
| 179 | | % guard strengthening: |
| 180 | | % A & I & J & H & W => G_i |
| 181 | | % guard strengthening (merge): |
| 182 | | % A & I & J & H & W & Tau => G_1 or ... or G_n |
| 183 | | % find all candidates for evt/grd/GRD proof obligations |
| 184 | | findall(RLEVENT, |
| 185 | | (b_get_machine_operation(_Name,_R,_P,Body,_OType,_), |
| 186 | | get_texpr_expr(Body,RLEVENT)), |
| 187 | | ListOfOperations), |
| 188 | | maplist(guard_strengthening_aux(Axioms,Invariant,Properties),ListOfOperations,Results,SubViolationFound), |
| 189 | | append(Results,ResultsFlat), |
| 190 | | merge_violation_found(SubViolationFound,ViolationFound). |
| 191 | | |
| 192 | | % guard_strengthening: not a refinement |
| 193 | | guard_strengthening_aux(_Axioms,_Invariant,_Properties, |
| 194 | | rlevent(_Name,_Section,_Stat,_Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,[]), |
| 195 | | [],false) :- !. % nothing to check |
| 196 | | |
| 197 | | % guard_strengthening: refining only one event |
| 198 | | guard_strengthening_aux(Axioms,Invariant,Properties, |
| 199 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,_Actions,VWit,PWit,_Unmod,[AbsEvent]), |
| 200 | | Results,ViolationFound) :- !, |
| 201 | | get_texpr_expr(AbsEvent,ABSRLEVENT), |
| 202 | | ABSRLEVENT = rlevent(_AbsName,_Absection,_AbsStat,_AbsParameters,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsEvents), |
| 203 | | conjunction_to_list(AbsGrds,AbsGrdsList), |
| 204 | | % map over all abstract guards |
| 205 | | maplist(guard_strengthening_single_event(Name,Axioms,Invariant,Properties,VWit,PWit,Guards),AbsGrdsList,Results,SubViolationFound), |
| 206 | | merge_violation_found(SubViolationFound,ViolationFound). |
| 207 | | |
| 208 | | % guard_strengthening: refining multiple events |
| 209 | | guard_strengthening_aux(Axioms,Invariant,Properties, |
| 210 | | rlevent(Name,_Section,_Stat,_Parameters,Guards,_Thm,Actions,VWit,PWit,_Unmod,AbsEvents), |
| 211 | | [Result],ViolationFound) :- |
| 212 | | % concrete before-after-predicate |
| 213 | | b_get_machine_variables(Vars), |
| 214 | | b_get_machine_constants(Consts), |
| 215 | | append(Vars,Consts,Both), |
| 216 | | before_after_predicate_list_conjunct_with_equalities(Actions,Both,Tau), |
| 217 | | % collect all abstract guards G_i and negate |
| 218 | | findall(AbsGrds, |
| 219 | | (member(Evt,AbsEvents), |
| 220 | | get_texpr_expr(Evt,rlevent(_AbsName,_AbsSection,_AbsStat,_AbsParams,AbsGrds,_AbsThm,_AbsAct,_AbsVWit,_AbsPWit,_AbsUnmod,_AbsAbsEvents))), |
| 221 | | ListOfAbstractGuards), |
| 222 | | maplist(create_negation,ListOfAbstractGuards,NegatedAbstractGuards), |
| 223 | | |
| 224 | | % build up predicate A & I & J & H & W & Tau => G_1 or ... or G_n |
| 225 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
| 226 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
| 227 | | |
| 228 | | append([Axioms,[Invariant,Properties,Guards,Tau],VWitPreds,PWitPreds,NegatedAbstractGuards],LHSPred), |
| 229 | | conjunct_predicates(LHSPred,Pred), |
| 230 | | solve_predicate(Pred,State,Res), |
| 231 | | |
| 232 | | assign_violation_found(Res,ViolationFound), |
| 233 | | |
| 234 | | % result string and print |
| 235 | | ajoin([Name,'/MRG: ','Counter-Example found: ', Res],Result), |
| 236 | | formatsilent('~w~n',[Result]), |
| 237 | | (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl). |
| 238 | | |
| 239 | | guard_strengthening_single_event(OpName,_Axioms,_Invariant,_Properties,_VWit,_PWit,_Guards,AbsGrd,Result,false) :- |
| 240 | | get_rodin_name(AbsGrd,GuardName), |
| 241 | | formatsilent('~nChecking single event guard strengthening for: ~w of ~w~n',[GuardName,OpName]), |
| 242 | | b_machine_name(MainMachineName), % we assume that we prove the guard strengthening for the main machine ! |
| 243 | | bmachine:discharged_guard_strengthening(MainMachineName,AbstractEvent,GuardName,OpName), |
| 244 | | formatsilent('Guard ~w of ~w is already proven for event ~w:~w !~n',[GuardName,AbstractEvent,MainMachineName,OpName]), |
| 245 | | get_preference(use_po,true), |
| 246 | | !, |
| 247 | | ajoin([OpName,'/',GuardName,'/GRD: ','already proven'],Result). |
| 248 | | guard_strengthening_single_event(OpName,Axioms,Invariant,Properties,VWit,PWit,Guards,AbsGrd,Result,ViolationFound) :- |
| 249 | | get_rodin_name(AbsGrd,GuardName), |
| 250 | | % build up predicate and check |
| 251 | | maplist(extract_witness_predicate,VWit,VWitPreds), |
| 252 | | maplist(extract_witness_predicate,PWit,PWitPreds), |
| 253 | | create_negation(AbsGrd,NegAbsGrd), |
| 254 | | |
| 255 | | append([Axioms,[Invariant,Properties,Guards,NegAbsGrd],VWitPreds,PWitPreds],Predicates), |
| 256 | | conjunct_predicates(Predicates,Pred), |
| 257 | | |
| 258 | | solve_predicate(Pred,State,Res), |
| 259 | | assign_violation_found(Res,ViolationFound), |
| 260 | | |
| 261 | | % result string and print |
| 262 | | ajoin([OpName,'/',GuardName,'/GRD: ','Counter-Example found: ', Res],Result), |
| 263 | | formatsilent('~w~n',[Result]), |
| 264 | | (debug_mode(off) -> true ; nested_print_bexpr(Pred), write(State),nl). |
| 265 | | |
| 266 | | extract_witness_predicate(Witness,Pred) :- |
| 267 | | get_texpr_expr(Witness,witness(_Id,Pred)). |
| 268 | | |
| 269 | | modifies_concrete_var(Action) :- |
| 270 | | get_texpr_info(Action,Info), |
| 271 | ? | member(modifies(ListOfVars), Info), |
| 272 | ? | some(is_concrete_var,ListOfVars). |
| 273 | | |
| 274 | | is_concrete_var(b(identifier(Name),_,_)) :- !, |
| 275 | ? | is_concrete_var(Name). |
| 276 | | is_concrete_var(VarName) :- |
| 277 | | b_get_machine_variables(Variables), |
| 278 | | b_machine_name(TopLevelName), % can have prefix MAIN_MACHINE_FOR_ |
| 279 | ? | member(b(identifier(VarName),_Type,Infos),Variables), |
| 280 | ? | member(occurrences(Machines),Infos), |
| 281 | | member(TopLevelName,Machines). |
| 282 | | |
| 283 | | all_abstract_parameters([],[]). |
| 284 | | all_abstract_parameters([Event|FurtherEvents],ParametersOut) :- |
| 285 | | get_texpr_expr(Event,rlevent(_Name,_Section,_Stat,Parameters,_Guards,_Thm,_Actions,_VWit,_PWit,_Unmod,_AbsEvents)), |
| 286 | | all_abstract_parameters(FurtherEvents,FurtherParameters), append(Parameters,FurtherParameters,ParametersOut). |
| 287 | | |
| 288 | | % ------------------------------------------- |
| 289 | | % classical b po generation |
| 290 | | % ------------------------------------------- |
| 291 | | |
| 292 | | classical_refinement_check(ResultList,ViolationFound) :- |
| 293 | | % fetch Axioms and Invariant/properties first |
| 294 | | full_b_machine(Machine), |
| 295 | | b_get_refined_machine(AbsMachine) |
| 296 | | -> b_get_invariant_from_machine(Invariant), |
| 297 | | b_get_linking_invariant_from_machine(LinkingInvariant), |
| 298 | | % check initialisation po |
| 299 | ? | initialisation_pos(LinkingInvariant,Machine,AbsMachine,IniPos,V1), |
| 300 | | % check all operation pos |
| 301 | | get_all_operations_from_machine(Machine,ConcreteOperations), |
| 302 | | get_all_operations_from_machine(AbsMachine,AbstractOperations), |
| 303 | ? | operations_pos(ConcreteOperations,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,V2), |
| 304 | | append([[IniPos],['\n'],ListOpPos],ResultList), |
| 305 | | merge_violation_found([V1,V2],ViolationFound) |
| 306 | | ; ResultList = ['Not a Refinement Machine']. |
| 307 | | |
| 308 | | get_all_operations_from_machine(Machine,Operations) :- |
| 309 | | get_section(operation_bodies,Machine,Ops), |
| 310 | | findall(operation(Name,Results,Parameters,Body), |
| 311 | | (get_texpr_expr(Op,operation(TId,Results,Parameters,Body)), |
| 312 | | get_texpr_id(TId,op(Name)),member(Op,Ops)), |
| 313 | | Operations). |
| 314 | | |
| 315 | | initialisation_pos(LinkingInvariant,Machine,AbsMachine,Result,ViolationFound) :- |
| 316 | | % get the two initialisations |
| 317 | | get_section(initialisation,Machine,ConcreteInitialisation), |
| 318 | | get_section(initialisation,AbsMachine,AbstractInitialisation), |
| 319 | | |
| 320 | | % set up proof obligation [T1] not [T] not J (Schneider p.222) |
| 321 | | create_negation(LinkingInvariant,NegLinkingInvariant), |
| 322 | | |
| 323 | | set_reference_machine(AbsMachine), |
| 324 | ? | weakest_precondition(AbstractInitialisation,NegLinkingInvariant,TempPred), |
| 325 | | delete_reference_machine, |
| 326 | | |
| 327 | | create_negation(TempPred,NotTNotJ), |
| 328 | ? | weakest_precondition(ConcreteInitialisation,NotTNotJ,PO), |
| 329 | | create_negation(PO,CounterExPO), |
| 330 | | |
| 331 | | solve_predicate(CounterExPO,State,Res), |
| 332 | | assign_violation_found(Res,ViolationFound), |
| 333 | | |
| 334 | | % result string and print |
| 335 | | ajoin(['Initialisation [T1] not [T] not J: Counter-Example found: ', Res],Result), |
| 336 | | formatsilent('~w~n',[Result]), |
| 337 | | (debug_mode(off) -> true ; nested_print_bexpr(CounterExPO), write(State),nl). |
| 338 | | |
| 339 | | operations_pos([],_I,_LI,_AM,_A,[],false). |
| 340 | | operations_pos([operation(Name,Results,_Parameters,_Body)|FurtherOps],Invariant, |
| 341 | | LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound) :- |
| 342 | | % there might be no abstract operation with the same name (includes, etc.) |
| 343 | ? | \+ (member(operation(Name,_AbsResults,_AbsParameters,_AbsBody),AbstractOperations)), !, |
| 344 | | operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,Results,ViolationFound). |
| 345 | | operations_pos([operation(Name,Results,_Parameters,Body)|FurtherOps],Invariant, |
| 346 | | LinkingInvariant,AbsMachine,AbstractOperations,[PreRefPoResult,RefPoResult|ListOpPos],ViolationFound) :- |
| 347 | | % first find the matching abstract operation |
| 348 | ? | member(operation(Name,_AbsResults,_AbsParameters,AbsBody),AbstractOperations), |
| 349 | | |
| 350 | | % check if we have preconditions - otherwise we assume true |
| 351 | | (get_texpr_expr(Body,precondition(Precondition,RealBody)) -> true ; RealBody=Body, create_texpr(truth,pred,[],Precondition)), |
| 352 | | (get_texpr_expr(AbsBody,precondition(AbsPrecondition,AbsRealBody)) -> true ; AbsRealBody=AbsBody, create_texpr(truth,pred,[],AbsPrecondition)), |
| 353 | | |
| 354 | | % refinement po for the preconditions |
| 355 | | create_negation(AbsPrecondition,NegAbsPrecondition), |
| 356 | | conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegAbsPrecondition],PreRefPo), |
| 357 | | solve_predicate(PreRefPo,State,PreRefPoRes), |
| 358 | | |
| 359 | | % result string and print |
| 360 | | ajoin([Name, ' Precondition Refinement I & J & P => P1: Counter-Example found: ', PreRefPoRes],PreRefPoResult), |
| 361 | | formatsilent('~w~n',[PreRefPoResult]), |
| 362 | | (debug_mode(off) -> true ; nested_print_bexpr(PreRefPo), write(State),nl), |
| 363 | | |
| 364 | | % for the refinement of operations, we need to rename existing output variables (i.e. prime them) |
| 365 | | prime_identifiers(Results,PrimedResults), |
| 366 | | list_renamings_to_primed_vars(Results,Renamings), |
| 367 | | rename_bt(RealBody,Renamings,RealBodyWithPrimedVariables), |
| 368 | | create_equals(Results,PrimedResults,EqualResultsPred), |
| 369 | | |
| 370 | | % refinement po for the operation |
| 371 | | % I & J & P => [S1[out'/out]] not S not (J & out'=out) |
| 372 | | conjunct_predicates([LinkingInvariant|EqualResultsPred],RHS), |
| 373 | | create_negation(RHS,NegRHS), |
| 374 | | |
| 375 | | set_reference_machine(AbsMachine), |
| 376 | ? | weakest_precondition(AbsRealBody,NegRHS,RHS2), |
| 377 | | delete_reference_machine, |
| 378 | | |
| 379 | | create_negation(RHS2,NegRHS2), |
| 380 | ? | weakest_precondition(RealBodyWithPrimedVariables,NegRHS2,RHS3), |
| 381 | | create_negation(RHS3,NegRHS3), |
| 382 | | conjunct_predicates([Invariant,LinkingInvariant,Precondition,NegRHS3],RefPo), |
| 383 | | |
| 384 | | solve_predicate(RefPo,State2,RefPoRes), |
| 385 | | % result string and print |
| 386 | | ajoin([Name, ' Refinement I & J & P => S1 not S not J: Counter-Example found: ', RefPoRes],RefPoResult), |
| 387 | | formatsilent('~w~n',[RefPoResult]), |
| 388 | | (debug_mode(off) -> true ; nested_print_bexpr(RefPo), write(State2),nl), |
| 389 | | |
| 390 | ? | operations_pos(FurtherOps,Invariant,LinkingInvariant,AbsMachine,AbstractOperations,ListOpPos,SubViolationFound), |
| 391 | | assign_violation_found(RefPoRes,V1), |
| 392 | | assign_violation_found(PreRefPoRes,V2), |
| 393 | | merge_violation_found([V1,V2,SubViolationFound],ViolationFound). |
| 394 | | |
| 395 | | create_equals([],[],[]). |
| 396 | | create_equals([Id|Ids],[Expr|Exprs],[TPred|SubPreds]) :- |
| 397 | | safe_create_texpr(equal(Id,Expr),pred,TPred), |
| 398 | | create_equals(Ids,Exprs,SubPreds). |
| 399 | | |
| 400 | | merge_violation_found(L,true) :- |
| 401 | ? | some('=='(true),L), !. |
| 402 | | merge_violation_found(L,R) :- |
| 403 | | some('=='(time_out),L), !, R=time_out. |
| 404 | | merge_violation_found(_,false). |
| 405 | | |
| 406 | | assign_violation_found(solution(_),true) :- !. |
| 407 | | assign_violation_found(time_out,R) :- !, R= time_out. |
| 408 | | assign_violation_found(_,false). |