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 | % WARNING (DEPRECATED) : it is planned to replace the debug_properties commands using the unsat_cores.pl predicates | |
6 | % operation enabling code should be moved to a separate module | |
7 | ||
8 | :- module(predicate_debugger,[tcltk_debug_properties/3, | |
9 | tcltk_debug_properties_or_op/4, adapt_tcl_operation_name/2, | |
10 | get_operation_propositional_guards/3, get_operation_propositional_guards/6, | |
11 | get_operation_enabling_condition/7, | |
12 | get_unsimplified_operation_guard/2, | |
13 | get_unsimplified_operation_enabling_condition/5, | |
14 | get_simplified_operation_enabling_condition/5, | |
15 | tcltk_get_unsat_core_with_types/1]). | |
16 | ||
17 | :- use_module(tools). | |
18 | ||
19 | :- use_module(module_information,[module_info/2]). | |
20 | :- module_info(group,misc). | |
21 | :- module_info(description,'The predicate debugger adds conjuncts one by one until the predicate becomes unsatisfiable.'). | |
22 | ||
23 | :- use_module(debug). | |
24 | :- use_module(self_check). | |
25 | :- use_module(preferences). | |
26 | :- use_module(error_manager). | |
27 | ||
28 | :- use_module(translate). | |
29 | :- use_module(b_interpreter). | |
30 | :- use_module(bsyntaxtree). | |
31 | :- use_module(b_ast_cleanup). | |
32 | ||
33 | :- use_module(library(timeout)). | |
34 | :- use_module(library(lists)). | |
35 | ||
36 | ||
37 | :- meta_predicate maplist5(4,-,-,-,-). | |
38 | maplist5(_P,[],[],[],[]). | |
39 | maplist5(P,[H1|T1],[H2|T2],[H3|T3],[H4|T4]) :- | |
40 | if(call(P,H1,H2,H3,H4), | |
41 | maplist5(P,T1,T2,T3,T4), | |
42 | (add_internal_error('Call fails: ',maplist5(P,H1,H2,H3,H4)), | |
43 | fail)). | |
44 | ||
45 | /* b_interpreter:b_debug_properties. */ | |
46 | ||
47 | :- volatile checked_property/1, last_checked_solution/2, failed_property/2, time_out_property/2, cur_conjunct_nr/1, projection_onto_component/1. | |
48 | :- dynamic checked_property/1. | |
49 | :- dynamic last_checked_solution/2. | |
50 | :- dynamic failed_property/2. | |
51 | :- dynamic time_out_property/2. | |
52 | :- dynamic cur_conjunct_nr/1. | |
53 | :- dynamic projection_onto_component/1. | |
54 | ||
55 | reset_debug_properties :- | |
56 | retractall(last_debug_info(_,_)), | |
57 | retractall(checked_property(_)), | |
58 | retractall(last_checked_solution(_,_)), | |
59 | retractall(failed_property(_,_)), | |
60 | retractall(time_out_property(_,_)), | |
61 | retractall(cur_conjunct_nr(_)), | |
62 | retractall(projection_onto_component(_)). | |
63 | ||
64 | :- use_module(b_global_sets,[b_global_set/1, b_get_fd_type_bounds/3, unfixed_deferred_set/1]). | |
65 | tcltk_debug_properties(RealRes,UnsatCore,Satisfiable) :- | |
66 | tcltk_debug_properties_or_op('@PROPERTIES',UnsatCore,RealRes,Satisfiable). | |
67 | ||
68 | % code below because names with $ cause problems in Tcl with eval | |
69 | adapt_tcl_operation_name(X,R) :- var(X),!,R=X. | |
70 | adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !. | |
71 | adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !. | |
72 | adapt_tcl_operation_name(X,X). | |
73 | ||
74 | tcltk_debug_properties_or_op(TclOpName,ComputeUnsatCore,list(RealRes),Satisfiable) :- | |
75 | adapt_tcl_operation_name(TclOpName,OpName), | |
76 | print(tcltk_debug_properties_or_op(OpName,ComputeUnsatCore,RealRes)),nl, | |
77 | (ComputeUnsatCore==false -> | |
78 | (OpName='$setup_constants' -> b_debug_properties | |
79 | ; OpName = '@GOAL' -> b_debug_goal | |
80 | ; b_debug_operation(OpName)) | |
81 | ; set_fast_unsat_core(ComputeUnsatCore), | |
82 | print('*** Finding Unsat Core : '), print(ComputeUnsatCore),nl, | |
83 | (b_find_unsat_core | |
84 | -> print('*** Finished '),nl | |
85 | ; add_error_fail(predicate_debugger,'Finding Unsat Core failed',OpName)) | |
86 | ), | |
87 | print(debugged(OpName)),nl, | |
88 | findall(TP, (checked_property(P), | |
89 | translate_bexpression_with_limit(P,TrP), | |
90 | ajoin([TrP,' &\n'],TP)), | |
91 | Res1), | |
92 | (projection_onto_component(_SubNr) | |
93 | -> Res1P = ['(only a sub-component was analysed)\n'|Res1] ; Res1P=Res1), | |
94 | (Res1=[] -> R1=Res1P ; | |
95 | R1=['\n ********\n\nSATISFIABLE CONSTRAINTS and PROPERTIES:\n'|Res1P] | |
96 | ), | |
97 | findall(TP2,( ((failed_property(P,_),RES='false') ; (time_out_property(P,_),RES='time_out')), | |
98 | translate_status(P,RES,TP2)), | |
99 | Res2), | |
100 | (Res2=[] -> R2=['\nNo unsatisfiable PROPERTY or CONSTRAINT'], Satisfiable=true | |
101 | ; R2=['\n ********\n\nFirst unsatisfiable PROPERTY or CONSTRAINT:\n'|Res2], | |
102 | Satisfiable=false | |
103 | ), | |
104 | findall(TP, (last_checked_solution(ConstantsState,_), % TO DO: Project on remaining variables !? | |
105 | translate_equivalence(b(identifier('SOLUTION'),boolean,[]),ConstantsState,TP)), | |
106 | Res12), | |
107 | append(R2,['\n\n ********\n\nSolution for satisfiable part:\n'|Res12],R2Res12), | |
108 | append(R1,R2Res12,Res), | |
109 | findall(SetDescr,(b_global_set(Set),b_get_fd_type_bounds(Set,LowBnd,UpBnd), Card is 1+UpBnd-LowBnd, | |
110 | create_texpr(identifier(Set),set(global(Set)),[],SetId), | |
111 | create_texpr(card(SetId),integer,[],CardExpr), | |
112 | create_texpr(value(int(Card)),integer,[],ValExpr), | |
113 | create_texpr(equal(CardExpr,ValExpr),prop,[],EqualExpr), | |
114 | translate_bexpression(EqualExpr,SetDescr1), | |
115 | (unfixed_deferred_set(Set) -> Xtra = ' (assumed for deferred set)' ; Xtra=''), | |
116 | ajoin([SetDescr1,Xtra,'\n'],SetDescr)), Sets), | |
117 | ||
118 | append(['\nCardinalities of SETS:\n'|Sets],Res,SRes), | |
119 | preferences:get_preference(minint,MININT), | |
120 | preferences:get_preference(maxint,MAXINT), | |
121 | clear_error_context, | |
122 | ajoin(['MININT .. MAXINT = ',MININT,'..',MAXINT],MINMAX), | |
123 | RealRes = ['SETTINGS:\n',MINMAX|SRes]. | |
124 | tcltk_debug_properties_or_op([],_,list(['Machine has no PROPERTIES']),true). | |
125 | ||
126 | failed_or_time_out_property(P) :- failed_property(P,_) ; time_out_property(P,_). | |
127 | ||
128 | :- use_module(library(codesio),[write_to_codes/2]). | |
129 | :- use_module(tools,[ajoin/2]). | |
130 | % use_module(probsrc(predicate_debugger)),predicate_debugger:print_unsat_core_with_types | |
131 | tcltk_get_unsat_core_with_types(ResultCodes) :- | |
132 | get_unsat_core(AllConj), | |
133 | translate_predicate_into_machine(AllConj,ResultAtom), | |
134 | write_to_codes(ResultAtom,ResultCodes). | |
135 | ||
136 | get_unsat_core(AllConj) :- (checked_property(_) ; failed_or_time_out_property(_)), !, | |
137 | findall(P,checked_property(P),Ps), | |
138 | findall(UnsatP,failed_or_time_out_property(UnsatP),UPs), | |
139 | append(Ps,UPs,All), | |
140 | conjunct_predicates(All,AllConj). | |
141 | get_unsat_core(Core) :- print('No predicate debugger analysis run'),nl, | |
142 | print('Trying to extract from b_interpreter'),nl, | |
143 | b_interpreter:get_unsat_component_predicate(_,Core,_Vars),!. | |
144 | get_unsat_core(b(truth,pred,[])). | |
145 | ||
146 | ||
147 | translate_equivalence(A,B,R) :- | |
148 | translate_bexpression(A,TA), | |
149 | translate_bstate(B,TB), | |
150 | ajoin([TA,'\n == ',TB,'\n'],R). | |
151 | :- use_module(translate,[translate_span/2]). | |
152 | translate_status(A,Status,R) :- | |
153 | translate_bexpression(A,TA), | |
154 | (translate_span(A,ASpan) | |
155 | -> ajoin([TA,'\n == ',Status,' ',ASpan],R) | |
156 | ; ajoin([TA,'\n == ',Status],R)). | |
157 | ||
158 | ||
159 | ||
160 | :- use_module(bmachine). | |
161 | b_debug_properties :- set_error_context(b_debug_properties), | |
162 | reset_debug_properties, | |
163 | %%b_extract_constants_and_properties(Constants,CstTypes,Properties), | |
164 | %b_machine_has_constants_or_properties, | |
165 | b_get_machine_constants(TypedConstants), | |
166 | get_adapted_properties(TypedConstants,AProperties,ATypedConstants,AllowTimeout), | |
167 | nr_of_conjuncts(AProperties,NrConj), | |
168 | (b_debug_properties2(AProperties,ATypedConstants,[],NrConj,AllowTimeout) -> true ; true). | |
169 | ||
170 | b_debug_goal :- | |
171 | bmachine:b_get_machine_goal(Goal), | |
172 | b_debug_predicate(Goal). | |
173 | b_debug_predicate(FullPred) :- set_error_context(b_debug_predicate), | |
174 | reset_debug_properties, | |
175 | get_parameters(FullPred,Params,Pred), | |
176 | get_current_state('@PRED',CurID,CurBState), | |
177 | set_error_context(b_debug_predicate(CurID)), | |
178 | nr_of_conjuncts(Pred,NrConj), | |
179 | (b_debug_properties2(Pred,Params,CurBState,NrConj,allow_timeout) -> true ; true). | |
180 | ||
181 | get_parameters(b(exists(Parameters,Pred),pred,_),Parameters,Pred) :- !. | |
182 | get_parameters(Pred,[],Pred). | |
183 | ||
184 | :- use_module(library(lists)). | |
185 | get_adapted_properties(TypedConstants,Pred,CTypedConstants,do_not_allow_timeout) :- | |
186 | %(b_interpreter:nr_of_components(NrC), NrC>1), | |
187 | preferences:get_preference(partition_predicates,true), | |
188 | b_interpreter:get_unsat_component_predicate(CompNr,Pred,Vars),!, % means there was no timeout | |
189 | assert(projection_onto_component(CompNr)), | |
190 | print(debugging_unsat_or_skipped_component(CompNr)),nl, | |
191 | print(component_vars(Vars)),nl, | |
192 | project_texpr_identifiers(TypedConstants,Vars,CTypedConstants). | |
193 | get_adapted_properties(TypedConstants,Properties,TypedConstants,allow_timeout) :- | |
194 | % TO DO determine whether timeout occured | |
195 | b_get_properties_from_machine(Properties). | |
196 | ||
197 | ||
198 | % only keep texpr_identifiers whose id is in the provided list | |
199 | project_texpr_identifiers([],_,[]). | |
200 | project_texpr_identifiers([TID|T],Vars,Res) :- | |
201 | (get_texpr_id(TID,ID),member(ID,Vars) | |
202 | -> Res = [TID|R2] ; Res=R2), | |
203 | project_texpr_identifiers(T,Vars,R2). | |
204 | ||
205 | :- use_module(specfile,[state_corresponds_to_initialised_b_machine/2, state_corresponds_to_set_up_constants/2]). | |
206 | /* b_interpreter:tcltk_debug_properties_or_op(prog1,R)*/ | |
207 | b_debug_operation(OpName) :- | |
208 | reset_debug_properties, | |
209 | get_current_state(OpName,CurID,CurBState), | |
210 | set_error_context(operation(OpName,CurID)), | |
211 | (get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BSVars,_,true,false) -> true | |
212 | ; add_error(b_debug_operation,'Operation does not exist or cannot determine enabling condition: ',OpName),fail),!, | |
213 | print('Enabling: '), print_bexpr(EnablingCondition),nl, | |
214 | flush_output(user), | |
215 | nr_of_conjuncts(EnablingCondition,NrConj), | |
216 | ~~mnf(insert_before_substitution_variables(BSVars,[],CurBState,CurBState,NewCurBState)), | |
217 | extract_exists_parameters(EnablingCondition,Parameters,NewCond,NewParas), | |
218 | (b_debug_properties2(NewCond,NewParas,NewCurBState,NrConj,allow_timeout) -> true ; true). | |
219 | ||
220 | :- use_module(state_space,[current_expression/2]). | |
221 | get_current_state(OpName,CurID,CurBState) :- | |
222 | (current_expression(CurID,CurState) -> true | |
223 | ; add_error(predicate_debugger,'Could not get current state',OpName),fail), | |
224 | (state_corresponds_to_initialised_b_machine(CurState,CurBState) -> true | |
225 | ; (OpName=='$initialise_machine', | |
226 | state_corresponds_to_set_up_constants(CurState,CurBState)) -> true | |
227 | ; add_error(b_debug_operation,'Machine not yet initialised! ',CurState),fail). | |
228 | ||
229 | ||
230 | % Try to lift out existentially quantified variables to the outer level; to make the debugging more fine-grained | |
231 | extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :- | |
232 | get_texpr_expr(Pred,exists(Vars,Body)), | |
233 | disjoint_list_union(Parameters,Vars,Paras1), !, % also checks if no clash exists; otherwise we have to keep exists | |
234 | print(augmented_paras(Paras1)),nl, | |
235 | extract_exists_parameters(Body,Paras1,NewPred,NewParas). | |
236 | extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :- | |
237 | get_texpr_expr(Pred,conjunct(LHS,RHS)),!, | |
238 | extract_exists_parameters(LHS,Parameters, NewLHS, IntParas), | |
239 | extract_exists_parameters(RHS,IntParas,NewRHS,NewParas), | |
240 | conjunct_predicates([NewLHS,NewRHS],NewPred). | |
241 | extract_exists_parameters(Pred,Par,Pred,Par). | |
242 | ||
243 | ||
244 | :- dynamic obtain_action_enabling_conditions/0, simplify_enabling_condition/1. | |
245 | obtain_action_enabling_conditions. simplify_enabling_condition(true). | |
246 | set_obtain_action_enabling_conditions(true) :- !, | |
247 | (obtain_action_enabling_conditions -> true ; assert(obtain_action_enabling_conditions)). | |
248 | set_obtain_action_enabling_conditions(_) :- retractall(obtain_action_enabling_conditions). | |
249 | set_simplify_enabling_condition(X) :- retractall(simplify_enabling_condition(_)), | |
250 | assert(simplify_enabling_condition(X)). | |
251 | ||
252 | :- use_module(b_interpreter_components,[construct_optimized_exists/3,construct_optimized_exists/4]). | |
253 | :- use_module(specfile,[animation_minor_mode/1]). | |
254 | :- use_module(external_functions,[external_subst_enabling_condition/3]). | |
255 | ||
256 | get_unsimplified_operation_guard(OpName,Guard) :- | |
257 | get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise), | |
258 | construct_optimized_exists(Parameters,EnablingCondition,Guard). | |
259 | ||
260 | get_unsimplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :- | |
261 | ? | Simplify=false, |
262 | ? | (animation_minor_mode(eventb) -> GetFromAction=false |
263 | ; GetFromAction=true), | |
264 | ? | get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise,GetFromAction,Simplify). |
265 | ||
266 | get_simplified_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise) :- | |
267 | Simplify=true, | |
268 | (animation_minor_mode(eventb) -> GetFromAction=false | |
269 | ; GetFromAction=true), | |
270 | get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,Precise,GetFromAction,Simplify). | |
271 | ||
272 | get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BecomesSuchVars,IsPrecise,GetAct,Simplify) :- | |
273 | ? | set_obtain_action_enabling_conditions(GetAct), % specify whether we want also conditions stemming from actions, such as :() or :: |
274 | ? | set_simplify_enabling_condition(Simplify), % specify whether we want to simplify the EnablingCondition if possible |
275 | %%nonvar(OpName), %% I am not sure why this test is here ?? | |
276 | %% print(getting_enabling(OpName,GetAct)),nl,%% | |
277 | ? | b_get_machine_operation_for_animation(OpName,_Results,Parameters,TBody,_OType,true), |
278 | get_operation_enabling_condition1(TBody,EnablingCondition,BecomesSuchVars,IsPreciseV), | |
279 | (var(IsPreciseV) -> IsPrecise = precise ; IsPrecise = imprecise). | |
280 | ||
281 | get_operation_enabling_condition1(TBody,EnablingCondition,BecomesSuchVars,IsPrecise) :- | |
282 | get_texpr_expr(TBody,Body), | |
283 | (get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars,IsPrecise) -> true | |
284 | ; add_internal_error('Getting enabling condition failed: ',Body), | |
285 | %trace,get_operation_enabling_condition2(Body,EnablingCondition,BecomesSuchVars), | |
286 | create_texpr(truth,pred,[],EnablingCondition), | |
287 | BecomesSuchVars=[]). | |
288 | ||
289 | /* TO DO: recursively expand the code below for more complicated SELECT,ANY,... */ | |
290 | get_operation_enabling_condition2(precondition(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % PRE | |
291 | get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise), | |
292 | ~~mnf(conjunct_predicates([PreCond,RC],Res)). | |
293 | get_operation_enabling_condition2(assertion(_PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ASSERT | |
294 | get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise). | |
295 | get_operation_enabling_condition2(block(TBody),Res,BecomesSuchVars,IsPrecise) :- !, % BEGIN ... END | |
296 | get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise). | |
297 | get_operation_enabling_condition2(choice(ChoiceList),Res,BecomesSuchVars,IsPrecise) :- !, % CHOICE ... OR ... | |
298 | get_disjunction_of_enabling_conditions(ChoiceList,Res,BecomesSuchVars,IsPrecise). | |
299 | get_operation_enabling_condition2(var(_Parameters,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % VAR | |
300 | % should the Parameters be added somewhere ? In principle the enabling condition should always be true, as we have a low-level construct | |
301 | get_operation_enabling_condition1(TBody,Res,BecomesSuchVars,IsPrecise). | |
302 | get_operation_enabling_condition2(sequence([TBody1|_]),Res,BecomesSuchVars,imprecise) :- !, % ; | |
303 | (debug:debug_mode(on) -> print(ignoring_potential_enabling_condition_in_tail_of_sequence),nl ; true), | |
304 | % TO DO: compute before-after predicate of TBody1 ? before_after_predicate_list_conjunct_with_equalities ? | |
305 | % we ignore rest of sequence; cannot influence enabling condition; probably this should always return truth | |
306 | get_operation_enabling_condition1(TBody1,Res,BecomesSuchVars,_IsPrecise). | |
307 | get_operation_enabling_condition2(lazy_let_subst(ID,ExprOrPred,TBody),Res,BecomesSuchVars,IsPrecise) :- !, | |
308 | Res = b(lazy_let_pred(ID,ExprOrPred,BodyRes),pred,[]), | |
309 | get_operation_enabling_condition1(TBody,BodyRes,BecomesSuchVars,IsPrecise). | |
310 | get_operation_enabling_condition2(let(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % LET | |
311 | % for the moment: treat like ANY, but we could avoid introducing existential quantifier ?! | |
312 | get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise). | |
313 | get_operation_enabling_condition2(any(Parameters,PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, % ANY | |
314 | get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise), | |
315 | ~~mnf(conjunct_predicates([PreCond,RC],Res1)), | |
316 | simplify_enabling_condition(Simplify), | |
317 | construct_optimized_exists(Parameters,Res1,Res,Simplify). | |
318 | %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)]),Res,BecomesSuchVars) :- !, | |
319 | % get_texpr_expr(TBody,Body), | |
320 | % ~~mnf(get_operation_enabling_condition2(Body,RC,BecomesSuchVars)), | |
321 | % ~~mnf(conjunct_predicates([PreCond,RC],Res)). | |
322 | %get_operation_enabling_condition2(select([b(select_when(PreCond, TBody),_,_)],b(skip,_,_)),Res,BecomesSuchVars) :- !, | |
323 | % get_texpr_expr(TBody,Body), | |
324 | % ~~mnf(get_operation_enabling_condition2(Body,RC,BecomesSuchVars)), | |
325 | % ~~mnf(conjunct_predicates([PreCond,RC],Res)). | |
326 | get_operation_enabling_condition2(select_when(PreCond,TBody),Res,BecomesSuchVars,IsPrecise) :- !, | |
327 | get_operation_enabling_condition1(TBody,RC,BecomesSuchVars,IsPrecise), | |
328 | ~~mnf(conjunct_predicates([PreCond,RC],Res)). | |
329 | get_operation_enabling_condition2(select(ListOfWhens),Res,BecomesSuchVars,IsPrecise) :- !, | |
330 | get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise). | |
331 | get_operation_enabling_condition2(select(ListOfWhens,Else),Res,BecomesSuchVars,IsPrecise) :- !, | |
332 | get_texpr_exprs(ListOfWhens,ListOfSelectWhens), | |
333 | maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1), | |
334 | get_operation_enabling_condition1(Else,ResElse,ElseBecomesSuchVars,IsPrecise), | |
335 | ~~mnf(disjunct_predicates([ResElse|Res1],Res)), | |
336 | append([ElseBecomesSuchVars|BecomesSuchVars1],BecomesSuchVars). | |
337 | get_operation_enabling_condition2(parallel([TH|T]),Res,BecomesSuchVars,IsPrecise) :- !, | |
338 | get_operation_enabling_condition1(TH,E1,BecomesSuchVarsH,IsPrecise), | |
339 | (T=[] -> Res=E1, BecomesSuchVarsH=BecomesSuchVars | |
340 | ; (~~mnf(get_operation_enabling_condition2(parallel(T),E2,BecomesSuchVarsT,IsPrecise)), | |
341 | append(BecomesSuchVarsH,BecomesSuchVarsT,BecomesSuchVars), | |
342 | conjunct_predicates([E1,E2],Res))). | |
343 | get_operation_enabling_condition2(becomes_element_of(_LHS,RHS),Res,[],_Precise) :- | |
344 | obtain_action_enabling_conditions, | |
345 | get_texpr_expr(RHS,RHSExpr),get_texpr_type(RHS,Type),!, | |
346 | (simplify_enabling_condition(true), | |
347 | definitely_not_empty(RHSExpr,Type) | |
348 | -> %print(def_not_empty(RHSExpr)),nl, | |
349 | create_texpr(truth,pred,[],Res) | |
350 | ; create_texpr(empty_set,Type,[],EmptySet), | |
351 | safe_create_texpr(not_equal(RHS,EmptySet),pred,Res2), | |
352 | %print(not_equal_empty(RHSExpr,Type)),nl, | |
353 | ~~mnf(clean_up(Res2,[],Res)) | |
354 | ). | |
355 | get_operation_enabling_condition2(becomes_such(Vars,Condition),Res,Vars,_Precise) :- % Vars : (Condition) | |
356 | % example x: (x$0 >= 1 & x=x$0+1) | |
357 | obtain_action_enabling_conditions,!, | |
358 | simplify_enabling_condition(Simplify), | |
359 | construct_optimized_exists(Vars,Condition,Res1,Simplify), | |
360 | %translate:print_bexpr(Res1),nl, | |
361 | % e.g, for example above we have #x.(x$0 >= 1 & x=x$0+1) -> x$0 >= 1 | |
362 | % now rename $0 variables to act on current state to obtain the condition: | |
363 | findall(rename(BeforeId,Id), | |
364 | (member(b(identifier(Id),_,Infos),Vars), | |
365 | member(before_substitution(_,BeforeId),Infos)), | |
366 | RenameList), | |
367 | rename_bt(Res1,RenameList,Res). % for example above: Res is x >= 1 | |
368 | get_operation_enabling_condition2(rlevent(_Name,_Section,_Status,_Params,Guard,_Theorems,Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),Res,BecomesSuchVars,IsPrecise) :- !, | |
369 | %print(actions(Actions)),nl, | |
370 | % TO DO: have a look at get_full_eventb_guard. Do we want to recurse through the abstractions ? | |
371 | (obtain_action_enabling_conditions | |
372 | -> get_operation_enabling_for_event_b_actions(Actions,Guard,Res,BecomesSuchVars,IsPrecise) | |
373 | ; Res=Guard,BecomesSuchVars=[]). | |
374 | get_operation_enabling_condition2(assign(_LHS,_RHS),Truth,[],_Precise) :- !, | |
375 | create_texpr(truth,pred,[],Truth). | |
376 | get_operation_enabling_condition2(assign_single_id(_IDE,_RHS),Truth,[],_Precise) :- !, | |
377 | create_texpr(truth,pred,[],Truth). | |
378 | get_operation_enabling_condition2(case(A,_,_),Truth,[],imprecise) :- !, % CASE is now translated to LET + IF-THEN-ELSE in b_ast_cleanup | |
379 | print('Not computing enabling for CASE: '), translate:print_bexpr(A),nl, | |
380 | create_texpr(truth,pred,[],Truth). | |
381 | get_operation_enabling_condition2(while(_,_,_,_),Truth,[],imprecise) :- !, | |
382 | debug:debug_println(9,enabling_for_while_assumed_true), | |
383 | create_texpr(truth,pred,[],Truth). | |
384 | get_operation_enabling_condition2(if(IfList),Res,BecomesSuchVars,IsPrecise) :- !, | |
385 | maplist5(get_if_condition(IsPrecise),IfList,Tests,Conds,BecomesSuchVars1), | |
386 | append(BecomesSuchVars1,BecomesSuchVars), | |
387 | ? | ((member(X,Conds), \+ is_truth(X)) |
388 | -> disjoin_ifs(Tests,Conds,[],L), | |
389 | conjunct_predicates(L,Res) | |
390 | ; create_texpr(truth,pred,[],Res) % all branches have no enabling condition | |
391 | ). | |
392 | get_operation_enabling_condition2(skip,Truth,[],_Prcise) :- !, | |
393 | create_texpr(truth,pred,[],Truth). | |
394 | get_operation_enabling_condition2(external_subst_call(Pred,Args),Res,[],_Precise) :- | |
395 | external_subst_enabling_condition(Pred,Args,Cond),!, Res=Cond. | |
396 | get_operation_enabling_condition2(operation_call(Operation,_OpCallResults,OpCallParas),Res,BecomeSuchVars,IsPrecise) :- | |
397 | def_get_texpr_id(Operation,op(OperationName)), | |
398 | b_get_machine_operation_for_animation(OperationName,_OpResults,OpParameters,Body,_OType,_TopLevel), | |
399 | bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParas,Body2), | |
400 | !, | |
401 | %print(get_enabling_for_opcall),nl,translate:print_subst(Body2),nl, | |
402 | get_operation_enabling_condition1(Body2,Res,BecomeSuchVars,IsPrecise). | |
403 | get_operation_enabling_condition2(X,Truth,[],imprecise) :- %print(cannot_obtain(X)),nl, | |
404 | (obtain_action_enabling_conditions | |
405 | -> functor(X,F,A),debug_println(9,cannot_obtain_enabling(F/A,X)) ; true), | |
406 | create_texpr(truth,pred,[],Truth). | |
407 | ||
408 | ||
409 | get_if_condition(IsPrecise,b(if_elsif(Test,TBody),_,_),Test,Condition,BecomesSuchVars) :- | |
410 | get_operation_enabling_condition1(TBody,Condition,BecomesSuchVars,IsPrecise). | |
411 | ||
412 | :- use_module(bsyntaxtree, [create_implication/3]). | |
413 | disjoin_ifs([],[],_,[]). | |
414 | disjoin_ifs([Test|TT],[EnableCond|TC],NegSoFar,[Res1|TR]) :- | |
415 | append(NegSoFar,[Test],L), | |
416 | conjunct_predicates(L,BranchTest), | |
417 | create_implication(BranchTest,EnableCond,Res1), % ELSEIF Test THEN Body ... ---> NegSoFar & Test => EnableCond | |
418 | create_negation(Test,NTest), | |
419 | append(NegSoFar,[NTest],NegSoFar1), % add negation of test as additional test for rest | |
420 | disjoin_ifs(TT,TC,NegSoFar1,TR). | |
421 | ||
422 | ||
423 | % for a list of substitutions: get enabling conditions and disjoin them | |
424 | get_disjunction_of_enabling_conditions(ListOfWhens,Res,BecomesSuchVars,IsPrecise) :- | |
425 | get_texpr_exprs(ListOfWhens,ListOfSelectWhens), | |
426 | maplist(get_operation_enabling_condition3(IsPrecise),ListOfSelectWhens,Res1,BecomesSuchVars1), | |
427 | ~~mnf(disjunct_predicates(Res1,Res)), | |
428 | append(BecomesSuchVars1,BecomesSuchVars). | |
429 | get_operation_enabling_condition3(Precise,Exp,Res,BV) :- get_operation_enabling_condition2(Exp,Res,BV,Precise). | |
430 | ||
431 | definitely_not_empty(bool_set,_). | |
432 | definitely_not_empty(integer_set(_),_). | |
433 | definitely_not_empty(identifier(X),set(global(X))). | |
434 | definitely_not_empty(string_set,_). | |
435 | ||
436 | ||
437 | ||
438 | % get operation enabling condition in context of an event-b action list: | |
439 | get_operation_enabling_for_event_b_actions([],Res,Res,[],_Precise). | |
440 | get_operation_enabling_for_event_b_actions([H|T],InRes,OutRes,BecomesSuchVars,IsPrecise) :- | |
441 | get_operation_enabling_condition1(H,ResH,HBecomesSuchVars,IsPrecise), | |
442 | ~~mnf(conjunct_predicates([InRes,ResH],IntRes)), | |
443 | get_operation_enabling_for_event_b_actions(T,IntRes,OutRes,TBecomesSuchVars,IsPrecise), | |
444 | append(HBecomesSuchVars,TBecomesSuchVars,BecomesSuchVars). | |
445 | ||
446 | % --------------- | |
447 | :- use_module(bmachine,[b_top_level_operation/1]). | |
448 | % LTSMIN style guards: a guard that does not depend on parameters | |
449 | get_operation_propositional_guards(OpName,Guards,RestBody) :- | |
450 | b_top_level_operation(OpName), | |
451 | b_get_machine_operation_for_animation(OpName,TResults,TParameters,TBody,_OType,true), % requires bmachine to be precompiled | |
452 | get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody). | |
453 | ||
454 | :- use_module(translate,[print_bexpr/1]). | |
455 | % the following can be called directly; does not require bmachine to be pre-compiled | |
456 | get_operation_propositional_guards(OpName,TResults,TParameters,TBody,Guards,RestBody) :- | |
457 | get_texpr_ids(TParameters,Ids1), | |
458 | get_texpr_ids(TResults,Ids2), | |
459 | append(Ids1,Ids2,Ids), sort(Ids,Parameters), | |
460 | get_operation_guards_aux(TBody,Parameters,top,Guards,RestBody), | |
461 | (debug:debug_mode(off) -> true | |
462 | ; format('OPERATION Guard Splitting ~w (~w)~n',[OpName,Parameters]), | |
463 | print('LTSMin Guards: '), maplist(print_bexpr,Guards),nl, | |
464 | print('LTSMin Body: '), translate:print_subst(RestBody),nl,nl | |
465 | ). | |
466 | ||
467 | :- use_module(bsyntaxtree, [conjunction_to_list/2,find_identifier_uses/3]). | |
468 | ||
469 | ||
470 | get_operation_guards_aux(Subst,Parameters,Top,Guards,OpBody) :- | |
471 | get_guards(Subst,Top,TIds,Guard,InnerBody,Infos), | |
472 | get_texpr_ids(TIds,Ids), sort(Ids,NewIds), | |
473 | ord_union(Parameters,NewIds,Parameters2), | |
474 | !, | |
475 | get_parameter_independent_guards(Guard,Parameters2,Indep,Dep), | |
476 | (Dep = [] | |
477 | -> OpBody = InnerOpBody % no need to keep b | |
478 | ; conjunct_predicates(Dep,DepCond), | |
479 | 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) | |
480 | ), | |
481 | get_operation_guards_aux(InnerBody,Parameters2,inner,InnerGuards,InnerOpBody), | |
482 | append(Indep,InnerGuards,Guards). | |
483 | ||
484 | get_operation_guards_aux(b(rlevent(Name,Sect,Status,Params,EvGuard,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info), | |
485 | Parameters,_,Guards,OpBody) :- !, | |
486 | get_parameter_independent_guards(EvGuard,Parameters,InDepGuards,Dep), | |
487 | (get_variant_pred(Status,VariantPred) | |
488 | -> %print(op_variant(_Name)),nl,translate:print_bexpr(VariantPred),nl, | |
489 | % 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 | |
490 | % TO DO: check if we need to add the witnesses as well ! | |
491 | Guards = [VariantPred|InDepGuards] | |
492 | ; Guards = InDepGuards), | |
493 | conjunct_predicates(Dep,DepG), | |
494 | OpBody = b(rlevent(Name,Sect,Status,Params,DepG,Theorems,Act,VWit,PWit,Unmod,AbsEvts),subst,Info). | |
495 | get_operation_guards_aux(TB,_,_,[],TB). | |
496 | ||
497 | ||
498 | :- use_module(bsyntaxtree, [safe_create_texpr/3]). | |
499 | % we integrate the Variant check into the guard to ensure the correct read matrix is produced | |
500 | % currently the Variant is checked upon event entry and for convergent events upon exit for decrease | |
501 | % in principle this should be more of an assertion_predicate or assertion_expression | |
502 | get_variant_pred(b(Status,status,_),Res) :- get_variant_pred_aux(Status,Res). | |
503 | get_variant_pred_aux(anticipated(Variant),Res) :- NATURAL = b(integer_set('NATURAL'),set(integer),[]), | |
504 | safe_create_texpr(member(Variant,NATURAL),pred,Res). | |
505 | get_variant_pred_aux(convergent(Variant),Res) :- NATURAL1 = b(integer_set('NATURAL1'),set(integer),[]), | |
506 | safe_create_texpr(member(Variant,NATURAL1),pred,Res). | |
507 | ||
508 | ||
509 | get_guards(b(precondition(Guard,TBody),subst,Info), top, [],Guard, TBody, Info) :- | |
510 | preferences:get_preference(treat_outermost_pre_as_select,true). | |
511 | get_guards(b(select([b(select_when(Guard, TBody),subst,_Info1)]),subst,Info2), _, [],Guard, TBody, Info2). | |
512 | % TO DO: for ANY try and extract propositional parts, e.g., for ANY pp WHERE pp:1..xx & z=1/yy THEN … | |
513 | get_guards(b(any(TIds,Guard,TBody),subst,Info),_, TIds,Guard,TBody,Info). | |
514 | ||
515 | ||
516 | construct_select([],Guard,TBody, Infos, Res) :- !, | |
517 | Res = b(select([b(select_when(Guard, TBody),subst,Infos)]),subst,Infos). | |
518 | construct_select(TIds,Guard,TBody,Infos, b(any(TIds,Guard,TBody),subst,Infos)). | |
519 | ||
520 | ||
521 | get_parameter_independent_guards(Guard,Parameters,Indep,Dep) :- | |
522 | conjunction_to_list(Guard,Gs), | |
523 | l_get_parameter_independent_guards(Gs,Parameters,at_front,Indep,Dep). | |
524 | ||
525 | :- use_module(library(ordsets)). | |
526 | :- use_module(bsyntaxtree,[always_well_defined/1]). | |
527 | l_get_parameter_independent_guards([],_,_,[],[]). | |
528 | l_get_parameter_independent_guards([G|Gs],Parameters,AtFront,Indep,Dep) :- | |
529 | find_identifier_uses(G,[],Ids), | |
530 | ((ord_disjoint(Ids,Parameters), | |
531 | (AtFront=at_front -> true ; always_well_defined(G))) | |
532 | -> Indep=[G|I1], Dep=D1, AtFront1=AtFront | |
533 | ; Indep=I1, Dep=[G|D1], | |
534 | AtFront1=not_at_front % we have skipped one guard; the next guard is not guaranteed to be at the front (relevant for well-definedness) | |
535 | ), | |
536 | l_get_parameter_independent_guards(Gs,Parameters,AtFront1,I1,D1). | |
537 | ||
538 | % ----------------------------------------- | |
539 | ||
540 | :- use_module(library(timeout)). | |
541 | ||
542 | ||
543 | nr_of_conjuncts(Pred,Nr) :- | |
544 | is_a_conjunct(Pred,LHS,RHS),!, | |
545 | nr_of_conjuncts(LHS,NrL), | |
546 | nr_of_conjuncts(RHS,NrR), | |
547 | Nr is NrL+NrR. | |
548 | nr_of_conjuncts(_,1). | |
549 | ||
550 | :- volatile last_debug_info/2. | |
551 | :- dynamic last_debug_info/2. | |
552 | b_debug_properties2(Pred,Constants,GlobalState,TotalNr,AllowTimeout) :- | |
553 | create_texpr(truth,pred,[b_debug_properties],Truth), | |
554 | retractall(last_debug_info(_,_)), assert(last_debug_info(Constants,GlobalState)), | |
555 | (b_debug_find_first_unsat_property(Pred,Truth,Constants,GlobalState,TotalNr,AllowTimeout) | |
556 | -> print('ALL PROPERTIES SATISFIABLE'),nl | |
557 | ; true % get_preference(debug_try_minimise,false) -> true ; b_find_unsat_core(Constants,GlobalState) | |
558 | ). | |
559 | ||
560 | b_find_unsat_core :- /* assumes that b_debug_properties was run before */ | |
561 | % b_machine_has_constants_or_properties, | |
562 | % b_get_machine_constants(TypedConstants), | |
563 | % b_get_properties_from_machine(Properties),!, | |
564 | % get_adapted_properties(TypedConstants,_AProperties,ATypedConstants), | |
565 | %b_find_unsat_core(ATypedConstants,[]). | |
566 | last_debug_info(Constants,GlobalState), b_find_unsat_core(Constants,GlobalState). | |
567 | b_find_unsat_core(Constants,GlobalState) :- | |
568 | print('TRYING TO MINIMISE UNSATISFIABLE PROPERTIES'),nl, | |
569 | (last_checked_solution(_,Time) | |
570 | -> print(' Time for last solution in ms: '), print(Time), nl ; true), | |
571 | findall(P,checked_property(P),SatProps), | |
572 | (failed_property(FailProp,USTime) -> true | |
573 | ; time_out_property(FailProp,USTime) -> true | |
574 | ; add_error_fail(b_find_unsat_core,'No failed or timed-out property:',SatProps)), | |
575 | print(' Time for unsatisfiable conjuncts in ms: '), print(USTime), nl, | |
576 | append(SatProps,[FailProp],Props), | |
577 | length(SatProps,SL), | |
578 | b_debug_try_remove_props(SatProps,Props,[],Constants,GlobalState,1,SL). | |
579 | % TO DO: partition into components; try removing compnents without FailProp | |
580 | ||
581 | b_debug_try_remove_props([],_,_,_,_,_,_) :- !. | |
582 | b_debug_try_remove_props([],_,_,TypedConstants,GlobalState,Count,_) :- !, % for debug | |
583 | format('~nFINISHED (~w); CHECKING CORE~n',[Count]), | |
584 | get_unsat_core(Core), | |
585 | nl,translate:print_bexpr(Core),nl, | |
586 | (timeout_fast_check_property(unsat,Core,TypedConstants,_,GlobalState,TimeOutResC) -> true | |
587 | ; TimeOutResC = 'UNSAT'), | |
588 | format('~nCORE RESULT: ~w~n',[TimeOutResC]). | |
589 | b_debug_try_remove_props([H|TSat],[H|TUnsat],Required,TypedConstants,GlobalState,Count,Total) :- | |
590 | append(Required,TSat,ConjunctsWithoutH), | |
591 | conjunct_predicates(ConjunctsWithoutH,SatPred), | |
592 | translate_bexpression(H,PT), | |
593 | format('~nCHECKING REMOVAL(~w/~w) OF: ~w~n',[Count,Total,PT]), | |
594 | (timeout_fast_check_property(sat,SatPred,TypedConstants,Sol,GlobalState,TimeOutResSat) | |
595 | -> (\+ is_time_out_result(TimeOutResSat) | |
596 | -> append(Required,TUnsat,ConjunctsWithoutH2), | |
597 | conjunct_predicates(ConjunctsWithoutH2,UnsatPred), | |
598 | ((timeout_fast_check_property(unsat,UnsatPred,TypedConstants,_,GlobalState,TimeOutRes), | |
599 | print(res(TimeOutRes)),nl, | |
600 | (is_time_out_result(TimeOutRes) -> \+ time_out_property(_,_) ; true) | |
601 | ) | |
602 | -> print('Required for inconsistency : '), print(TimeOutRes),nl, | |
603 | append(Required,[H],NewRequired) | |
604 | ; /* H is not required for inconsistency/timeout */ | |
605 | print('NOT required for INCONSISTENCY !'),nl, | |
606 | % print_bexpr(UnsatPred),nl, | |
607 | Required=NewRequired, | |
608 | % TO DO: update found solution | |
609 | (retract(last_checked_solution(_,LastTime)) -> true | |
610 | ; print('*** Could not remove last_checked_solution'),nl, | |
611 | preferences:get_computed_preference(debug_time_out,LastTime) | |
612 | ), | |
613 | assert(last_checked_solution(Sol,LastTime)), | |
614 | (retract(checked_property(H)) -> true | |
615 | ; print('*** Could not remove checked_property: '), print(H),nl | |
616 | ) | |
617 | ) | |
618 | ; print('Required for efficiency'),nl, | |
619 | append(Required,[H],NewRequired) | |
620 | ) | |
621 | ; nl,print('*** INTERNAL ERROR: FAILED'),nl,nl, | |
622 | append(Required,[H],NewRequired) | |
623 | ), | |
624 | C1 is Count+1, | |
625 | b_debug_try_remove_props(TSat,TUnsat,NewRequired,TypedConstants,GlobalState,C1,Total). | |
626 | ||
627 | b_debug_find_first_unsat_property(Pred,Rest,Constants,GlobalState,TotalNr,AllowTimeout) :- | |
628 | is_a_conjunct(Pred,LHS,RHS),!, | |
629 | (b_debug_find_first_unsat_property(LHS,Rest,Constants,GlobalState,TotalNr,AllowTimeout) | |
630 | -> conjunct_predicates([Rest,LHS],Rest2), | |
631 | b_debug_find_first_unsat_property(RHS,Rest2,Constants,GlobalState,TotalNr,AllowTimeout) | |
632 | ; fail | |
633 | ). | |
634 | b_debug_find_first_unsat_property(Prop,Rest,TypedConstants,GlobalState,TotalNr,AllowTimeout) :- | |
635 | nl,nl,flush_output(user), | |
636 | conjunct_predicates([Rest,Prop],Pred), | |
637 | (retract(cur_conjunct_nr(CurNr)) -> true ; CurNr=1), CurNrP1 is CurNr+1, | |
638 | assert(cur_conjunct_nr(CurNrP1)), | |
639 | translate_bexpression(Prop,PT), | |
640 | format('~nCHECKING (~w/~w) OF: ~w~n',[CurNr,TotalNr,PT]), | |
641 | statistics(runtime,[Start,_]), | |
642 | (timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) | |
643 | -> statistics(runtime,[Stop,_]), Time is Stop - Start, | |
644 | print_time(TimeOutRes,Time), | |
645 | format('~nINFO: ~w~n~n',[TimeOutRes]), | |
646 | (((\+ last_checked_solution(_,_) % we haven't found a solution yet | |
647 | ; AllowTimeout=allow_timeout), | |
648 | is_time_out_result(TimeOutRes)) | |
649 | -> assert(time_out_property(Prop,Time)) | |
650 | ; is_time_out_failure(TimeOutRes) | |
651 | -> assert(time_out_property(Prop,Time)) | |
652 | ; | |
653 | assert_checked_property(Prop,ConstantsState,Time) % could also be timeout | |
654 | ) | |
655 | ; statistics(runtime,[Stop,_]), Time is Stop - Start, | |
656 | assert(failed_property(Prop,Time)), | |
657 | print('No Solution Found !! ('),print(Time), print(' ms)'),nl, flush_output(user), | |
658 | %print_bexpr(Pred),nl, | |
659 | fail | |
660 | ). | |
661 | ||
662 | is_time_out_failure(virtual_time_out(failure_enumeration_warning(_,_,_,_,_))). | |
663 | ||
664 | print_time(TimeOutRes,Time) :- is_time_out_result(TimeOutRes),!, | |
665 | (TimeOutRes=virtual_time_out(_) -> print('VIRTUAL ') ; true), | |
666 | print('TIMEOUT !! ('),print(Time), print(' ms)'),nl, flush_output(user). | |
667 | print_time(_TimeOutRes,Time) :- | |
668 | print('OK ('), print(Time), print(' ms)'), flush_output(user). | |
669 | ||
670 | ||
671 | last_unsat_time(Time) :- time_out_property(_,Time) -> true ; failed_property(_,Time). | |
672 | ||
673 | set_fast_unsat_core(T) :- retractall(fast_unsat_core), | |
674 | (T==fast -> assert(fast_unsat_core) ; true). | |
675 | :- dynamic fast_unsat_core/0. | |
676 | fast_unsat_core. | |
677 | ||
678 | additional_time(301). % additional time given to account for variations in solving | |
679 | %additional_time(1301). | |
680 | ||
681 | get_timeout(sat,DebugTimeOut) :- | |
682 | last_checked_solution(_,LTime), | |
683 | !, | |
684 | additional_time(AT), | |
685 | DebugTimeOut is LTime+AT. | |
686 | get_timeout(unsat,DebugTimeOut) :- | |
687 | last_unsat_time(USTime), | |
688 | last_checked_solution(_,LSTime), | |
689 | (fast_unsat_core -> TT is min(USTime,LSTime) ; TT is max(USTime,LSTime)), | |
690 | !, | |
691 | additional_time(AT), | |
692 | DebugTimeOut is TT+AT. | |
693 | get_timeout(S,DebugTimeOut) :- print('*** Could not get TimeOut : '), print(S),nl, | |
694 | preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 1. | |
695 | ||
696 | ||
697 | timeout_fast_check_property(ExpectSat,Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :- | |
698 | get_timeout(ExpectSat,DebugTimeOut), | |
699 | % print(time_out_value(DebugTimeOut)),nl, | |
700 | % print_bexpr(Pred),nl, | |
701 | statistics(runtime,[Start,_]), | |
702 | timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes), | |
703 | statistics(runtime,[Stop,_]), Time is Stop - Start, print(time(Time)),nl, | |
704 | (is_time_out_result(TimeOutRes) -> print(time_out_occurred(Time,DebugTimeOut)),nl, | |
705 | (debug:debug_mode(on) -> print_bexpr(Pred),nl ; true) | |
706 | ; true). | |
707 | ||
708 | timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :- | |
709 | preferences:get_computed_preference(debug_time_out,DebugTimeOut), | |
710 | timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes), | |
711 | % Note: will translate failure with enumeration warning into virtual_timeout; see is_time_out_failure above | |
712 | format('~nCHECKING RESULT is: ~w~n',[TimeOutRes]). | |
713 | ||
714 | timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState, DebugTimeOut,TimeOutRes) :- | |
715 | on_exception(E, | |
716 | time_out_with_enum_warning_one_solution( | |
717 | b_check_property_satisfiable(Pred,TypedConstants,ConstantsState,GlobalState), | |
718 | DebugTimeOut,TimeOutRes), | |
719 | TimeOutRes = virtual_time_out(exception(E))). % probably CLPFD overflow | |
720 | ||
721 | ||
722 | assert_checked_property(P,ConstantsState,Time) :- | |
723 | assert(checked_property(P)), | |
724 | (var(ConstantsState) -> print('NO SOLUTION'),nl | |
725 | ; retractall(last_checked_solution(_,_)), | |
726 | assert(last_checked_solution(ConstantsState,Time))). | |
727 | ||
728 | :- use_module(kernel_waitflags). | |
729 | :- use_module(b_enumerate). | |
730 | ||
731 | % TO DO: call something which will use predicate_components | |
732 | ||
733 | b_check_property_satisfiable(Properties,TypedConstants,ConstantsState,GlobalState) :- | |
734 | b_ast_cleanup:clean_up_pred(Properties,[],Pred), | |
735 | set_up_typed_localstate(TypedConstants,_FreshVars,TypedVals,[],ConstantsState,positive), | |
736 | b_interpreter_components:reset_component_info(false), | |
737 | append(ConstantsState,GlobalState,State), | |
738 | b_interpreter_components:b_trace_test_components(Pred,State,TypedVals), | |
739 | \+ b_interpreter_components:unsat_component_exists. | |
740 | ||
741 | ||
742 | ||
743 | % ------------------------------------ | |
744 | % This code might be obsolete - replaced by unsat_cores module | |
745 | % ------------------------------------ | |
746 | ||
747 | % NEW FIND UNSAT CORE | |
748 | ||
749 | % Assumes predicate unsatisfiable without time-out to start with | |
750 | % not yet finished | |
751 | ||
752 | %:- use_module(bsyntaxtree, [conjunction_to_list/2,conjunct_predicates/2,find_identifier_uses/3]). | |
753 | ||
754 | % :- use_module(predicate_debugger), predicate_debugger:unsat_core_goal. | |
755 | %unsat_core_goal :- | |
756 | % bmachine:b_get_machine_goal(Goal), | |
757 | % unsat_core(Goal). | |
758 | %unsat_core(FullPred) :- | |
759 | % get_parameters(FullPred,Params,Conj), | |
760 | % get_current_state('@PRED',CurID,CurBState), | |
761 | % set_error_context(unsat_core(CurID)), | |
762 | % conjunction_to_list(Conj,List), | |
763 | % create_texpr(truth,pred,[],T), append(List,[T],ListT), % so that we also check full property | |
764 | % unsat_core_list(ListT,[],Params,CurBState). | |
765 | ||
766 | %remove_last(List,H,NewList) :- append(NewList,[H],List). | |
767 | ||
768 | %unsat_core_list([],List,_Parameters,_CurBState) :- | |
769 | % conjunct_predicates(List,Pred), | |
770 | % print('UNSAT CORE: '), translate:print_bexpr(Pred),nl, | |
771 | % find_identifier_uses(Pred,[],Used), | |
772 | % print('USED IDENTIFIERS: '), print(Used),nl. | |
773 | %unsat_core_list(List1,List2,Parameters,CurBState) :- | |
774 | % remove_last(List1,H,NewList1), | |
775 | % print('Checking removal of : '), translate:print_bexpr(H),nl, | |
776 | % append(NewList1,List2,List), | |
777 | % conjunct_predicates(List,Pred), | |
778 | % print(' --> '),translate:print_bexpr(Pred),nl, | |
779 | % preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 3, | |
780 | % tools:start_ms_timer(TIMER), | |
781 | % (time_out(b_check_property_satisfiable(Pred,Parameters,_ConstantsState,CurBState), | |
782 | % DebugTimeOut,TimeOutRes) | |
783 | % -> (TimeOutRes=time_out -> print('*** TIME OUT ***') ; print(' *** SAT ***')),nl, | |
784 | % tools:stop_ms_timer(TIMER), | |
785 | % unsat_core_list(NewList1,[H|List2],Parameters,CurBState) | |
786 | % ; print(' --- STILL UNSAT (REMOVING CONJUNCT) ---'),nl, | |
787 | % tools:stop_ms_timer(TIMER), | |
788 | % unsat_core_list(NewList1,List2,Parameters,CurBState) | |
789 | % ). | |
790 |