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