1 % (c) 2009-2025 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,EnablingCondition,BecomesSuchVars,IsPrecise) -> true
103 ; add_internal_error('Getting enabling condition failed: ',Body),
104 create_texpr(truth,pred,PosInfos,EnablingCondition),
105 BecomesSuchVars=[]).
106
107 get_operation_enabling_condition1(if(IfList),PosInfos,Res,BecomesSuchVars,IsPrecise) :- !,
108 ? maplist5(get_if_condition(IsPrecise),IfList,Tests,Conds,BecomesSuchVars1),
109 append(BecomesSuchVars1,BecomesSuchVars),
110 ? (member(X,Conds), \+ is_truth(X)
111 -> disjoin_ifs(Tests,Conds,[],L),
112 conjunct_predicates_with_pos_info(L,Res)
113 ; create_texpr(truth,pred,PosInfos,Res) % all branches have no enabling condition
114 ).
115 get_operation_enabling_condition1(Subst,PosInfos,Truth,[],_Prcise) :- has_no_enabling_condition(Subst),!,
116 create_texpr(truth,pred,PosInfos,Truth).
117 get_operation_enabling_condition1(case(A,_,_),PosInfos,Truth,[],imprecise) :- !, % CASE is now translated to LET + IF-THEN-ELSE in b_ast_cleanup
118 print('Not computing enabling for CASE: '), translate:print_bexpr(A),nl,
119 create_texpr(truth,pred,PosInfos,Truth).
120 get_operation_enabling_condition1(becomes_element_of(_LHS,RHS),PosInfos,Res,[],_Precise) :-
121 obtain_action_enabling_conditions,
122 get_texpr_expr(RHS,RHSExpr),get_texpr_type(RHS,Type),!,
123 (simplify_enabling_condition(true),
124 definitely_not_empty(RHSExpr,Type)
125 -> %print(def_not_empty(RHSExpr)),nl,
126 create_texpr(truth,pred,PosInfos,Res)
127 ; create_texpr(empty_set,Type,[],EmptySet),
128 safe_create_texpr(not_equal(RHS,EmptySet),pred,PosInfos,Res2),
129 %print(not_equal_empty(RHSExpr,Type)),nl,
130 clean_up(Res2,[],Res)
131 ).
132 get_operation_enabling_condition1(Body,_,EnablingCondition,BecomesSuchVars,IsPrecise) :-
133 ? get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars,IsPrecise),!.
134 get_operation_enabling_condition1(X,PosInfos,Truth,[],imprecise) :- %print(cannot_obtain(X)),nl,
135 (obtain_action_enabling_conditions
136 -> functor(X,F,A),debug_println(9,cannot_obtain_enabling(F/A,X)) ; true),
137 create_texpr(truth,pred,PosInfos,Truth).
138
139 /* TO DO: recursively expand the code below for more complicated SELECT,ANY,... */
140 get_operation_enabling_condition2(precondition(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % PRE
141 get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
142 conjunct_predicates_with_pos_info(PreCond,RC,Res).
143 get_operation_enabling_condition2(assertion(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ASSERT
144 get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).
145 get_operation_enabling_condition2(witness_then(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % WITNESS
146 get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).
147 get_operation_enabling_condition2(block(TBody),Res,BecomesSuchVars,IsPrecise) :- !, % BEGIN ... END
148 get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).
149 get_operation_enabling_condition2(choice(ChoiceList),Res,BecomesSuchVars,IsPrecise) :- !, % CHOICE ... OR ...
150 get_disjunction_of_enabling_conditions(ChoiceList,Res,BecomesSuchVars,IsPrecise).
151 get_operation_enabling_condition2(var(_Parameters,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % VAR
152 % should the Parameters be added somewhere ? In principle the enabling condition should always be true, as we have a low-level construct
153 get_substitution_enabling_condition(TBody,Res,BecomesSuchVars,IsPrecise).
154 get_operation_enabling_condition2(sequence([TBody1|Tail]),Res,BecomesSuchVars,IsPrecise) :- !, % ;
155 get_substitution_enabling_condition(TBody1,Res,BecomesSuchVars,IsPrecise),
156 (nonvar(IsPrecise) -> true
157 ; maplist(has_no_enabling_condition,Tail) -> true
158 ; IsPrecise = imprecise
159 ),
160 (debug_mode(on), nonvar(IsPrecise)
161 -> print(ignoring_potential_enabling_condition_in_tail_of_sequence),nl ; true).
162 % TO DO: compute before-after predicate of TBody1 ? before_after_predicate_list_conjunct_with_equalities ?
163 get_operation_enabling_condition2(lazy_let_subst(ID,ExprOrPred,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
164 Res = b(lazy_let_pred(ID,ExprOrPred,BodyRes),pred,[]),
165 get_substitution_enabling_condition(TBody,BodyRes,BecomesSuchVars,IsPrecise).
166 get_operation_enabling_condition2(let(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % LET
167 % for the moment: treat like ANY, but we could avoid introducing existential quantifier ?!
168 ? get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise).
169 get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ANY
170 get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
171 conjunct_predicates_with_pos_info(PreCond,RC,Res1),
172 simplify_enabling_condition(Simplify),
173 ? construct_optimized_exists(Parameters,Res1,Res,Simplify).
174 %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)]),Res,BecomesSuchVars) :- !,
175 % get_texpr_expr(TBody,Body),
176 % get_operation_enabling_condition2(Body,RC,BecomesSuchVars),
177 % conjunct_predicates([PreCond,RC],Res).
178 %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)],b(skip,_,_)),Res,BecomesSuchVars) :- !,
179 % get_texpr_expr(TBody,Body),
180 % get_operation_enabling_condition2(Body,RC,BecomesSuchVars),
181 % conjunct_predicates([PreCond,RC],Res).
182 get_operation_enabling_condition2(select_when(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !,
183 get_substitution_enabling_condition(TBody,RC,BecomesSuchVars,IsPrecise),
184 conjunct_predicates_with_pos_info(PreCond,RC,Res).
185 get_operation_enabling_condition2(select(ListOfWhens),Res,BecomesSuchVars,IsPrecise) :- !,
186 get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise).
187 get_operation_enabling_condition2(select(ListOfWhens,Else),Res,BecomesSuchVars,IsPrecise) :- !,
188 get_texpr_exprs(ListOfWhens,ListOfSelectWhens),
189 maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1),
190 get_substitution_enabling_condition(Else,ResElse,ElseBecomesSuchVars,IsPrecise),
191 disjunct_predicates([ResElse|Res1],Res),
192 append([ElseBecomesSuchVars|BecomesSuchVars1],BecomesSuchVars).
193 get_operation_enabling_condition2(parallel([TH|T]),Res,BecomesSuchVars,IsPrecise) :- !,
194 get_substitution_enabling_condition(TH,E1,BecomesSuchVarsH,IsPrecise),
195 (T=[] -> Res=E1, BecomesSuchVarsH=BecomesSuchVars
196 ; get_operation_enabling_condition2(parallel(T),E2,BecomesSuchVarsT,IsPrecise),
197 append(BecomesSuchVarsH,BecomesSuchVarsT,BecomesSuchVars),
198 conjunct_predicates_with_pos_info(E1,E2,Res)
199 ).
200 get_operation_enabling_condition2(becomes_such(Vars,Condition),Res,Vars,_Precise) :- % Vars : (Condition)
201 % example x: (x$0 >= 1 & x=x$0+1)
202 obtain_action_enabling_conditions,!,
203 simplify_enabling_condition(Simplify),
204 ? construct_optimized_exists(Vars,Condition,Res1,Simplify),
205 %translate:print_bexpr(Res1),nl,
206 % e.g, for example above we have #x.(x$0 >= 1 & x=x$0+1) -> x$0 >= 1
207 % now rename $0 variables to act on current state to obtain the condition:
208 findall(rename(BeforeId,Id),
209 (member(b(identifier(Id),_,Infos),Vars),
210 member(before_substitution(_,BeforeId),Infos)),
211 RenameList),
212 rename_bt(Res1,RenameList,Res). % for example above: Res is x >= 1
213 get_operation_enabling_condition2(rlevent(_Name,_Section,_Status,_Params,Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),Res,BecomesSuchVars,IsPrecise) :- !,
214 %print(actions(Actions)),nl,
215 % TO DO: have a look at get_full_eventb_guard. Do we want to recurse through the abstractions ?
216 (obtain_action_enabling_conditions
217 -> get_operation_enabling_for_event_b_actions(Actions,Guard,Res,BecomesSuchVars,IsPrecise)
218 ; Res=Guard,BecomesSuchVars=[]).
219 get_operation_enabling_condition2(while(Cond,_,_,_),Truth,[],imprecise) :- !,
220 debug_println(9,enabling_for_while_assumed_true),
221 get_texpr_pos_infos(Cond,PosInfos),
222 create_texpr(truth,pred,PosInfos,Truth).
223 get_operation_enabling_condition2(external_subst_call(Pred,Args),Res,[],_Precise) :-
224 external_subst_enabling_condition(Pred,Args,Cond),!, Res=Cond.
225 get_operation_enabling_condition2(operation_call(Operation,OpCallResults,OpCallParas),Res,BecomeSuchVars,IsPrecise) :-
226 def_get_texpr_id(Operation,op(OperationName)), TopLevel=false,
227 b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel),
228 bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParas,Body2),
229 (b_operation_reads_output_variables(OperationName,[_|_],_)
230 -> bsyntaxtree:replace_ids_by_exprs(Body2,OpResults,OpCallResults,Body3)
231 ; Body3=Body2
232 ),
233 !,
234 %print(get_enabling_for_opcall),nl,translate:print_subst(Body2),nl,
235 get_substitution_enabling_condition(Body3,Res,BecomeSuchVars,IsPrecise).
236
237 % check if an substitution obviously has no guard/pre condition
238 has_no_enabling_condition(assign(_LHS,_RHS)).
239 has_no_enabling_condition(assign_single_id(_LHS,_RHS)).
240 has_no_enabling_condition(skip).
241
242 get_if_condition(IsPrecise,b(if_elsif(Test,TBody),_,_),Test,Condition,BecomesSuchVars) :-
243 get_substitution_enabling_condition(TBody,Condition,BecomesSuchVars,IsPrecise).
244
245 :- use_module(bsyntaxtree, [create_implication/3]).
246 disjoin_ifs([],[],_,[]).
247 disjoin_ifs([Test|TT],[EnableCond|TC],NegSoFar,[Res1|TR]) :-
248 append(NegSoFar,[Test],L),
249 conjunct_predicates_with_pos_info(L,BranchTest),
250 create_implication(BranchTest,EnableCond,Res1), % ELSEIF Test THEN Body ... ---> NegSoFar & Test => EnableCond
251 create_negation(Test,NTest),
252 append(NegSoFar,[NTest],NegSoFar1), % add negation of test as additional test for rest
253 disjoin_ifs(TT,TC,NegSoFar1,TR).
254
255
256 % for a list of substitutions: get enabling conditions and disjoin them
257 get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise) :-
258 get_texpr_exprs(ListOfWhens,ListOfSelectWhens),
259 maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1),
260 disjunct_predicates(Res1,Res),
261 append(BecomesSuchVars1,BecomesSuchVars).
262 get_operation_enabling_condition3(Precise,Exp,Res,BV) :- get_operation_enabling_condition2(Exp,Res,BV,Precise).
263
264 % see more powerful definitely_not_empty_set
265 definitely_not_empty(bool_set,_).
266 definitely_not_empty(integer_set(_),_).
267 definitely_not_empty(float_set,_).
268 definitely_not_empty(real_set,_).
269 definitely_not_empty(identifier(X),set(global(X))). % assume no local version of X overrides global X
270 definitely_not_empty(string_set,_).
271
272
273
274 % get operation enabling condition in context of an event-b action list:
275 get_operation_enabling_for_event_b_actions([],Res,Res,[],_Precise).
276 get_operation_enabling_for_event_b_actions([H|T],InRes,OutRes,BecomesSuchVars,IsPrecise) :-
277 get_substitution_enabling_condition(H,ResH,HBecomesSuchVars,IsPrecise),
278 conjunct_predicates_with_pos_info(InRes,ResH,IntRes),
279 get_operation_enabling_for_event_b_actions(T,IntRes,OutRes,TBecomesSuchVars,IsPrecise),
280 append(HBecomesSuchVars,TBecomesSuchVars,BecomesSuchVars).
281
282 % ---------------
283 :- use_module(bmachine,[b_top_level_operation/1]).
284 % LTSMIN style guards: a guard that does not depend on parameters
285 get_operation_propositional_guards(OpName,Guards,RestBody) :-
286 b_top_level_operation(OpName),
287 b_get_machine_operation_for_animation(OpName,TResults,TParameters,TBody), % requires bmachine to be precompiled
288 get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody).
289
290 :- use_module(translate,[print_bexpr/1]).
291 % the following can be called directly; does not require bmachine to be pre-compiled
292 get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody) :-
293 get_texpr_ids(TParameters,Ids1),
294 get_texpr_ids(TResults,Ids2),
295 append(Ids1,Ids2,Ids), sort(Ids,Parameters),
296 get_operation_guards_aux(TBody,Parameters,top,Guards,RestBody),
297 (debug_mode(off) -> true
298 ; format('OPERATION Guard Splitting ~w (~w)~n',[OpName,Parameters]),
299 print('LTSMin Guards: '), maplist(print_bexpr,Guards),nl,
300 print('LTSMin Body: '), translate:print_subst(RestBody),nl,nl
301 ).
302
303 :- use_module(bsyntaxtree, [conjunction_to_list/2,find_identifier_uses/3]).
304
305
306 get_operation_guards_aux(Subst,Parameters,Top,Guards,OpBody) :-
307 ? get_guards(Subst,Top,TIds,Guard,InnerBody,Infos),
308 get_texpr_ids(TIds,Ids), sort(Ids,NewIds),
309 ord_union(Parameters,NewIds,Parameters2),
310 !,
311 get_parameter_independent_guards(Guard,Parameters2,Indep,Dep),
312 (Dep = []
313 -> OpBody = InnerOpBody % no need to keep b
314 ; conjunct_predicates_with_pos_info(Dep,DepCond),
315 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)
316 ),
317 get_operation_guards_aux(InnerBody,Parameters2,inner,InnerGuards,InnerOpBody),
318 append(Indep,InnerGuards,Guards).
319
320 get_operation_guards_aux(b(rlevent(Name,Sect,Status,Params,EvGuard,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info),
321 Parameters,_,Guards,OpBody) :- !,
322 get_parameter_independent_guards(EvGuard,Parameters,InDepGuards,Dep),
323 (get_variant_pred(Status,VariantPred)
324 -> %print(op_variant(_Name)),nl,translate:print_bexpr(VariantPred),nl,
325 % 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
326 % TO DO: check if we need to add the witnesses as well !
327 Guards = [VariantPred|InDepGuards]
328 ; Guards = InDepGuards),
329 conjunct_predicates_with_pos_info(Dep,DepG),
330 OpBody = b(rlevent(Name,Sect,Status,Params,DepG,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info).
331 get_operation_guards_aux(TB,_,_,[],TB).
332
333
334 :- use_module(bsyntaxtree, [safe_create_texpr/3]).
335 % we integrate the Variant check into the guard to ensure the correct read matrix is produced
336 % currently the Variant is checked upon event entry and for convergent events upon exit for decrease
337 % in principle this should be more of an assertion_predicate or assertion_expression
338 get_variant_pred(b(Status,status,_),Res) :- get_variant_pred_aux(Status,Res).
339 get_variant_pred_aux(anticipated(Variant),Res) :- NATURAL = b(integer_set('NATURAL'),set(integer),[]),
340 safe_create_texpr(member(Variant,NATURAL),pred,Res).
341 get_variant_pred_aux(convergent(Variant),Res) :- NATURAL1 = b(integer_set('NATURAL1'),set(integer),[]),
342 safe_create_texpr(member(Variant,NATURAL1),pred,Res).
343
344
345 get_guards(b(precondition(Guard,TBody),subst,Info), top, [],Guard, TBody, Info) :-
346 preferences:get_preference(treat_outermost_pre_as_select,true).
347 get_guards(b(select([b(select_when(Guard, TBody),subst,_Info1)]),subst,Info2), _, [],Guard, TBody, Info2).
348 % TO DO: for ANY try and extract propositional parts, e.g., for ANY pp WHERE pp:1..xx & z=1/yy THEN …
349 get_guards(b(any(TIds,Guard,TBody),subst,Info),_, TIds,Guard,TBody,Info).
350 get_guards(b(operation_call(Operation,[],Parameters),subst,Info),_, InnerParas,Guard, TBody, Info) :-
351 Parameters=[], % TO DO: improve, will require substituting Parameters inside OpRealBody
352 bmachine_is_precompiled,
353 def_get_texpr_id(Operation,op(OpName)),
354 b_get_machine_operation(OpName,[],RealParameters,OpRealBody,_OType,_OpPos), RealParameters=[],
355 get_guards(OpRealBody, inner, InnerParas, Guard, TBody, _ ).
356
357 construct_select([],Guard,TBody, Infos, Res) :- !,
358 Res = b(select([b(select_when(Guard, TBody),subst,Infos)]),subst,Infos).
359 construct_select(TIds,Guard,TBody,Infos, b(any(TIds,Guard,TBody),subst,Infos)).
360
361
362 get_parameter_independent_guards(Guard,Parameters,Indep,Dep) :-
363 conjunction_to_list(Guard,Gs),
364 l_get_parameter_independent_guards(Gs,Parameters,at_front,Indep,Dep).
365
366 :- use_module(bsyntaxtree,[always_well_defined/1]).
367 l_get_parameter_independent_guards([],_,_,[],[]).
368 l_get_parameter_independent_guards([G|Gs],Parameters,AtFront,Indep,Dep) :-
369 find_identifier_uses(G,[],Ids),
370 ( ord_disjoint(Ids,Parameters),
371 (AtFront=at_front -> true ; always_well_defined(G))
372 -> Indep=[G|I1], Dep=D1, AtFront1=AtFront
373 ; Indep=I1, Dep=[G|D1],
374 AtFront1=not_at_front % we have skipped one guard; the next guard is not guaranteed to be at the front (relevant for well-definedness)
375 ),
376 l_get_parameter_independent_guards(Gs,Parameters,AtFront1,I1,D1).
377
378 % for synthesis of sequential programs
379 % not yet used
380 /*
381 % find events which have common guards
382 get_common_guards(Ev1,Ev2,Common,Rest1,Rest2) :-
383 get_unsimplified_operation_guard(Ev1,G1), conjunction_to_list(G1,GL1),
384 get_unsimplified_operation_guard(Ev2,G2), Ev1 @< Ev2, conjunction_to_list(G2,GL2),
385 find_common(GL1,GL2,Common,Rest1,Rest2),
386 format('~nCommon guard for ~w <-> ~w~n Common: ',[Ev1,Ev2]), translate:l_print_bexpr_or_subst(Common),nl,
387 format(' Rest1: ',[]),translate:l_print_bexpr_or_subst(Rest1),nl,
388 format(' Rest2: ',[]),translate:l_print_bexpr_or_subst(Rest2),nl.
389
390 % check if abrial merge rule 15.3 from Bee-Book for if/while is applicable:
391 get_abrial_rule(Ev1,Ev2,Common,Rest1) :-
392 get_common_guards(Ev1,Ev2,Common,Rest1,Rest2),
393 conjunct_predicates(Rest1,R1),
394 conjunct_predicates(Rest2,R2),
395 is_negated_predicate(R1,R2),
396 format('*** Can be merged ~w <-> ~w !~n~n',[Ev1,Ev2]).
397
398 find_common([],GL2,[],[],GL2).
399 find_common([G1|T1],GL2,[G1|TCommon],Rest1,Rest2) :-
400 select(G2,GL2,T2), % TODO: check WD
401 same_predicate(G1,G2),!, % we could also use norm_expr
402 find_common(T1,T2,TCommon,Rest1,Rest2).
403 find_common([G1|T1],GL2,TCommon,[G1|Rest1],Rest2) :-
404 find_common(T1,GL2,TCommon,Rest1,Rest2).
405
406 same_predicate(G1,G2) :- bsyntaxtree:same_texpr(G1,G2).
407 same_predicate(G1,G2) :- b_interpreter_check:norm_pred_check(G1,N1), b_interpreter_check:norm_pred_check(G2,N2), N2=N1.
408
409 is_negated_predicate(G1,G2) :- bsyntaxtree:is_negation_of(G1,G2).
410 */
411