1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(predicate_evaluator,[tcltk_analyse_goal/1, tcltk_analyse_goal/2, |
6 | | tcltk_analyse_invariant/2, |
7 | | tcltk_analyse_assertions/2, tcltk_analyse_assertions/3, |
8 | | tcltk_analyse_properties/2, check_summary_all_true/1, |
9 | | tcltk_analyse_deadlock/2, |
10 | | %get_analyse_error_span_linecol/4, |
11 | | |
12 | | % a way to customize what is done with false/unknown conjuncts |
13 | | reset_conjunct_error_hook/0, register_conjunct_error_hook/1, |
14 | | register_conjunct_register_error_span/0 % conjuncts which are not true are registered as error spans |
15 | | ]). |
16 | | |
17 | | % a simple textual analysis of the conjuncts of a predicate |
18 | | |
19 | | :- use_module(tools). |
20 | | |
21 | | :- use_module(module_information,[module_info/2]). |
22 | | :- module_info(group,misc). |
23 | | :- module_info(description,'Various tools to analyse conjunctions of predicates textually (along with statistics).'). |
24 | | |
25 | | :- use_module(bmachine). |
26 | | :- use_module(error_manager). |
27 | | :- use_module(translate). |
28 | | :- use_module(debug). |
29 | | :- use_module(preferences,[get_computed_preference/2,get_preference/2,get_time_out_preference_with_factor/2]). |
30 | | :- use_module(state_space,[current_state_corresponds_to_setup_constants_b_machine/0, |
31 | | current_state_corresponds_to_fully_setup_b_machine/0]). |
32 | | |
33 | | :- use_module(b_interpreter,[b_generate_for_all_list_domain_nolwf/8]). |
34 | | :- use_module(b_state_model_check,[get_unsorted_all_guards_false_pred/1]). |
35 | | :- use_module(kernel_waitflags,[ground_wait_flags/1,init_wait_flags/1]). |
36 | | |
37 | | |
38 | | current_b_state_with_all_constants_valued :- |
39 | | (current_state_corresponds_to_setup_constants_b_machine -> true |
40 | | ; \+ b_machine_has_constants). % also allow analysis if we have no constants (but possibly properties) |
41 | | |
42 | | tcltk_analyse_goal(List) :- tcltk_analyse_goal(List,_). |
43 | | tcltk_analyse_goal(list(List),Summary) :- |
44 | | current_b_state_with_all_constants_valued, |
45 | | b_get_machine_goal(Goal),!, |
46 | | b_analyse_boolean_expression(Goal,false,List,Summary). |
47 | | tcltk_analyse_goal(list(['Cannot evaluate GOAL yet.\nSetup constants first.\n\n'|List]),Summary) :- |
48 | | b_get_machine_goal(Goal),!, |
49 | | get_conjuncts(Goal,List,undefined), unknown_summary(1,Summary). |
50 | | tcltk_analyse_goal(list(['Cannot find GOAL DEFINITION (must be a predicate).\n']),Summary) :- |
51 | | unknown_summary(1,Summary). |
52 | | |
53 | | tcltk_analyse_invariant(list(List),Summary) :- |
54 | | current_state_corresponds_to_fully_setup_b_machine,!, |
55 | | b_get_invariant_from_machine(Invariant), |
56 | | preferences:get_preference(partition_predicates,Partition), |
57 | | b_analyse_boolean_expression(Invariant,Partition,List,Summary). |
58 | | tcltk_analyse_invariant(list(['Cannot evaluate invariant yet.\nInitialise machine first.\n\n'|List]),Summary) :- |
59 | | b_get_invariant_from_machine(Invariant), |
60 | | get_conjuncts(Invariant,List,undefined), |
61 | | length(List,TL), unknown_summary(TL,Summary). |
62 | | |
63 | | :- use_module(specfile,[animation_mode/1, csp_with_bz_mode/0]). |
64 | | tcltk_analyse_assertions(List,Summary) :- tcltk_analyse_assertions(all,List,Summary). |
65 | | tcltk_analyse_assertions(_ALL,list(['CSP Assertions'|CA]),Summary) :- (animation_mode(cspm) ; csp_with_bz_mode),!, |
66 | | user:tcltk_check_csp_assertions(CA,Summary), print(CA),nl, print(Summary),nl. |
67 | | tcltk_analyse_assertions(all,list(['This Machine has no ASSERTIONS.']),Summ) :- |
68 | | b_get_dynamic_assertions_from_machine([]),b_get_static_assertions_from_machine([]),!,empty_summary(Summ). |
69 | | tcltk_analyse_assertions(main,list(['The Main Machine has no ASSERTIONS.']),Summ) :- |
70 | | b_main_machine_has_no_assertions, |
71 | | !,empty_summary(Summ). |
72 | | tcltk_analyse_assertions(ALL,list(List),Summary) :- |
73 | ? | current_state_corresponds_to_fully_setup_b_machine,!, |
74 | | %conjunct_predicates(Ass,BExpr) |
75 | ? | b_get_assertions(ALL,static,SAss), |
76 | ? | println_silent('Checking Static Assertions'), |
77 | | % translate:nested_print_bexpr(SAss), |
78 | ? | b_analyse_boolean_expression(SAss,false,SList,SSummary), |
79 | ? | b_get_assertions(ALL,dynamic,DAss), |
80 | ? | println_silent('Checking Dynamic Assertions'), |
81 | ? | b_analyse_boolean_expression(DAss,false,DList,DSummary), |
82 | ? | combine_summary(SSummary,DSummary,Summary), |
83 | ? | combine_static_dynamic_result(SList,DList,List). |
84 | | tcltk_analyse_assertions(ALL,list(ListRes),Summary) :- |
85 | ? | current_b_state_with_all_constants_valued, |
86 | ? | b_get_assertions(ALL,static,Ass),Ass\=[],!, |
87 | ? | b_analyse_boolean_expression(Ass,false,SList,SSummary), |
88 | ? | b_get_assertions(ALL,dynamic,DynAss), |
89 | ? | (DynAss=[] -> ListRes = List, Summary = SSummary |
90 | | ; ListRes = ['Only evaluating STATIC ASSERTIONS.\nInitialise machine to evaluate other ASSERTIONS.\n\n'|List], |
91 | | (length(DynAss,Len) -> true ; Len=1), |
92 | | unknown_summary(Len,US),combine_summary(US,SSummary,Summary) |
93 | | ), |
94 | ? | get_assertions_as_undefined(ALL,dynamic,DList), |
95 | ? | combine_static_dynamic_result(SList,DList,List). |
96 | | tcltk_analyse_assertions(ALL,list(['Cannot evaluate assertions yet.\nInitialise machine first.\n\n'|List]),Summary) :- |
97 | | print('*** Cannot evaluate ASSERTIONS\nSPECIFICATION not initialised.'),nl, |
98 | | get_assertions_as_undefined(ALL,static,SList), |
99 | | get_assertions_as_undefined(ALL,dynamic,DList), |
100 | | length(SList,SL), length(DList,DL), TL is SL+DL, unknown_summary(TL,Summary), |
101 | | combine_static_dynamic_result(SList,DList,List). |
102 | | |
103 | | :- use_module(library(lists),[maplist/3]). |
104 | | get_assertions_as_undefined(ALL,SD,List) :- |
105 | | b_get_assertions(ALL,SD,Ass), |
106 | | flatten_conjunction(Ass,FAss,[]), |
107 | | maplist(get_as_undefined,FAss,List). |
108 | | % (Ass=[] -> List=[] ; conjunct_predicates(Ass,BExpr),get_conjuncts(BExpr,List,undefined)). |
109 | | |
110 | | get_as_undefined(Conjunct,Translation) :- translate_conj_status(Conjunct,undefined,false,Translation). |
111 | | |
112 | | combine_static_dynamic_result([],L,L). |
113 | | combine_static_dynamic_result(L,[],L). |
114 | | combine_static_dynamic_result(S,D,List) :- |
115 | | List = ['STATIC ASSERTIONS:\n'|List0], |
116 | | append(S,['DYNAMIC ASSERTIONS:\n'|D],List0). |
117 | | |
118 | | unknown_summary(Nr,[total/Nr,unknown/Nr,unknown_after_expansion/Nr]). |
119 | | combine_summary([],S,S). |
120 | | combine_summary([K/V|T],S,R) :- update(S,K,V,S2), combine_summary(T,S2,R). |
121 | | update([],K,V,[K/V]). |
122 | | update([K1/V1|T],K1,V2,[K1/NV|T]) :- !,NV is V1+V2. |
123 | | update([K1/V1|T],K,V,[K1/V1|NT]) :- update(T,K,V,NT). |
124 | | |
125 | | tcltk_analyse_deadlock(list(List),Summary) :- current_state_corresponds_to_fully_setup_b_machine,!, |
126 | | b_state_model_check:get_unsorted_all_guards_false_pred(BExpr), |
127 | | b_analyse_boolean_expression(BExpr,false,List,Summary). |
128 | | tcltk_analyse_deadlock(list(['Cannot evaluate deadlock yet.\nInitialise machine first.\n\n'|List]),[]) :- |
129 | | b_state_model_check:get_unsorted_all_guards_false_pred(BExpr), |
130 | | get_conjuncts(BExpr,List,undefined). |
131 | | |
132 | | tcltk_analyse_properties(list([Res]),[]) :- |
133 | | b_get_properties_from_machine(b(truth,_,_)),!, |
134 | | (b_machine_has_constants |
135 | | -> Res = 'This Machine has only typing information in the PROPERTIES.' |
136 | | ; Res = 'This Machine has no PROPERTIES clause.' |
137 | | ). |
138 | | tcltk_analyse_properties(list(List),Summary) :- |
139 | | current_b_state_with_all_constants_valued, |
140 | | !, |
141 | | b_get_properties_from_machine(Prop), |
142 | | preferences:get_preference(partition_predicates,Partition), |
143 | | b_analyse_boolean_expression(Prop,Partition,List,Summary). |
144 | | tcltk_analyse_properties(list(['Cannot evaluate properties yet.\nSet up constants first.\n\n'|List]),Summary) :- |
145 | | b_get_properties_from_machine(Prop), |
146 | | (preferences:get_preference(partition_predicates,false) |
147 | | -> get_conjuncts(Prop,List,undefined), length(List,NrConjuncts) |
148 | | ; bsyntaxtree:predicate_components(Prop,Components), |
149 | | findall(CList, |
150 | | (member(component(CP,_CompVars),Components), |
151 | | get_conjuncts(CP,CList,undefined)), CCList), |
152 | | flatten_comp(CCList,List,NrConjuncts) |
153 | | ), |
154 | | unknown_summary(NrConjuncts,Summary). |
155 | | |
156 | | flatten_comp([],[],0). |
157 | | flatten_comp([H|T],['COMPONENT:\n'|Res],NrConjuncts) :- |
158 | | flatten_comp(T,TR,TNr), |
159 | | length(H,LH), NrConjuncts is LH+TNr, |
160 | | append(H,TR,Res). |
161 | | |
162 | | |
163 | | %:- dynamic conj_nr/1. |
164 | | %conj_nr(1). |
165 | | %get_and_inc_conj_nr(X) :- retract(conj_nr(X)), X1 is X+1, assert(conj_nr(X1)). |
166 | | %reset_conj_nr :- retractall(conj_nr(_)), assert(conj_nr(1)). |
167 | | |
168 | | |
169 | | % check if a summary report is all true |
170 | | check_summary_all_true(L) :- |
171 | | member(total_after_expansion/Nr,L), member(true_after_expansion/Nr,L), |
172 | | member(false/0,L), member(unknown/0,L), member(timeout/0,L). |
173 | | |
174 | | empty_summary([total/0, total_after_expansion/0, |
175 | | true/0, true_after_expansion/0, false/0, false_after_expansion/0, |
176 | | unknown/0, unknown_after_expansion/0, timeout/0, runtime/0, enum_warning/0]). |
177 | | :- use_module(specfile, [current_b_expression/1]). |
178 | | :- use_module(state_space, [current_state_id/1]). |
179 | | get_current_b_expression(S) :- |
180 | | (current_b_expression(S) -> true |
181 | | ; current_state_id(root), \+ b_machine_has_constants -> S = [] |
182 | | ; add_internal_error('Could not get B state for analysis',get_current_b_expression(S)),S=[] |
183 | | ). |
184 | | b_analyse_boolean_expression(VAR,P,L,S) :- var(VAR),!, |
185 | | add_internal_error('Illegal call: ',b_analyse_boolean_expression(VAR,P,L,S)), |
186 | | S=[unknown/1]. |
187 | | b_analyse_boolean_expression(BExpr,Partition,List, |
188 | | [total/NrTotal, total_after_expansion/NrTotalExpanded, |
189 | | true/NrTrue, true_after_expansion/NrTrueExpanded, |
190 | | false/NrFalse, false_after_expansion/NrFalseExpanded, |
191 | | unknown/NrUnknown, unknown_after_expansion/NrUnknownExpanded, |
192 | | timeout/NrTimeout, runtime/TotalTime, enum_warning/NrEnumWarning]) :- |
193 | | get_current_b_expression(RealCurState), |
194 | | %reset_conj_nr, |
195 | | statistics(walltime,[CurTime,_]), /* get current time in ms */ |
196 | | b_analyze_all_sub_conjuncts(Partition,BExpr, RealCurState, CList), |
197 | | statistics(walltime,[CurTime2,_]), /* get current time in ms */ |
198 | | formatsilent('~N=======~NSUMMARY~N=======~N',[]), |
199 | | new_counter(Counter0), |
200 | | l_translate_conjunct_analysis_result(CList,List,none/true,'$_no_model'(none),Counter0,ResCounter), |
201 | | %print_counter(ResCounter), |
202 | | get_counter(total,ResCounter,NrTotal), get_counter(total_after_expansion,ResCounter,NrTotalExpanded), |
203 | | get_counter(true,ResCounter,NrTrue), get_counter(true_after_expansion,ResCounter,NrTrueExpanded), |
204 | | get_counter(false,ResCounter,NrFalse), get_counter(false_after_expansion,ResCounter,NrFalseExpanded), |
205 | | get_counter(unknown,ResCounter,NrUnknown), get_counter(unknown_after_expansion,ResCounter,NrUnknownExpanded), |
206 | | get_counter(timeout,ResCounter,NrTimeout), get_counter(enum_warning,ResCounter,NrEnumWarning), |
207 | | (NrTotal=NrTotalExpanded |
208 | | -> format('~p predicates: ~p TRUE, ~p FALSE, ~p UNKNOWN (~p timeouts)~N',[NrTotal,NrTrue,NrFalse,NrUnknown,NrTimeout]) |
209 | | ; format('~p predicates (~p after expansion): ~p TRUE (~p after expansion), ~p FALSE (~p after expansion), ~p UNKNOWN (~p after expansion) (~p timeouts)~N',[NrTotal,NrTotalExpanded,NrTrue,NrTrueExpanded,NrFalse,NrFalseExpanded,NrUnknown,NrUnknownExpanded,NrTimeout])), |
210 | | TotalTime is CurTime2-CurTime, |
211 | | print(TotalTime), print(' ms to analyse'),nl. |
212 | | |
213 | | :- use_module(bsyntaxtree). |
214 | | |
215 | | b_analyze_all_sub_conjuncts(true,BExpr, RealCurState, CList) :- !, |
216 | | bsyntaxtree:predicate_components(BExpr,Components), % Note: does not support list of conjunctions (as generated by b_get_assertions_from_machine) |
217 | | findall(comp_res(CCList,CompVars), |
218 | | (member(component(CompBExpr,CompVars),Components), |
219 | | analyze_all_conjuncts2(CompBExpr, RealCurState, CCList)),CompRes), |
220 | | flatten_comp_res(CompRes,CList). |
221 | | b_analyze_all_sub_conjuncts(_Partition,BExpr, RealCurState, CList) :- |
222 | | analyze_all_conjuncts2(BExpr, RealCurState, CList). |
223 | | |
224 | | flatten_comp_res([],[]). |
225 | | flatten_comp_res([comp_res(CCList,Vars)|T],Res) :- |
226 | | flatten_comp_res(T,FT), |
227 | | append([vars(Vars)|CCList],FT,Res). |
228 | | |
229 | | analyze_all_conjuncts2(BExpr, RealCurState, CList) :- |
230 | | findall(conj(Nr,Conjunct,Status,EnumWarning,IsExpanded), |
231 | | (%get_and_inc_conj_nr(Nr), print(analysing_conjunct(Nr)),nl, |
232 | | b_analyse_conjunction(BExpr,[],RealCurState,Nr,Conjunct,Status,EnumWarning,IsExpanded) |
233 | | ), |
234 | | CList). |
235 | | |
236 | | %:- use_module(library(codesio)). |
237 | | :- use_module(tools_meta,[translate_term_into_atom/2]). |
238 | | l_translate_conjunct_analysis_result([],[],CurConjNr/CurStatus,_LastModel,Acc,ResAcc) :- |
239 | | flush_cur_status(CurConjNr,CurStatus,Acc,ResAcc). |
240 | | l_translate_conjunct_analysis_result([vars(Vars)|T],Res,CurConjNr/CurStatus,_LastModel,Acc,CRes) :- |
241 | | flush_cur_status(CurConjNr,CurStatus,Acc,Acc1), |
242 | | (Vars=[] -> Res = ['** ISOLATED CONJUNCT **\n'|TT] |
243 | | ; Res = [CS,CV,' **\n'|TT], CS = '** CONJUNCTS OVER IDENTIFIERS:'), |
244 | | translate_term_into_atom(Vars,CV), |
245 | | l_translate_conjunct_analysis_result(T,TT,none/true,'$_no_model'(none),Acc1,CRes). |
246 | | l_translate_conjunct_analysis_result([conj(NextNr,Conjunct,Status,EnumWarning,IsExpanded)|T],TranslationResult,CurConjNr/CurStatus,LastModel,Acc,CRes) :- |
247 | | translate_conjunct(Conjunct,Status,EnumWarning,CS), |
248 | | inc_counter(total_after_expansion,Acc,AA), |
249 | | (EnumWarning==true -> inc_counter(enum_warning,AA,A1) ; AA=A1), |
250 | | ( Status = 'TRUE' -> inc_counter(true_after_expansion,A1,NewAcc) |
251 | | ; Status = timeout_true -> inc_counter(true_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) |
252 | | ; Status = false -> inc_counter(false_after_expansion,A1,NewAcc) |
253 | | ; Status = timeout_false -> inc_counter(false_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) |
254 | | ; Status = both_true_false -> inc_counter(unknown_after_expansion,A1,NewAcc) |
255 | | ; Status = wd_error_true -> inc_counter(unknown_after_expansion,A1,NewAcc) |
256 | | ; Status = wd_error_false -> inc_counter(unknown_after_expansion,A1,NewAcc) |
257 | | ; inc_counter(unknown_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc) |
258 | | ), |
259 | | (call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS) -> true |
260 | | ; add_internal_error('Conjunct error hook failed: ', |
261 | | call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS))), |
262 | | (CurConjNr==NextNr |
263 | | -> combine_status(CurStatus,Status,NewStatus), NewAcc=NewAcc2 % still the same conjunct; combine status |
264 | | ; flush_cur_status(CurConjNr,CurStatus,NewAcc,NewAcc2), |
265 | | convert_status(Status,NewStatus)), |
266 | | ((get_rodin_model_name(Conjunct,NewModel), NewModel \= LastModel) |
267 | | -> TranslationResult = [' * MODEL: ',NewModel,'\n',CS|TT] % show from which model the conjuncts come from |
268 | | ; NewModel = LastModel, TranslationResult = [CS|TT]), |
269 | | l_translate_conjunct_analysis_result(T,TT,NextNr/NewStatus,NewModel,NewAcc2,CRes). |
270 | | |
271 | | flush_cur_status(CurConjNr,CurStatus,Acc,NewAcc2) :- |
272 | | (CurConjNr==none -> Acc=NewAcc2 |
273 | | ; inc_counter(total,Acc,NewAcc1), |
274 | | (CurStatus = true -> inc_counter(true,NewAcc1,NewAcc2) |
275 | | ; CurStatus = false -> inc_counter(false,NewAcc1,NewAcc2) |
276 | | ; inc_counter(unknown,NewAcc1,NewAcc2)) ). |
277 | | |
278 | | combine_status(true,X,R) :- convert_status(X,R). |
279 | | combine_status(false,_,false). |
280 | | combine_status(unknown,false,R) :- !,R=false. |
281 | | combine_status(unknown,_,unknown). |
282 | | |
283 | | convert_status('TRUE',true) :- !. |
284 | | convert_status(timeout_true,true) :- !. |
285 | | convert_status(false,false) :- !. |
286 | | convert_status(timeout_false,false) :- !. |
287 | | convert_status(_,unknown). |
288 | | |
289 | | :- dynamic conjunct_error_hook_pred/1. |
290 | | conjunct_error_hook_pred(default_hook). |
291 | | call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, TranslatedConjunct) :- |
292 | | convert_status(Status,ConvStatus), |
293 | | conjunct_error_hook_pred(Pred), |
294 | | call(Pred,Conjunct,ConvStatus,EnumWarning,IsExpanded, TranslatedConjunct). |
295 | | :- public default_hook/5. |
296 | | default_hook(_,_Status,_,_, _CS). |
297 | | %((Status='TRUE' ; Status = timeout_true) -> print(CS),nl ; true). |
298 | | |
299 | | :- use_module(error_manager,[register_error_span/2]). |
300 | | register_span_hook(Conjunct,ConvStatus,_EnumWarning,_IsExpanded, _TranslatedConjunct) :- |
301 | | %print(status(ConvStatus)),nl, |
302 | | (ConvStatus=true -> true ; register_error_span(predicate_evaluator,Conjunct)). % store positions for Tcl/Tk |
303 | | |
304 | | reset_conjunct_error_hook :- retractall(conjunct_error_hook_pred(_)), assert(conjunct_error_hook_pred(default_hook)). |
305 | | :- meta_predicate register_conjunct_error_hook(5). |
306 | | register_conjunct_error_hook(Pred) :- retractall(conjunct_error_hook_pred(_)), assert(conjunct_error_hook_pred(Pred)). |
307 | | |
308 | | register_conjunct_register_error_span :- register_conjunct_error_hook(register_span_hook). |
309 | | |
310 | | |
311 | | % some utilities to count occurences of certain things: |
312 | | :- use_module(library(assoc)). |
313 | | new_counter(C) :- empty_assoc(C). |
314 | | %reset_counter(Key,C,NC) :- put_assoc(Key,C,0,NC). |
315 | | inc_counter(Key,C,NC) :- (get_assoc(Key,C,Val) -> NewVal is Val+1 ; NewVal =1), |
316 | | put_assoc(Key,C,NewVal,NC). |
317 | | %cond_inc_counter(true,Key,C,NC) :- !, inc_counter(Key,C,NC). |
318 | | %cond_inc_counter(_,_,C,C). |
319 | | get_counter(Key,C,Val) :- (get_assoc(Key,C,Val) -> true ; Val =0). |
320 | | %print_counter(C) :- portray_assoc(C),nl. |
321 | | %get_counter_list(C,L) :- assoc_to_list(C,L). |
322 | | |
323 | | :- use_module(b_interpreter). |
324 | | :- use_module(bsyntaxtree,[is_a_conjunct/3]). |
325 | | |
326 | | % conjunct_ |
327 | | %b_analyse_conjunction(C, LocalState,State,Conjunct,Status,EnumWarning) :- tools_printing:print_term_summary(C),nl,fail. |
328 | | |
329 | | :- use_module(library(lists),[nth1/3]). |
330 | | b_analyse_conjunction(Conj, LocalState,State,Nr,EvConjunct,Status,EnumWarning,IsExpanded) :- |
331 | ? | flatten_conjunction(Conj,ConjList,[]), |
332 | ? | nth1(Nr, ConjList, Conjunct), |
333 | ? | b_analyse_conjunction_nr(Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded). |
334 | | |
335 | | flatten_conjunction([]) --> !, []. |
336 | | flatten_conjunction([H|T]) --> !, flatten_conjunction(H),flatten_conjunction(T). |
337 | | flatten_conjunction(C) --> {is_a_conjunct(C,LHS,RHS)}, |
338 | ? | {\+ do_not_decompose(C)}, % otherwise the user wants to group it |
339 | | !, |
340 | | flatten_conjunction(LHS), flatten_conjunction(RHS). |
341 | | flatten_conjunction(C) --> [C]. |
342 | | |
343 | | do_not_decompose(C) :- bsyntaxtree:get_texpr_labels(C,_),!. % otherwise the user wants to group it |
344 | ? | do_not_decompose(C) :- get_texpr_info(C,Infos), |
345 | ? | member(generated_conjunct,Infos). % the conjunct has been generated, e.g., by b_ast_cleanup |
346 | | |
347 | | :- use_module(tools_meta,[safe_time_out/3]). |
348 | | :- meta_predicate analyse_quick_time_out(0). |
349 | | analyse_quick_time_out(Call) :- |
350 | | get_time_out_preference_with_factor(0.05,DTimeOut), |
351 | | (DTimeOut > 400 -> TO = 400 ; TO = DTimeOut), |
352 | | on_enumeration_warning( |
353 | | safe_time_out(Call,TO,Res), |
354 | | fail), % in case of enumeration warnings: we could not compute all elements of domain |
355 | | \+ is_time_out_result(Res). |
356 | | %analyse_time_out(Call) :- |
357 | | % preferences:get_computed_preference(debug_time_out,DTimeOut), |
358 | | % time_out_with_enum_warning_one_solution(Call,DTimeOut,Res), |
359 | | % \+ is_time_out_result(Res). |
360 | | |
361 | | b_analyse_conjunction_nr(_Nr,b(forall(Parameters,LHS,RHS),pred,Info),LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :- |
362 | ? | IsExpanded=true, |
363 | ? | preferences:get_preference(expand_forall_upto,MaxLenForEpxansion), |
364 | ? | MaxLenForEpxansion>0, |
365 | | % print(generating_for_all_domain(Parameters)),nl, |
366 | ? | analyse_quick_time_out((kernel_waitflags:init_wait_flags(WF), |
367 | | b_interpreter:b_generate_for_all_list_domain_nolwf(Parameters,LHS,RHS,LocalState,State,AllSols,NewRHS,WF), |
368 | | kernel_waitflags:ground_wait_flags(WF))), |
369 | ? | length(AllSols,Len), Len>0, Len=<MaxLenForEpxansion,!, |
370 | ? | (silent_mode(on) -> true ; print('FORALL domain computed: '), translate:print_bexpr(LHS),nl), |
371 | ? | member(ParResult,AllSols), |
372 | | set_up_equality(Parameters,ParResult,EqList), |
373 | | conjunct_predicates(EqList,EqPred), |
374 | | EvConjunct = b(forall(Parameters,EqPred,RHS),pred,Info), |
375 | | (debug_mode(on) -> print('Testing: '), print_bexpr(EvConjunct),nl ; true), |
376 | | set_up_typed_localstate(Parameters,ParResult,_,LocalState,NewLocalState,positive), |
377 | | b_analyse_individual_conjunct(NewRHS,NewLocalState,State,_,Status,EnumWarning). |
378 | | b_analyse_conjunction_nr(_Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :- |
379 | | %debug:debug_println(9,analysing_conjunct_in_component(Nr)), |
380 | | IsExpanded=false, |
381 | | b_analyse_individual_conjunct(Conjunct,LocalState,State,EvConjunct,Status,EnumWarning). |
382 | | |
383 | | set_up_equality([],[],[]). |
384 | | set_up_equality([Identifier|IR],[Val|VR],[b(equal(Identifier,b(value(Val),IDType,[])),pred,[])|TE]) :- |
385 | | get_texpr_type(Identifier,IDType), |
386 | | set_up_equality(IR,VR,TE). |
387 | | |
388 | | |
389 | | |
390 | | :- use_module(tools_meta,[safe_time_out/3,call_residue/2]). |
391 | | |
392 | | :- meta_predicate call_residue_check(0). |
393 | | call_residue_check(Call) :- |
394 | ? | call_residue(Call,Residue), |
395 | | (Residue = [] -> true |
396 | | ; add_internal_error('Call had residue: ',residue(Residue)/call(Call))). |
397 | | |
398 | | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). |
399 | | % very similar to time_out_with_enum_warning, adds catch_clpfd_overflow_call1 |
400 | | :- meta_predicate time_out_and_catch_errors(0,*,*). |
401 | | time_out_and_catch_errors(Call,TimeOut,Result) :- |
402 | ? | on_exception(enumeration_warning(_,_,_,_,_), |
403 | | safe_time_out(catch_clpfd_overflow_call1(call_residue_check(Call)),TimeOut,Result), |
404 | | (print('Treating enumeration warning as TIMEOUT !'),nl, |
405 | | Result=time_out)). |
406 | | |
407 | | :- use_module(tools_printing,[print_red/1, print_green/1]). |
408 | | b_analyse_individual_conjunct(Conjunct,LocalState,State,Conjunct,Status,EnumWarning) :- |
409 | | |
410 | | preferences:get_computed_preference(debug_time_out,DTimeOut), |
411 | | |
412 | | (silent_mode(on) -> true |
413 | | ; nl,print('==> '),translate:print_bexpr(Conjunct),nl), |
414 | | %translate:print_bexpr_with_limit(Conjunct,250),nl, |
415 | | statistics(walltime,[T1,_]), |
416 | | % print(b_test_boolean_expression_wf(Conjunct,LocalState,State)),nl, |
417 | | enter_new_error_scope(ScopeID,b_analyse_individual_conjunct), |
418 | | (time_out_and_catch_errors(b_test_boolean_expression_wf(Conjunct,LocalState,State),DTimeOut,TimeOutRes) -> |
419 | | /* PREDICATE TRUE */ |
420 | | statistics(walltime,[T2,_]),check_enum_warning(positive,EnumWarning), |
421 | | exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_true), % Warning: if strict_raise_warnings is set to true we also get the warnings as errors here !! |
422 | | (TimeOutRes=time_out |
423 | | -> print_red('TIMEOUT'),nl,Status=timeout |
424 | | ; ErrOcc=true -> (preferences:get_preference(strict_raise_warnings,true) -> print('POSSIBLY ') ; true), |
425 | | print_red('NOT-WELL-DEFINED (TRUE)'),nl, Status = wd_error_true |
426 | | ; print_true, |
427 | | enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_true), |
428 | | ((preferences:get_preference(double_evaluation_when_analysing,true), |
429 | | time_out_and_catch_errors(b_not_test_boolean_expression_wf(Conjunct,LocalState,State),DTimeOut,TimeOutRes2)) |
430 | | -> (TimeOutRes2==time_out -> Status = timeout_true ; Status = both_true_false) |
431 | | ; Status = 'TRUE' ), |
432 | | check_enum_warning(_,_NegEnumWarning), |
433 | | exit_error_scope(NegScopeID,_NegTErrorOccurred,b_analyse_double_evaluation_true) % Should we also report those errors ? + NegEnumWarning ? |
434 | | ) |
435 | | ; /* PREDICATE FALSE */ |
436 | | statistics(walltime,[T2,_]), check_enum_warning(negative,EnumWarning), |
437 | | exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_false), |
438 | | (ErrOcc=true -> print_red('NOT-WELL-DEFINED (FALSE)'),nl, Status = wd_error_false |
439 | | ; (EnumWarning=true -> print_red('UNKNOWN') ; print_red('FALSE')),nl, |
440 | | enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_false), |
441 | ? | ((preferences:get_preference(double_evaluation_when_analysing,false) ; time_out_and_catch_errors(b_not_test_boolean_expression_wf(Conjunct,LocalState,State),DTimeOut,TimeOutRes2)) |
442 | | -> (TimeOutRes2==time_out -> Status = timeout_false ; Status = false) |
443 | | ; Status = unknown), |
444 | | exit_error_scope(NegScopeID,_NegFErrorOccurred,b_analyse_double_evaluation_false) % Should we also report those errors ? + NegEnumWarning ? |
445 | | ) |
446 | | ), |
447 | | statistics(walltime,[T3,_]), |
448 | | Time1 is T2-T1, Time2 is T3-T2, Time is T3-T1, |
449 | | (silent_mode(on) -> true |
450 | | ; format('~w (~w ms + ~w ms = ~w ms)',[Status,Time1,Time2,Time]), |
451 | | (Status = 'TRUE' -> true |
452 | ? | ; translate:translate_span(Conjunct,SpanS), SpanS \= '' -> print(' '),print(SpanS) |
453 | | ; true),nl |
454 | | ). |
455 | | |
456 | | print_true :- silent_mode(on),!. |
457 | | print_true :- print_green('TRUE'),nl. |
458 | | |
459 | | check_enum_warning(positive,EnumWarning) :- !, |
460 | | (enumeration_warning_occured_in_error_scope |
461 | | -> print('### Enumeration warnings not critical (solution found)'),nl %, error_manager:trace_if_user_wants_it %% |
462 | | ; true), EnumWarning = false. |
463 | | check_enum_warning(_,EnumWarning) :- |
464 | | \+ enumeration_warning_occured_in_error_scope,!, |
465 | | EnumWarning = false. |
466 | | check_enum_warning(_,EnumWarning) :- |
467 | | (event_occurred_in_error_scope(enumeration_warning(enumerating(_),_,_,_,_)) |
468 | | -> print('### Warning: infinite types were enumerated'),nl, E1=true |
469 | | ; true), |
470 | | (event_occurred_in_error_scope(enumeration_warning(checking_finite_closure,_,_,_,_)) |
471 | | -> print('### Warning: finiteness of comprehension sets could not be determined'),nl, E2=true |
472 | | ; true), |
473 | | ((var(E1),var(E2)) |
474 | | -> print('### Unknown enumeration warning occurred !') |
475 | | ; true), |
476 | | EnumWarning = true. |
477 | | |
478 | | translate_conjunct([],_Status,_EnumWarning,'EmptyInvariant') :- !. |
479 | | /* translate_conjunct(Conjunct,true,true) :- !. */ /* do not show true conjuncts */ |
480 | | translate_conjunct(Conjunct,Status,EnumWarning,Translation) :- |
481 | | translate_conj_status(Conjunct,Status,EnumWarning,Translation). |
482 | | |
483 | | |
484 | | get_conjuncts(BoolExpr,Conjuncts,Status) :- findall(C,get_conjunct(BoolExpr,C,Status),Conjuncts). |
485 | | get_conjunct(C,Conjunct,Status) :- is_a_conjunct(C,LHS,RHS),!, |
486 | | (get_conjuncts(LHS,Conjunct,Status) ; get_conjuncts(RHS,Conjunct,Status)). |
487 | | get_conjunct(Conjunct,Translation,Status) :- |
488 | | translate_conj_status(Conjunct,Status,false,Translation). |
489 | | |
490 | | translate_conj_status(Conjunct,Status,EnumWarning,Translation) :- |
491 | | translate_bexpression_with_limit(Conjunct,500,TC), |
492 | | (EnumWarning=true -> |
493 | | ajoin([TC,'\n == ',Status,' (#### infinite set expanded ####)\n\n'],Translation) |
494 | | ; ajoin([TC,'\n == ',Status,'\n\n'],Translation)). |
495 | | |