| 1 | % (c) 2009-2019 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_interpreter_eventb, | |
| 6 | [ b_event/6 | |
| 7 | , b_event_with_change_set/7 | |
| 8 | , b_event_constraints/7 | |
| 9 | ]). | |
| 10 | ||
| 11 | :- use_module(tools). | |
| 12 | :- use_module(bsyntaxtree). | |
| 13 | :- use_module(store). | |
| 14 | :- use_module(bmachine). | |
| 15 | :- use_module(kernel_objects). | |
| 16 | :- use_module(error_manager). | |
| 17 | :- use_module(kernel_waitflags). | |
| 18 | :- use_module(b_enumerate). | |
| 19 | :- use_module(state_space). | |
| 20 | ||
| 21 | :- use_module(b_interpreter). | |
| 22 | ||
| 23 | :- use_module(debug). | |
| 24 | ||
| 25 | :- use_module(module_information,[module_info/2]). | |
| 26 | :- module_info(group,interpreter). | |
| 27 | :- module_info(description,'This is an Event-B specific part of the interpreter. It contains the interpreter rules for events (as opposed to operations in classical B.'). | |
| 28 | ||
| 29 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 30 | % Event-B multilevel execution | |
| 31 | % | |
| 32 | % used shortcuts: IS=InState, OS=OutState, LS=LocalState | |
| 33 | ||
| 34 | % execute an Event: | |
| 35 | % difference with b_event_with_change_set : OutState already setup | |
| 36 | b_event(TBody,Parameters,NormalisedParaValues,InState,OutState,Path) :- | |
| 37 | get_texpr_expr(TBody,Event), | |
| 38 | b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,no_change_set_available,OutState,Path). | |
| 39 | ||
| 40 | ||
| 41 | :- use_module(store,[copy_variable_store/4]). | |
| 42 | % a version of b_event which gets the operation ChangeSet passed | |
| 43 | b_event_with_change_set(TBody,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path) :- | |
| 44 | get_texpr_expr(TBody,Event), | |
| 45 | b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path). | |
| 46 | ||
| 47 | /* TO DO: | |
| 48 | b_event_with_change_set_aux(lazy_let_subst(Id,IdExpr,TBody),Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path) :- !, | |
| 49 | add_lazy_let_id_and_expression(Id,IdExpr,LocalState,InState,NewLocalState,WF), | |
| 50 | b_event_with_change_set(TBody,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path). */ | |
| 51 | b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path) :- | |
| 52 | extract_event(Event,Name,Section,Guard), | |
| 53 | setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS), | |
| 54 | % evaluate the event's guard | |
| 55 | evaluate_predicate_if_necessary(Guard,ParamTypedVals,LS,InState), | |
| 56 | % execute the event | |
| 57 | init_trace_of_event(Name,Section,Parameters,ParaValues,Guard,Path,RestPath,Desc), | |
| 58 | (ChangeSet==no_change_set_available -> OutState=Updates | |
| 59 | ; copy_variable_store(InState,ChangeSet,Updates,OutState)), | |
| 60 | execute_event_body(Event,InState,LS,OutState,RestPath,Desc). | |
| 61 | ||
| 62 | evaluate_predicate_if_necessary(Guard,ParamTypedVals,LS,InState) :- | |
| 63 | (pge_algo: do_not_evaluate_guard, ParamTypedVals==[] -> | |
| 64 | % if we already know that the event is enabled | |
| 65 | % in the current state, we don't need to evaluate the guard here | |
| 66 | debug_println(9,guard_will_not_be_evaluated_b_event) | |
| 67 | ; otherwise -> | |
| 68 | evaluate_predicate(Guard,ParamTypedVals,LS,InState) | |
| 69 | ). | |
| 70 | ||
| 71 | % TO DO: add support for lazy_let_subst by calling add_lazy_let_id_and_expression | |
| 72 | :- use_module(error_manager,[add_error/2]). | |
| 73 | extract_event(Event,Name,Section,FullGuard) :- | |
| 74 | Event = rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents), | |
| 75 | !, | |
| 76 | % check for user-defined additional guard | |
| 77 | full_guard(Guard,FullGuard), | |
| 78 | (Name='INITIALISATION',FullGuard \== Guard | |
| 79 | % The guard is evaluated on the state before ! It should be executed on the state after ! %% TO DO | |
| 80 | -> add_error(b_interpreter_eventb,'Additional guards not yet supported for Event-B INITIALISATION') | |
| 81 | ; true). | |
| 82 | extract_event(Event,Name,Section,FullGuard) :- | |
| 83 | add_internal_error('Illegal Event-B Event: ',extract_event(Event,Name,Section,FullGuard)),fail. | |
| 84 | ||
| 85 | setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS) :- | |
| 86 | empty_state(EmptyState), | |
| 87 | set_up_typed_localstate(Parameters,ParaValues,ParamTypedVals,EmptyState,LS,positive), | |
| 88 | store:l_expand_and_normalise_values(ParaValues,NormalisedParaValues,Parameters). | |
| 89 | ||
| 90 | init_trace_of_event(Name,Section,Parameters,ParaValues,FullGuard,[event(Path),eventtrace(Trace)],RestPath,D2) :- | |
| 91 | Path = [event(Name,ParaValues)|RestPath], | |
| 92 | eventtrace_init(Name,Desc,Trace), | |
| 93 | eventtrace_add(event(Name,Section),Desc,D1), | |
| 94 | eventtrace_add(true_guard(Parameters,ParaValues,FullGuard),D1,D2). | |
| 95 | ||
| 96 | full_guard(Guard,FullGuard) :- | |
| 97 | bmachine:b_machine_temp_predicate(TempPred),!, | |
| 98 | conjunct_predicates([TempPred,Guard],FullGuard). | |
| 99 | full_guard(Guard,Guard). | |
| 100 | ||
| 101 | execute_event_body(Event,InState,LS,OutState,AbstractPath,D) :- | |
| 102 | Event = rlevent(_Name,_Section,Status,_Params,_Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents), | |
| 103 | % for convergent/anticipated events: check if the variant is non-negative | |
| 104 | check_event_entry_status(Status,InState,LS,VariantValue,D,D2), | |
| 105 | % check if the theorems hold | |
| 106 | check_event_theorems(Theorems,InState,LS,D2,D3), | |
| 107 | % execute the actions | |
| 108 | b_execute_eventb_actions(Actions,InState,LS,OutState,D3,D4), | |
| 109 | % for convergent/anticipated events: check if the variant has decreased/not increased | |
| 110 | check_event_exit_status(VariantValue,Status,OutState,LS,D4,D5), | |
| 111 | check_if_invalid_vars_are_modified(Unmodifiables,InState,OutState,D5), | |
| 112 | %print(go_for_abstract(AbstractEvents,VWitnesses,PWitnesses)),nl, | |
| 113 | go_for_abstract_events(AbstractEvents,VWitnesses,PWitnesses,InState,LS,OutState,AbstractPath,D5). | |
| 114 | ||
| 115 | ||
| 116 | go_for_abstract_events([],_VWit,_PWit,_IS,_LS,_OS,[],D) :- | |
| 117 | % no more refined level exists, stop here | |
| 118 | !, eventtrace_finalise(D,_). | |
| 119 | go_for_abstract_events(AbstractEvents,[],[],IS,LS,OS,AbstractPath,Din) :- | |
| 120 | !, % optimisation: If no witness has to be evaluated, do not copy primed variables | |
| 121 | execute_abstract_events(AbstractEvents,[],[],IS,LS,OS,AbstractPath,Din). | |
| 122 | go_for_abstract_events(AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,Din) :- | |
| 123 | % copy a primed version of all values in the outstate into the local state | |
| 124 | copy_primed(OS,LS,NewLS), | |
| 125 | % evaluate witnesses for dropped abstract vars | |
| 126 | evaluate_witnesses_for_abstract_vars(VWitnesses,IS,NewLS,OS,Din,D1), | |
| 127 | % evaluate witnesses for dropped parameters | |
| 128 | evaluate_witnesses_for_abstract_parameters(PWitnesses,IS,NewLS,AbsLS,Params,PValues,D1,D2), | |
| 129 | % continue with the next refinement level | |
| 130 | execute_abstract_events(AbstractEvents,Params,PValues,IS,AbsLS,OS,AbstractPath,D2). | |
| 131 | ||
| 132 | check_event_entry_status(TStatus,IS,LS,VariantValue,Din,Dout) :- | |
| 133 | get_texpr_expr(TStatus,Status), | |
| 134 | check_event_entry_status2(Status,IS,LS,VariantValue,Din,Dout). | |
| 135 | check_event_entry_status2(ordinary,_IS,_LS,-,D,D). | |
| 136 | check_event_entry_status2(anticipated(Variant),IS,LS,Val,Din,Dout) :- | |
| 137 | variant_is_not_negative(Variant,anticipated,IS,LS,Val,Din,Dout). | |
| 138 | check_event_entry_status2(convergent(Variant),IS,LS,Val,Din,Dout) :- | |
| 139 | variant_is_not_negative(Variant,convergent,IS,LS,Val,Din,Dout). | |
| 140 | variant_is_not_negative(Variant,_CType,IS,LS,Value,Din,Dout) :- | |
| 141 | get_texpr_type(Variant, set(_)),!, | |
| 142 | % if variant is of type set, it cannot be negative | |
| 143 | % nevertheless, we compute its value here to check later if the set has been decreased | |
| 144 | if( b_compute_expression_nowf(Variant,LS,IS,Value), % Daniel: why are LS & IS swapped ? | |
| 145 | Din=Dout, | |
| 146 | eventtrace_store_event_error(event_wd_error(Variant,variant),Din,Dout)). | |
| 147 | variant_is_not_negative(Variant,CType,IS,LS,Value,Din,Dout) :- | |
| 148 | % print_bt_message(computing_variant), print_bexpr(Variant),nl, | |
| 149 | % print(local(LS)), nl, print(global(IS)),nl, | |
| 150 | if( b_compute_expression_nowf(Variant,LS,IS,Value), % Daniel: why are LS & IS swapped ? | |
| 151 | %print_bt_message(variant(Value)), | |
| 152 | ( less_than(Value, int(0)) -> | |
| 153 | eventtrace_store_event_error(variant_negative(CType,Variant,Value),Din,Dout) | |
| 154 | ; otherwise -> eventtrace_add(variant_checked_pre(CType,Variant,Value),Din,Dout)), | |
| 155 | eventtrace_store_event_error(event_wd_error(Variant,variant),Din,Dout)). | |
| 156 | ||
| 157 | ||
| 158 | check_event_exit_status(-,_TStatus,_OS,_LS,D,D) :- !. | |
| 159 | check_event_exit_status(EntryValue,TStatus,OS,LS,Din,Dout) :- | |
| 160 | get_texpr_expr(TStatus,Status), | |
| 161 | % Status is convergent(VariantExpr) or anticipated(VariantExpr) | |
| 162 | functor(Status,CType,1),arg(1,Status,VariantExpr), | |
| 163 | get_texpr_type(VariantExpr,Type), | |
| 164 | if( b_compute_expression_nowf(VariantExpr,LS,OS,ExitValue), | |
| 165 | ( variant_condition(CType,Type,EntryValue,ExitValue) -> | |
| 166 | eventtrace_add(variant_checked_post(CType,VariantExpr,EntryValue,ExitValue),Din,Dout) | |
| 167 | ; otherwise -> | |
| 168 | eventtrace_store_event_error(invalid_variant(CType,VariantExpr,EntryValue,ExitValue),Din,Dout)), | |
| 169 | eventtrace_store_event_error(event_wd_error(VariantExpr,variant_after_event),Din,Dout)). | |
| 170 | ||
| 171 | ||
| 172 | variant_condition(anticipated, integer, Pre, Post) :- !, less_than_equal(Post,Pre). | |
| 173 | variant_condition(anticipated, set(_), Pre, Post) :- !, check_subset_of(Post,Pre). | |
| 174 | variant_condition(convergent, integer, Pre, Post) :- !, less_than(Post,Pre). | |
| 175 | variant_condition(convergent, set(_), Pre, Post) :- !, strict_subset_of(Post,Pre). | |
| 176 | ||
| 177 | check_event_theorems([],_State,_LState,D,D). | |
| 178 | check_event_theorems([Theorem|Trest],State,LState,Din,Dout) :- | |
| 179 | check_event_theorem(Theorem,State,LState,Din,Dinter), | |
| 180 | check_event_theorems(Trest,State,LState,Dinter,Dout). | |
| 181 | check_event_theorem(Theorem,State,LState,Din,Dout) :- | |
| 182 | ( evaluate_predicate(Theorem,[],LState,State) -> | |
| 183 | Din = Dout | |
| 184 | %eventtrace_add(theorem_checked(Theorem),Din,Dout) | |
| 185 | ; otherwise -> | |
| 186 | eventtrace_store_event_error(invalid_theorem_in_guard(Theorem),Din,Dout) | |
| 187 | ). | |
| 188 | ||
| 189 | % check if variables that are not modified by an abstract event or newly introduced into | |
| 190 | % the current refinement level are modified. | |
| 191 | check_if_invalid_vars_are_modified([],_IS,_OS,_D). | |
| 192 | check_if_invalid_vars_are_modified([Unmod|UnmodRest],IS,OS,D) :- | |
| 193 | check_unmodifiable(Unmod,IS,OS,D), | |
| 194 | check_if_invalid_vars_are_modified(UnmodRest,IS,OS,D). | |
| 195 | check_unmodifiable(Var,IS,OS,D) :- | |
| 196 | def_get_texpr_id(Var,Id), | |
| 197 | lookup_value(Id,IS,Pre),!, | |
| 198 | lookup_value(Id,OS,Post),!, | |
| 199 | ( equal_object(Pre,Post) -> true | |
| 200 | ; otherwise -> | |
| 201 | eventtrace_failure(invalid_modification(Var,Pre,Post),D)). | |
| 202 | ||
| 203 | evaluate_witnesses_for_abstract_parameters(Witnesses,IS,LS,AbsLS,Params,PValues,Din,Dout) :- | |
| 204 | evaluate_witnesses_for_abstract_parameters2(Witnesses,IS,LS,LS,AbsLS,Params,PValues,Din,Dout). | |
| 205 | evaluate_witnesses_for_abstract_parameters2([],_State,_OrigLS,LS,LS,[],[],D,D). | |
| 206 | evaluate_witnesses_for_abstract_parameters2([Witness|WRest],State,OrigLS,LS,AbsLS,[TId|Params],[Value|PValues],Din,Dout) :- | |
| 207 | witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS), | |
| 208 | if( evaluate_predicate(Predicate,TypedVals,WitnessLS,State), | |
| 209 | ( eventtrace_add(eval_witness(parameter,TId,Value,Predicate),Din,D1), | |
| 210 | evaluate_witnesses_for_abstract_parameters2(WRest,State,OrigLS,ExtLS,AbsLS,Params,PValues,D1,Dout)), | |
| 211 | eventtrace_failure(no_witness_found(parameter,TId,Predicate), Din) ). | |
| 212 | ||
| 213 | witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS) :- | |
| 214 | extract_witness(Witness,TId,Id,_Type,Predicate), | |
| 215 | set_up_typed_localstate([TId],[Value],TypedVals,LS,ExtLS,positive), | |
| 216 | add_var_to_localstate(Id,Value,OrigLS,WitnessLS). | |
| 217 | ||
| 218 | extract_witness(Witness,TId,Id,Type,Predicate) :- | |
| 219 | get_texpr_expr(Witness,witness(TId,Predicate)), | |
| 220 | def_get_texpr_id(TId,Id), | |
| 221 | get_texpr_type(TId,Type). | |
| 222 | ||
| 223 | eventtrace_init(EventName, desc(EventName,D,D), D). | |
| 224 | eventtrace_add( Entry, desc(EN,D,[Entry|L]), desc(EN,D,L) ). | |
| 225 | eventtrace_name( desc(EN,_,_), EN). | |
| 226 | eventtrace_finalise(desc(_EN,D,[]),D). | |
| 227 | eventtrace_store_event_error(Error,Din,Dout) :- | |
| 228 | eventtrace_name(Din, EventName), | |
| 229 | copy_term(Din,Dcopy), | |
| 230 | eventtrace_add(Error,Dcopy,Dc1), | |
| 231 | eventtrace_finalise(Dc1,D), | |
| 232 | store_error_for_context_state(eventerror(EventName,Error,D),Id), | |
| 233 | eventtrace_add(error(Error,Id),Din,Dout). | |
| 234 | eventtrace_failure(Error,Desc) :- | |
| 235 | eventtrace_name(Desc,EventName), | |
| 236 | eventtrace_add(Error,Desc,D1), | |
| 237 | eventtrace_finalise(D1,D), | |
| 238 | store_error_for_context_state(eventerror(EventName,Error,D),_Id), | |
| 239 | fail. | |
| 240 | ||
| 241 | evaluate_predicate(Predicate,TypedVals,LS,State) :- | |
| 242 | init_wait_flags(WF), | |
| 243 | enumerate_predicate(Predicate,TypedVals,LS,State,WF), | |
| 244 | ground_wait_flags(WF). | |
| 245 | ||
| 246 | enumerate_predicate(Predicate,TypedVals,LS,State,WF) :- | |
| 247 | b_test_boolean_expression(Predicate,LS,State,WF), | |
| 248 | b_tighter_enumerate_values(TypedVals,WF). % moved this later for performance, see PerformanceTests/ParameterEnumeration_mch.eventb | |
| 249 | ||
| 250 | execute_abstract_events(Events,Params,PValues,IS,LS,OS,[event(Name,PValues)|Path],Din) :- | |
| 251 | if( select_event(Events,Params,PValues,IS,LS,Event,Name,Din,D1), | |
| 252 | execute_event_body(Event,IS,LS,OS,Path,D1), | |
| 253 | ( generate_simulation_error(Events,Error), eventtrace_failure(Error,Din) )). | |
| 254 | ||
| 255 | generate_simulation_error(Events,simulation_error(FailedEvents)) :- | |
| 256 | generate_simulation_error2(Events,FailedEvents). | |
| 257 | generate_simulation_error2([],[]). | |
| 258 | generate_simulation_error2([TEvent|Erest],[event(Name,Section,Guard)|Srest]) :- | |
| 259 | get_texpr_expr(TEvent,Event), | |
| 260 | Event = rlevent(Name,Section,_Status,_Params,Guard,_Thms,_Actions,_VWitnesses,_PWitnesses,_Unmodifiables,_AbstractEvents), | |
| 261 | generate_simulation_error2(Erest,Srest). | |
| 262 | ||
| 263 | select_event(Events,Params,PValues,IS,LS,Event,Name,Din,Dout) :- | |
| 264 | member(TEvent,Events), | |
| 265 | get_texpr_expr(TEvent,Event), | |
| 266 | Event = rlevent(Name,Section,_Status,_Params,Guard,_Thms,_Act,_VWit,_PWit,_Unmod,_Evt), | |
| 267 | b_test_boolean_expression_wf(Guard,LS,IS), | |
| 268 | eventtrace_add(event(Name,Section),Din,D1), | |
| 269 | eventtrace_add(true_guard(Params,PValues,Guard),D1,Dout). | |
| 270 | ||
| 271 | evaluate_witnesses_for_abstract_vars([],_IS,_LS,_OS,D,D). | |
| 272 | evaluate_witnesses_for_abstract_vars([Witness|WRest],IS,LS,OS,Din,Dout) :- | |
| 273 | extract_witness(Witness,TId,Id,Type,Predicate), | |
| 274 | if( (init_wait_flags(WF), | |
| 275 | b_enumerate_values_in_store([Id],[Type],[Value],LS,WF), | |
| 276 | b_test_boolean_expression(Predicate,LS,IS,WF), | |
| 277 | ground_wait_flags(WF)), | |
| 278 | ( eventtrace_add(eval_witness(variable,TId,Value,Predicate),Din,D1), | |
| 279 | evaluate_witnesses_for_abstract_vars(WRest,IS,LS,OS,D1,Dout)), | |
| 280 | eventtrace_failure(no_witness_found(variable,TId,Predicate),Din) ). | |
| 281 | ||
| 282 | b_execute_eventb_actions([],_IS,_LS,_OS,D,D). | |
| 283 | b_execute_eventb_actions([TAction|ARest],IS,LS,OS,Din,Dout) :- | |
| 284 | get_texpr_expr(TAction,Action), | |
| 285 | if( ( init_wait_flags(WF), | |
| 286 | b_execute_eventb_action(Action,IS,LS,OS,WF,Step), | |
| 287 | ground_wait_flags(WF)), | |
| 288 | ( eventtrace_add(Step,Din,D1), | |
| 289 | b_execute_eventb_actions(ARest,IS,LS,OS,D1,Dout)), | |
| 290 | eventtrace_failure(action_not_executable(TAction),Din)). | |
| 291 | %get_assigned_vars(TAction,Assigned) :- | |
| 292 | % get_texpr_info(TAction,Info), | |
| 293 | % member(assigned_after(Assigned),Info),!. | |
| 294 | b_execute_eventb_action(assign(Lhs,Exprs),IS,LS,OS,WF,Step) :- !, | |
| 295 | b_interpreter:b_compute_expressions(Exprs,LS,IS,VALs,WF), % VALs - a list of computed values | |
| 296 | b_interpreter:b_assign_values_or_functions(Lhs,VALs,LS,IS,NewValues,WF,output_required), | |
| 297 | eventb_store_new_values(NewValues,OS), | |
| 298 | Step = action(Lhs,Exprs,VALs). | |
| 299 | b_execute_eventb_action(becomes_element_of(Lhs,Rhs),IS,LS,OS,WF,Step) :- !, | |
| 300 | convert_pairs_into_list(Lhs,Val,ValList), | |
| 301 | get_texpr_types(Lhs,Types), | |
| 302 | b_compute_expression(Rhs,LS,IS,ValueSet,WF), | |
| 303 | check_element_of_wf(Val,ValueSet,WF), | |
| 304 | b_enumerate_typed_values(ValList,Types,WF), | |
| 305 | % ground_det_wait_flag(WF), | |
| 306 | b_interpreter:b_assign_values_or_functions(Lhs,ValList,LS,IS,NewValues,WF,output_required), | |
| 307 | eventb_store_new_values(NewValues,OS), | |
| 308 | Step = action_set(Lhs,Rhs,ValueSet,ValList). | |
| 309 | b_execute_eventb_action(becomes_such(Ids,Pred),IS,LS,OS,WF,Step) :- !, | |
| 310 | b_interpreter:b_execute_becomes_such(Ids,Pred,LS,IS,OutputValues,IdsValues,WF), | |
| 311 | eventb_store_new_values(OutputValues,OS), | |
| 312 | Step = action_pred(Ids,Pred,IdsValues). | |
| 313 | b_execute_eventb_action(Action,IS,LS,OS,WF,Step) :- | |
| 314 | add_internal_error('Unknown Event-B action: ',b_execute_eventb_action(Action,IS,LS,OS,WF,Step)),fail. | |
| 315 | %b_execute_eventb_action(evb2_becomes_such(Ids,Pred),IS,LS,OS,WF,Step) :- % is now translated to becomes_such | |
| 316 | % add_primed_vars(Ids,OS,LS,NewLS,TypedVals,Values), | |
| 317 | % b_tighter_enumerate_values(TypedVals,WF),b_test_boolean_expression(Pred,NewLS,IS,WF), | |
| 318 | % Step = action_pred(Ids,Pred,Values). | |
| 319 | ||
| 320 | %primed vars always trigger an enum warning | |
| 321 | %this might be split up depending on where they are introduced | |
| 322 | %add_primed_vars([],_State,LS,LS,[],[]). | |
| 323 | %add_primed_vars([TId|IRest],State,In,Out,[typedval(Value,Type,Id,trigger_true(Primed))|TypeValRest],[Value|Vrest]) :- | |
| 324 | % def_get_texpr_id(TId,Id), get_texpr_type(TId,Type), | |
| 325 | % lookup_value(Id,State,Value), | |
| 326 | % atom_concat(Id,'\'',Primed), | |
| 327 | % add_var_to_localstate(Primed,Value,In,Inter), | |
| 328 | % add_primed_vars(IRest,State,Inter,Out,TypeValRest,Vrest). | |
| 329 | ||
| 330 | eventb_store_new_values([],_Store). | |
| 331 | eventb_store_new_values([bind(Id,Value)|IRest],Store) :- | |
| 332 | (lookup_value(Id,Store,Res) -> StoreValue=Res | |
| 333 | ; add_internal_error('Cannot find Event-B identifier:',Id:Store),fail), | |
| 334 | equal_object(StoreValue,Value), | |
| 335 | eventb_store_new_values(IRest,Store). | |
| 336 | ||
| 337 | ||
| 338 | % copy_primed(+Store, +InStore, -OutStore) | |
| 339 | % copies and primes all variables from Store | |
| 340 | % TO DO: maybe only copy those that are really used as primed variables in witnesses,... | |
| 341 | copy_primed([], InStore, InStore). | |
| 342 | copy_primed([bind(OldVar,Value)|Srest], InStore, OutStore) :- | |
| 343 | atom_concat(OldVar,'\'',NewVar), % is faster than caching this using a dynamic fact | |
| 344 | copy_primed(Srest,[bind(NewVar,Value)|InStore], OutStore). | |
| 345 | ||
| 346 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 347 | % Multilevel-animation: Version that is intended to set up constraints | |
| 348 | % between two states and not to find errors in one event | |
| 349 | ||
| 350 | % part below only used for cbc/state_model_check | |
| 351 | ||
| 352 | b_event_constraints(TBody,Parameters,NormalisedParaValues,IS,OS,Path,WF) :- | |
| 353 | get_texpr_expr(TBody,Event), | |
| 354 | b_event_constraints_aux(Event,Parameters,NormalisedParaValues,IS,OS,Path,WF). | |
| 355 | ||
| 356 | b_event_constraints_aux(Event,Parameters,NormalisedParaValues,IS,OS,Path,WF) :- | |
| 357 | extract_event(Event,Name,Section,Guard), | |
| 358 | setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS), | |
| 359 | % evaluate guard | |
| 360 | enumerate_predicate(Guard,ParamTypedVals,LS,IS,WF), | |
| 361 | % execute the event | |
| 362 | init_trace_of_event(Name,Section,Parameters,ParaValues,Guard,Path,RestPath,Desc), | |
| 363 | event_body_constraints(Event,IS,LS,OS,RestPath,Desc,WF). | |
| 364 | ||
| 365 | event_body_constraints(Event,IS,LS,OS,AbstractPath,D,WF) :- | |
| 366 | Event = rlevent(_Name,_Section,_Status,_Params,_Guard,_Thms,Actions,VWitnesses,PWitnesses,_Unmodifiables,AbstractEvents), | |
| 367 | % for convergent/anticipated events: check if the variant is non-negative | |
| 368 | % check_event_entry_status(Status,IS,LS,VariantValue,D,D2), | |
| 369 | eventb_actions_constraints(Actions,IS,LS,OS,D,D2,WF), | |
| 370 | % for convergent/anticipated events: check if the variant has decreased/not increased | |
| 371 | % check_event_exit_status(VariantValue,Status,OS,LS,D3,D4), | |
| 372 | % check_if_invalid_vars_are_modified(Unmodifiables,IS,OS,D4), | |
| 373 | abstract_event_constraints(AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,D2,WF). | |
| 374 | ||
| 375 | eventb_actions_constraints([],_IS,_LS,_OS,D,D,_WF). | |
| 376 | eventb_actions_constraints([TAction|ARest],IS,LS,OS,Din,Dout,WF) :- | |
| 377 | get_texpr_expr(TAction,Action), | |
| 378 | b_execute_eventb_action(Action,IS,LS,OS,WF,Step), | |
| 379 | eventtrace_add(Step,Din,D1), | |
| 380 | eventb_actions_constraints(ARest,IS,LS,OS,D1,Dout,WF). | |
| 381 | ||
| 382 | abstract_event_constraints([],_VWit,_PWit,_IS,_LS,_OS,[],D,_WF) :- | |
| 383 | % no more refined level exists, stop here | |
| 384 | !, eventtrace_finalise(D,_). | |
| 385 | abstract_event_constraints(AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,Din,WF) :- | |
| 386 | % copy a primed version of all values in the outstate | |
| 387 | % into the local state | |
| 388 | copy_primed(OS,LS,NewLS), | |
| 389 | % evaluate witnesses for dropped abstract vars | |
| 390 | abstract_var_witnesses_constraints(VWitnesses,IS,NewLS,OS,Din,D1,WF), | |
| 391 | % evaluate witnesses for dropped parameters | |
| 392 | abstract_parameter_witnesses_constraints(PWitnesses,IS,NewLS,AbsLS,_Params,_PValues,D1,D2,WF), | |
| 393 | % continue with the next refinement level | |
| 394 | execute_abstract_events_with_constraints(AbstractEvents,IS,AbsLS,OS,AbstractPath,D2,WF). | |
| 395 | ||
| 396 | abstract_var_witnesses_constraints([],_IS,_LS,_OS,D,D,_WF). | |
| 397 | abstract_var_witnesses_constraints([Witness|WRest],IS,LS,OS,Din,Dout,WF) :- | |
| 398 | extract_witness(Witness,TId,Id,Type,Predicate), | |
| 399 | b_enumerate_values_in_store([Id],[Type],[Value],LS,WF), | |
| 400 | b_test_boolean_expression(Predicate,LS,IS,WF), | |
| 401 | eventtrace_add(eval_witness(variable,TId,Value,Predicate),Din,D1), | |
| 402 | abstract_var_witnesses_constraints(WRest,IS,LS,OS,D1,Dout,WF). | |
| 403 | ||
| 404 | abstract_parameter_witnesses_constraints(Witnesses,IS,LS,AbsLS,Params,PValues,Din,Dout,WF) :- | |
| 405 | abstract_parameter_witnesses_constraints2(Witnesses,IS,LS,LS,AbsLS,Params,PValues,Din,Dout,WF). | |
| 406 | abstract_parameter_witnesses_constraints2([],_State,_OrigLS,LS,LS,[],[],D,D,_WF). | |
| 407 | abstract_parameter_witnesses_constraints2([Witness|WRest],State,OrigLS,LS,AbsLS,[TId|Params],[Value|PValues],Din,Dout,WF) :- | |
| 408 | witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS), | |
| 409 | enumerate_predicate(Predicate,TypedVals,WitnessLS,State,WF), | |
| 410 | eventtrace_add(eval_witness(parameter,TId,Value,Predicate),Din,D1), | |
| 411 | abstract_parameter_witnesses_constraints2(WRest,State,OrigLS,ExtLS,AbsLS,Params,PValues,D1,Dout,WF). | |
| 412 | ||
| 413 | execute_abstract_events_with_constraints(AbstractEvents,IS,LS,OS,Path,D,WF) :- | |
| 414 | % This introduces a choicepoint when there are more than one abstract event. | |
| 415 | % But the usual case is just one abstract event | |
| 416 | member(TEvent,AbstractEvents), | |
| 417 | get_texpr_expr(TEvent,Event), | |
| 418 | event_body_constraints(Event,IS,LS,OS,Path,D,WF). |