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 | | |
6 | | :- module(bvisual2,[ reset_bvisual/0 |
7 | | , bv_get_top_level/1 |
8 | | , bv_expand_formula/3 |
9 | | , bv_get_values/3 |
10 | | , bv_get_values/2 |
11 | | , bv_insert_formula/3 |
12 | | , bv_include_variables/0 |
13 | | , bv_get_value_unlimited/3 |
14 | | , bv_is_explanation_node/1 |
15 | | , bv_print_to_file/3 |
16 | | , bv_write_all_variables_and_constants/2 |
17 | | , set_bvisual2_translation_mode/1 |
18 | | , bv_get_top_level_formula/4 |
19 | | , bv_get_top_level_formula/5 |
20 | | , bv_value_to_atom/2 |
21 | | , bv_show_formula_origin/2 |
22 | | , bv_formula_description/2 |
23 | | , bv_is_typed_formula/1 |
24 | | , bv_is_typed_predicate/1 |
25 | | , bv_is_typed_identifier/2 |
26 | | , bv_get_stored_formula_expr/2 |
27 | | , tcltk_register_new_user_formula/1 |
28 | | , html_debug_operation_for_stateid/4 |
29 | | ]). |
30 | | |
31 | | :- use_module(library(lists)). |
32 | | :- use_module(library(codesio)). |
33 | | %:- use_module(library(timeout)). |
34 | | |
35 | | :- use_module(bmachine, [ b_machine_has_constants_or_properties/0 |
36 | | , b_get_machine_variables/1 |
37 | | , b_get_machine_constants/1 |
38 | | , b_get_machine_operation/4 |
39 | | , b_get_properties_from_machine/1 |
40 | | , b_get_invariant_from_machine/1 |
41 | | , b_get_static_assertions_from_machine/1 |
42 | | , b_get_assertions_from_main_machine/2 |
43 | | , b_get_dynamic_assertions_from_machine/1 |
44 | | , b_get_assertion_count/3 |
45 | | , b_get_operation_variant/3 |
46 | | ]). |
47 | | :- use_module(specfile, [ state_corresponds_to_initialised_b_machine/2 |
48 | | , state_corresponds_to_set_up_constants/2 |
49 | | ]). |
50 | | :- use_module(state_space, [ visited_expression/2 |
51 | | , current_state_id/1 |
52 | | , invariant_not_yet_checked/1 |
53 | | , invariant_violated/1 |
54 | | , transition/3 |
55 | | ]). |
56 | | :- use_module(store, [ empty_state/1 |
57 | | , normalise_store/2 |
58 | | ]). |
59 | | :- use_module(b_interpreter, [ b_test_boolean_expression_wf/3 |
60 | | , b_not_test_boolean_expression_wf/3 |
61 | | , b_test_boolean_expression/4 |
62 | | , b_compute_expression_nowf/4 |
63 | | , set_up_typed_localstate/6 |
64 | | ]). |
65 | | :- use_module(translate, [ translate_subst_or_bexpr_in_mode/3 |
66 | | , translate_bexpression_to_codes/2 |
67 | | , translate_bvalue_for_expression_with_limit/4 |
68 | | , translate_bvalue_for_expression/3 |
69 | | , translate_bvalue_with_type_and_limit/4 |
70 | | , translate_bvalue/2 |
71 | | ]). |
72 | | :- use_module(bsyntaxtree, [ get_texpr_expr/2 |
73 | | , get_texpr_type/2 |
74 | | , get_texpr_info/2 |
75 | | , get_texpr_id/2 |
76 | | , is_texpr/1 |
77 | | , create_texpr/4 |
78 | | , safe_create_texpr/3 |
79 | | , syntaxtraversion/6 |
80 | | , conjunction_to_list/2 |
81 | | , conjunct_predicates/2 |
82 | | , create_exists/3, create_forall/3 |
83 | | %, find_identifier_uses/3 |
84 | | ]). |
85 | | :- use_module(b_ast_cleanup, [ clean_up_pred/3 |
86 | | ]). |
87 | | :- use_module(error_manager, [ get_all_errors_and_clear/1 |
88 | | , time_out_with_enum_warning_one_solution/3 |
89 | | ]). |
90 | | :- use_module(preferences, [ get_preference/2 |
91 | | , set_preference/2 |
92 | | ]). |
93 | | :- use_module(kernel_waitflags, [ init_wait_flags/1 |
94 | | , ground_wait_flags/1]). |
95 | | :- use_module(b_enumerate, [ b_tighter_enumerate_values/2 ]). |
96 | | :- use_module(tools_files, [ put_codes/2]). |
97 | | |
98 | | :- use_module(module_information,[module_info/2]). |
99 | | :- module_info(group,analysis). |
100 | | :- module_info(description,'This module contains functionality to analyse B expressions and predicates by evaluating and decomposing them into substructures.'). |
101 | | |
102 | | :- dynamic top_level_node/1, subnode/2, supernode/2. |
103 | | :- dynamic stored_formula/2, expanded/1, explanation_parent/1. |
104 | | :- dynamic id_counter/1. |
105 | | :- dynamic formula_cache/3. |
106 | | % We store the information whether a node can introduce new values as an (counter-)example |
107 | | % in example_node/1; the value is computed in explore_node/2. |
108 | | % For such nodes, the found examples are stored in local_state/3. |
109 | | :- dynamic example_node/1,local_state/3. |
110 | | |
111 | | |
112 | | bv_value_to_atom(p(P),R) :- !, % a predicate value |
113 | | (P=true -> R='TRUE' ; P=false -> R='FALSE' ; R=P). |
114 | | bv_value_to_atom(e(_),R) :- !, R='ERROR'. |
115 | | bv_value_to_atom(v(V),R) :- !, R=V. % a value, already pretty-printed !?? |
116 | | bv_value_to_atom(i,R) :- !, R='INACTIVE'. |
117 | | bv_value_to_atom(V,V). |
118 | | |
119 | | |
120 | | :- dynamic variables_should_be_included/0. |
121 | | bv_include_variables :- |
122 | | ( variables_should_be_included -> true |
123 | | ; otherwise -> assert(variables_should_be_included)). |
124 | | |
125 | | clear_bvisual :- |
126 | | retractall(top_level_node(_)), |
127 | | retractall(subnode(_,_)), % TO DO: do not delete user formulas for a simple re-load ?! |
128 | | retractall(supernode(_,_)), |
129 | | retractall(stored_formula(_,_)), |
130 | | retractall(expanded(_)), |
131 | | retractall(explanation_parent(_)), |
132 | | retractall(formula_cache(_,_,_)), |
133 | | retractall(example_node(_)), |
134 | | retractall(local_state(_,_,_)). |
135 | | % This predicate should be called after loading a new specification |
136 | | % and before using the other predicates below |
137 | | reset_bvisual :- |
138 | | clear_bvisual, |
139 | | register_top_level. |
140 | | |
141 | | :- public portray_bvisual/0. % debugging utility |
142 | | portray_bvisual :- %listing(top_level_node/1), listing(subnode/2), listing(stored_formula/2) |
143 | | top_level_node(N), bv_portray(N,1),fail. |
144 | | portray_bvisual. |
145 | | bv_portray(ID,Level) :- |
146 | | (stored_formula(ID,Form) -> functor(Form,F,_) ; F = '??'), |
147 | | (expanded(ID) -> E=expanded ; E = 'not_expanded'), |
148 | | indent(Level),format('~w -> ~w [~w]~n',[ID,F,E]), |
149 | | L1 is Level+1, |
150 | | subnode(ID,ID2), |
151 | | bv_portray(ID2,L1). |
152 | | indent(0) :- !. |
153 | | indent(N) :- N>0,!, N1 is N-1, print(' '), indent(N1). |
154 | | |
155 | | % returns the top-level nodes as a list of IDs |
156 | | bv_get_top_level(Tops) :- |
157 | | findall( Id, top_level_node(Id), Tops ). |
158 | | |
159 | | % bv_expand_formula(+FormulaID,-LabelAtom,-) |
160 | | % Input: Id |
161 | | % Output: Label of Formula, list of children |
162 | | bv_expand_formula(Id,Label,Children) :- |
163 | | expanded(Id),!, |
164 | | get_node_label(Id,Label), |
165 | | findall(C, subnode(Id,C), Children). |
166 | | bv_expand_formula(Id,Label,Children) :- |
167 | | get_node_label(Id,Label), |
168 | | explore_node(Id,Children). |
169 | | |
170 | | % bv_get_values in current state |
171 | | bv_get_values(Ids,Values) :- |
172 | | current_state_id(StateId), |
173 | | bv_get_values(Ids,StateId,Values). |
174 | | |
175 | | :- use_module(specfile,[prepare_state_for_specfile_trans/2]). |
176 | | |
177 | | % bv_get_values(+IdsOfFormulas,+CurrentStateID,-ValuesOfFormulas) |
178 | | bv_get_values(Ids,StateId,Values) :- |
179 | | visited_expression(StateId,State),!, |
180 | | prepare_state_for_specfile_trans(State,PreparedState), |
181 | | get_preference(time_out,Timeout), |
182 | | bv_get_values2(Ids,PreparedState,StateId,Timeout,Values). |
183 | | bv_get_values(Ids,_StateId,Values) :- |
184 | | % in case that the state ID cannot be resolved, we |
185 | | % return an error for each formula |
186 | | same_length(Ids,Values), |
187 | | same_value(Values,e('unkown state')). |
188 | | same_value([],_). |
189 | | same_value([V|Rest],V) :- same_value(Rest,V). |
190 | | |
191 | | |
192 | | % Insert a new formula |
193 | | % bv_insert_formula(+TypeCheckedExpression,+ParentID,-IDofNewFormula) |
194 | | bv_insert_formula(TExpr,ParentId,Id) :- %print(bv_insert_formula(TExpr,ParentId)),nl, |
195 | | get_new_id(Id), |
196 | | assert( stored_formula(Id,TExpr) ), |
197 | | assert( subnode(ParentId,Id) ), |
198 | | assert( supernode(Id,ParentId) ), |
199 | | ( ParentId == top -> |
200 | | assert( top_level_node(Id) ) |
201 | | ; otherwise -> |
202 | | true). |
203 | | |
204 | | |
205 | | :- meta_predicate bv_time_out_call(0,-,-,-). |
206 | | bv_time_out_call(Call,ValueFromCall,Timeout,Value) :- |
207 | | (time_out_with_enum_warning_one_solution( Call, |
208 | | Timeout, |
209 | | Result) |
210 | | -> |
211 | | ( Result == success -> Value = ValueFromCall |
212 | | ; Result = virtual_time_out(failure_enumeration_warning(_Info,_,_,_,critical)) -> Value = e('?(\x221E\)') % Value = e('\x22A5\?(\x221E\)') % 8734 in decimal % Feedback for user: increasing MAXINT,... could mean ProB can find a solution; However, increasing TIMEOUT value will not help |
213 | | ; Result = virtual_time_out(_) -> Value = e('?(\x221E\)') % infinity symbol: Feedback to the user: probably no way to solve the issue apart from ensuring that set comprehensions are finite ... |
214 | | ; otherwise -> Value = e(timeout)) |
215 | | ). |
216 | | |
217 | | bv_get_values2([],_,_,_,[]). |
218 | | bv_get_values2([Id|Irest],State,StateId,Timeout,[Value|Vrest]) :- |
219 | | bv_get_value(Id,State,StateId,Timeout,Value), |
220 | | bv_get_values2(Irest,State,StateId,Timeout,Vrest). |
221 | | bv_get_value(Id,State1,StateId,Timeout,FinalValue) :- |
222 | | bv_get_value_unprocessed(Id,State1,StateId,Timeout,Value), |
223 | | value_post_processing(Value,FinalValue). |
224 | | bv_get_value_unprocessed(Id,State1,StateId,Timeout,Value) :- |
225 | | is_active(Id,StateId,State1,State,LocalState),!, %print(is_active(Id)), debug:nl_time, |
226 | | ( is_cached(Id,StateId,State1,Value1) -> |
227 | | FromCache = true |
228 | | ; bv_get_value1(Id,State,LocalState,Timeout,Value1) -> |
229 | | FromCache = false %, print(evaluated),debug:nl_time |
230 | | ; otherwise -> |
231 | | Value1 = e('evaluation failed'), |
232 | | FromCache = false), |
233 | | handle_errors(Value1,Value), |
234 | | ( FromCache==false, should_be_cached(Id) -> |
235 | | write_to_cache(Id,StateId,State1,Value) |
236 | | ; otherwise -> true). |
237 | | bv_get_value_unprocessed(_Id,_State1,_StateId,_Timeout,i). % INACTIVE |
238 | | bv_get_value1(Id,State,LocalState,Timeout,Value) :- |
239 | | stored_formula(Id,Formula), |
240 | | bv_get_value2(Formula,State,LocalState,Timeout,Value). |
241 | | bv_get_value2(Formula,State,LocalState,Timeout,Value) :- |
242 | | is_texpr(Formula),!, |
243 | | get_texpr_type(Formula,Type), |
244 | | bv_get_value3(Type,Formula,LocalState,State,Timeout,Value). |
245 | | bv_get_value2(bind(_ID,Value),_,_,_,btvalue(Value)). |
246 | | bv_get_value2(textnode(Value,_),_State,_LS,_,v(Value)). |
247 | | %bv_get_value2(cbc_path(_LastStateID,Path,_Last),_State,_LS,_,v(NrOfPaths)) :- |
248 | | % append(Path,_,Prefix), |
249 | | % findall(Last,sap:cb_path(_,Prefix,Last),AllPathsWithPrefix), |
250 | | % length(AllPathsWithPrefix,NrOfPaths). |
251 | | bv_get_value2(variant(_Name,_ConvOrAnt,Variant),State,LocalState,Timeout,Value) :- |
252 | | bv_get_value2(Variant,State,LocalState,Timeout,Value). |
253 | | bv_get_value2(guard(_Name,Parameters,Guard),State,LocalState,Timeout,Value) :- !, |
254 | | get_guard_formula(Parameters,Guard,Expr), |
255 | | bv_get_value2(Expr,State,LocalState,Timeout,Value). |
256 | | bv_get_value2(guard_theorems(_Name,Parameters,Guard,Theorems),State,LocalState,Timeout,Value) :- !, |
257 | | get_guard_theorems_formula(Parameters,Guard,Theorems,Expr), |
258 | | bv_get_value2(Expr,State,LocalState,Timeout,Value). |
259 | | bv_get_value3(pred,Formula,LocalState,State,Timeout,Value) :- |
260 | | !, |
261 | | % print('CHECKING PREDICATE: '), translate:print_bexpr(Formula),nl, |
262 | | ( bv_time_out_call(b_test_boolean_expression_wf(Formula,LocalState,State),true,Timeout,ValuePos) -> true |
263 | | ; otherwise -> ValuePos=false), |
264 | | ( get_preference(double_evaluation_when_analysing,true) -> |
265 | | ( bv_time_out_call(b_not_test_boolean_expression_wf(Formula,LocalState,State),true,Timeout,ValueNeg) -> true |
266 | | ; otherwise -> ValueNeg=false), |
267 | | combine_predicate_values(ValuePos,ValueNeg,Value) |
268 | | ; otherwise -> encode_predicate_value(ValuePos,Value)). |
269 | | bv_get_value3(_,Formula,LocalState,State,Timeout,Res) :- |
270 | | bv_time_out_call(b_compute_expression_nowf(Formula,LocalState,State,FValue),FValue,Timeout,Value),!, |
271 | | ( Value = e(E) -> Res = e(E) % e for exception or timeout |
272 | | ; otherwise -> Res = btvalue(Value,Formula) |
273 | | ). |
274 | | |
275 | | |
276 | | encode_predicate_value(e(Error),e(Error)). |
277 | | encode_predicate_value(true,p(true)). |
278 | | encode_predicate_value(false,p(false)). |
279 | | combine_predicate_values(e(_Error),true,p(false)) :- print('### Ignoring Timeout in Positive Case of DOUBLE_EVALUATION as Negated Predicate is TRUE'),nl. |
280 | | combine_predicate_values(e(_Error),false,p(true)) :- print('### Ignoring Timeout in Positive Case of DOUBLE_EVALUATION as Negated Predicate is FALSE'),nl. |
281 | | combine_predicate_values(e(Error),e(_),e(Error)). |
282 | | combine_predicate_values(true,false,p(true)). |
283 | | combine_predicate_values(false,true,p(false)). |
284 | | combine_predicate_values(true,true,e('both true and false')). |
285 | | combine_predicate_values(false,false,e(undefined)). |
286 | | combine_predicate_values(true,e(_Error),p(true)) :- print('### Ignoring Timeout in Negative Case of DOUBLE_EVALUATION'),nl. |
287 | | combine_predicate_values(false,e(_Error),p(false)) :- print('### Ignoring Timeout in Negative Case of DOUBLE_EVALUATION'),nl. |
288 | | |
289 | | :- dynamic get_unlimited_value/0. |
290 | | |
291 | | :- use_module(translate,[set_translation_mode/1,unset_translation_mode/1]). |
292 | | |
293 | | value_post_processing(In,Out) :- |
294 | | bvisual2_translation_mode(Mode), |
295 | | set_translation_mode(Mode), |
296 | | ( value_post_processing2(In,O) -> O=Out |
297 | | ; otherwise -> Out=e('internal error: failed to post-process value')), |
298 | | unset_translation_mode(Mode). |
299 | | value_post_processing2(v(Value),v(Value)). |
300 | | value_post_processing2(p(Value),p(Value)). |
301 | | value_post_processing2(e(Error),e(Error)). |
302 | | value_post_processing2(i,i). |
303 | | value_post_processing2(btvalue(BValue,Expr),v(Value)) :- |
304 | | (get_unlimited_value -> translate_bvalue_for_expression(BValue,Expr,Value) |
305 | | ; translate_bvalue_for_expression_with_limit(BValue,Expr,600,Value) % one can always use bv_get_value_unlimited |
306 | | ). |
307 | | value_post_processing2(btvalue(BValue),v(Value)) :- |
308 | | % TO DO: get type for variables and constants |
309 | | (get_unlimited_value -> translate_bvalue(BValue,Value) |
310 | | ; translate_bvalue_with_type_and_limit(BValue,any,600,Value)). |
311 | | |
312 | | |
313 | | |
314 | | |
315 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
316 | | % caching of some values |
317 | | :- use_module(store,[no_value_for_variable/2]). |
318 | | |
319 | | % we do not compute the theorems node, only its subnodes |
320 | | is_cached(theoremsc,_,_,v('')) :- !. |
321 | | is_cached(theoremscm,_,_,v('')) :- !. |
322 | | is_cached(theoremsv,_,_,v('')) :- !. |
323 | | is_cached(theoremsvm,_,_,v('')) :- !. |
324 | | is_cached(goal,_,_,v('')) :- !. |
325 | | % we use the invariant_violated flag of the state space as a kind of cache |
326 | | is_cached(inv,StateId,_State,Value) :- |
327 | | \+ invariant_not_yet_checked(StateId), |
328 | | ( invariant_violated(StateId) -> Value=p(false) |
329 | | ; otherwise -> Value=p(true)). |
330 | | % axioms are usually true in the constants' state |
331 | | is_cached(axioms,StateId,concrete_constants(State),R) :- !, |
332 | | is_cached_constants_state(StateId,State,R). |
333 | | is_cached(axioms,StateId,[_|_],R) :- !, % states consisting of just a list are either constructed by |
334 | | % find valid state, state-based MC,... or when there are no constants |
335 | | % We assume PROPERTIES/axioms to be true; by constructing these commands have to satisfy the properties |
336 | | is_cached_constants_state(StateId,[],R). |
337 | | % this formula was already computed and cached for the given state |
338 | | is_cached(FormulaId,StateId,_State,Value) :- |
339 | | formula_cache(FormulaId,StateId,Value),!. |
340 | | % in case of axiom, we can look at the reverences constants' state |
341 | | is_cached(FormulaId,_,expanded_const_and_vars(ConstId,_,_),Value) :- is_cached_axiom(FormulaId,ConstId,Value). |
342 | | is_cached(FormulaId,_,const_and_vars(ConstId,_),Value) :- is_cached_axiom(FormulaId,ConstId,Value). |
343 | | is_cached_axiom(FormulaId,ConstId,Value) :- |
344 | | is_axiom_or_static_theorem(FormulaId), |
345 | | visited_expression(ConstId,ConstState), |
346 | | is_cached(FormulaId,ConstId,ConstState,Value),!. |
347 | | |
348 | | is_cached_constants_state(StateId,State,R) :- |
349 | | % only if a partial_setup_constants event led to that |
350 | | % state, then something did not work |
351 | | ( transition(root,'$partial_setup_constants',StateId) -> |
352 | | (member(bind(_,Val),State), no_value_for_variable(Val,_) |
353 | | -> R = e('some constants have no values') |
354 | | ; animation_minor_mode(eventb) -> R = e('some axioms may be false') |
355 | | ; otherwise -> R = e('some properties may be false') |
356 | | ) |
357 | | ; otherwise -> |
358 | | R = p(true)). |
359 | | |
360 | | should_be_cached(FormulaId) :- |
361 | | is_axiom_or_static_theorem(FormulaId). |
362 | | |
363 | | write_to_cache(FormulaId,_StateId,const_and_vars(ConstId,_),Value) :- |
364 | | is_axiom_or_static_theorem(FormulaId),!, |
365 | | visited_expression(ConstId,ConstState), |
366 | | write_to_cache(FormulaId,ConstId,ConstState,Value). |
367 | | write_to_cache(FormulaId,StateId,_State,Value) :- |
368 | | assert(formula_cache(FormulaId,StateId,Value)). |
369 | | |
370 | | is_axiom_or_static_theorem(axioms) :- !. |
371 | | is_axiom_or_static_theorem(theoremsc) :- !. |
372 | | is_axiom_or_static_theorem(theoremscm) :- !. |
373 | | is_axiom_or_static_theorem(FormulaId) :- |
374 | | supernode(FormulaId,Parent),is_axiom_or_static_theorem(Parent). |
375 | | |
376 | | handle_errors(_,e(ErrorMsg)) :- |
377 | | get_all_errors_and_clear([Error|_]),!, % TO DO: use proper error scoping and do not trigger when error stored before calling bvisual2 |
378 | | write_to_codes(Error,ErrorCodes), |
379 | | limit_error(ErrorCodes,ErrorCodes2), |
380 | | atom_codes(ErrorMsg,ErrorCodes2). |
381 | | handle_errors(Value,Value). |
382 | | |
383 | | limit_error(ErrorCodes,ErrorCodes) :- |
384 | | length(ErrorCodes,L),L < 200,!. |
385 | | limit_error(In,Out) :- |
386 | | prefix_length(In,Start,200), |
387 | | append(Start,"...",Out). |
388 | | |
389 | | % is_active(+FormulaID,+InState,-PossiblyExpandedState) |
390 | | % says if a FormulaID makes sense for the current state, if not: it will be grayed out |
391 | | is_active(user,StateId,InState,OutState,LocalState) :- !, |
392 | | is_active(inv,StateId,InState,OutState,LocalState). |
393 | | is_active(inv,_StateId,InState,OutState,LocalState) :- !, |
394 | | empty_state(LocalState), |
395 | | state_corresponds_to_initialised_b_machine(InState,OutState). |
396 | | is_active(axioms,_StateId,InState,OutState,LocalState) :- !, |
397 | | InState \= root, |
398 | | empty_state(LocalState), |
399 | | state_corresponds_to_set_up_constants(InState,OutState), |
400 | | !. |
401 | | is_active(variants,StateId,InState,OutState,LocalState) :- !, |
402 | | is_active(inv,StateId,InState,OutState,LocalState). |
403 | | is_active(theoremsc,StateId,InState,OutState,LocalState) :- !, |
404 | | is_active(axioms,StateId,InState,OutState,LocalState). |
405 | | is_active(theoremscm,StateId,InState,OutState,LocalState) :- !, |
406 | | is_active(axioms,StateId,InState,OutState,LocalState). |
407 | | is_active(theoremsv,StateId,InState,OutState,LocalState) :- !, |
408 | | is_active(inv,StateId,InState,OutState,LocalState). |
409 | | is_active(theoremsvm,StateId,InState,OutState,LocalState) :- !, |
410 | | is_active(inv,StateId,InState,OutState,LocalState). |
411 | | is_active(guards,StateId,InState,OutState,LocalState) :- !, |
412 | | is_active(inv,StateId,InState,OutState,LocalState). |
413 | | is_active(guard_theorems,StateId,InState,OutState,LocalState) :- !, |
414 | | is_active(inv,StateId,InState,OutState,LocalState). |
415 | | is_active(variables,StateId,InState,OutState,LocalState) :- !, |
416 | | is_active(inv,StateId,InState,OutState,LocalState). |
417 | | is_active(constants,StateId,InState,OutState,LocalState) :- !, |
418 | | is_active(axioms,StateId,InState,OutState,LocalState). |
419 | | is_active(sets,_StateId,InState,OutState,LocalState) :- !, b_or_z_successsful_mode, |
420 | | empty_state(LocalState), InState=OutState. |
421 | | is_active(freetypes,_StateId,InState,OutState,LocalState) :- !, |
422 | | empty_state(LocalState), InState=OutState. |
423 | | is_active(goal,StateId,InState,OutState,LocalState) :- !, |
424 | | is_active(inv,StateId,InState,OutState,LocalState). |
425 | | is_active(user_formulas,StateId,InState,OutState,LocalState) :- !, |
426 | | is_active(inv,StateId,InState,OutState,LocalState). |
427 | | is_active(definitions,StateId,InState,OutState,LocalState) :- !, |
428 | | is_active(inv,StateId,InState,OutState,LocalState). |
429 | | is_active(channels,_StateId,S,OutState,LocalState) :- !, |
430 | | csp_mode, OutState=S,empty_state(LocalState). |
431 | | is_active(datatypes,_StateId,S,OutState,LocalState) :- !, |
432 | | csp_mode, OutState=S,empty_state(LocalState). |
433 | | is_active(subtypes,_StateId,S,OutState,LocalState) :- !, |
434 | | csp_mode, OutState=S,empty_state(LocalState). |
435 | | %is_active(cbc_tests,_StateId,_InState,_OutState,_LocalState) :- !, |
436 | | % sap:cb_path(_,[_],_). % show cbc_tests if we ran CBC test-case generator |
437 | | is_active(NodeId,StateId,InState,OutState,LocalState) :- |
438 | | supernode(NodeId,Super), |
439 | | is_active(Super,StateId,InState,OutState,InLocalState), |
440 | | % check if the parent node introduces example values (e.g. in a exists-clause) |
441 | | % If yes, the local state is extended by the values |
442 | | ( example_node(Super) -> |
443 | | find_example(Super,StateId,OutState,InLocalState,LocalState) |
444 | | ; otherwise -> |
445 | | InLocalState = LocalState). |
446 | | |
447 | | find_example(NodeId,StateId,_State,_InLocalState,LocalState) :- |
448 | | % check if the value was computed and cached before |
449 | | local_state(NodeId,StateId,Result),!, |
450 | | % if Result is not of the form example/1, no example |
451 | | % was found. Just fail to show inactive state |
452 | | Result = example(LocalState). |
453 | | find_example(NodeId,StateId,State,InLocalState,LocalState) :- |
454 | | % how the example is computed depends on the expression (e.g. exists) |
455 | | % and the outcome of the parent node (true or false) |
456 | | bv_get_values([NodeId],StateId,[V]),!, |
457 | | stored_formula(NodeId,Formula), |
458 | | ( find_example1(Formula,V,State,InLocalState,LocalState) -> |
459 | | Result = example(LocalState) |
460 | | ; otherwise -> |
461 | | Result = not_found), |
462 | | % currently we just ignore errors |
463 | | handle_errors(_,_), |
464 | | assert( local_state(NodeId,StateId,Result) ), |
465 | | Result = example(_). |
466 | | find_example1(TExpr,V,State,InLocalState,LocalState) :- |
467 | | is_texpr(TExpr),!, |
468 | | get_texpr_expr(TExpr,Expr), |
469 | | find_example2(Expr,V,State,InLocalState,LocalState). |
470 | | find_example1(guard(_Name,Parameters,Guard),V,State,InLocalState,LocalState) :- |
471 | | create_exists(Parameters,Guard,Exists), |
472 | | find_example1(Exists,V,State,InLocalState,LocalState). |
473 | | find_example1(guard_theorems(_Name,Parameters,Guard,Theorems),V,State,InLocalState,LocalState) :- |
474 | | create_forall(Parameters,b(implication(Guard,Theorems),pred,[]),ForAll), |
475 | | find_example1(ForAll,V,State,InLocalState,LocalState). |
476 | | find_example2(let_predicate(Ids,AssignmentExprs,Pred),Status,State,InLocalState,LocalState) :- |
477 | | % translate LET back to exists |
478 | | create_exists_for_let(Ids,AssignmentExprs,Pred,_,ExistsPred), |
479 | | find_example2(exists(Ids,ExistsPred),Status,State,InLocalState,LocalState). |
480 | | find_example2(exists(Ids,Predicate),p(true),State,InLocalState,LocalState) :- |
481 | | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState). |
482 | | find_example2(exists(Ids,Predicate),p(false),State,InLocalState,LocalState) :- |
483 | | Predicate = b(conjunct(_,_),pred,_), % we have a false conjunct: try and find maximal prefix that is satisfiable |
484 | | conjunction_to_list(Predicate,PredList), |
485 | | maxsat_conjunct(Ids,PredList,[],State,InLocalState,no_solution,LocalState), |
486 | | LocalState \= no_solution, |
487 | | !. |
488 | | find_example2(exists(Ids,Predicate),p(false),State,InLocalState,LocalState) :- |
489 | | safe_create_texpr(negation(Predicate),pred,Negation), |
490 | | find_solution_for_predicate(Ids,Negation,State,InLocalState,LocalState). |
491 | | find_example2(forall(Ids,Pre,Condition),p(false),State,InLocalState,LocalState) :- |
492 | | safe_create_texpr(negation(Condition),pred,Negation), |
493 | | conjunct_predicates([Pre,Negation],Predicate), |
494 | | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState). |
495 | | find_example2(forall(Ids,Pre,Condition),p(true),State,InLocalState,LocalState) :- |
496 | | conjunct_predicates([Pre,Condition],Predicate), |
497 | | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState), |
498 | | !. |
499 | | find_example2(forall(Ids,Pre,_),p(true),State,InLocalState,LocalState) :- |
500 | | % the LHS of the forall is never true; try find maximal subsequence for it: |
501 | | find_example2(exists(Ids,Pre),p(false),State,InLocalState,LocalState). |
502 | | find_solution_for_predicate(Ids,Predicate,State,InLocalState,NormedLocalState) :- |
503 | | get_preference(time_out,Timeout), |
504 | | set_up_typed_localstate(Ids,_FreshVars,TypedVals,InLocalState,LocalState,positive), |
505 | | (time_out_with_enum_warning_one_solution( (init_wait_flags(WF), |
506 | | b_tighter_enumerate_values(TypedVals,WF), |
507 | | b_test_boolean_expression(Predicate,LocalState,State,WF), |
508 | | ground_wait_flags(WF)), |
509 | | Timeout,Result) |
510 | | -> Result == success, |
511 | | normalise_store(LocalState,NormedLocalState) |
512 | | ). |
513 | | |
514 | | create_exists_for_let(Ids,AssignmentExprs,Pred,Equalities,ExistsPred) :- |
515 | | maplist(create_equality,Ids,AssignmentExprs,Equalities), |
516 | | append(Equalities,[Pred],L), |
517 | | conjunct_predicates(L,ExistsPred). |
518 | | |
519 | | create_equality(ID,Expr,Equality) :- |
520 | | safe_create_texpr(equal(ID,Expr),pred,Equality). |
521 | | |
522 | | % find maximal subsequence of conjuncts that are satisfiable and return LocalState solution found |
523 | | maxsat_conjunct(Ids,[LHS|Rest],ConSoFar,State,InLocalState,_BestLocalStateSoFar,ResLocalState) :- |
524 | | append(ConSoFar,[LHS],NewConjunctList), |
525 | | %print('TRY: '), translate:print_bexpr(LHS),nl, |
526 | | conjunct_predicates(NewConjunctList,NewConjunct), |
527 | | find_solution_for_predicate(Ids,NewConjunct,State,InLocalState,LocalState), |
528 | | !, % print('+'), |
529 | | maxsat_conjunct(Ids,Rest,NewConjunctList,State,InLocalState, LocalState,ResLocalState). |
530 | | maxsat_conjunct(Ids,[_|Rest],ConSoFar,State,InLocalState,BestLocalStateSoFar,Res) :- !, % allows skipping conjuncts |
531 | | maxsat_conjunct(Ids,Rest,ConSoFar,State,InLocalState,BestLocalStateSoFar,Res). |
532 | | maxsat_conjunct(_Ids,_Rest,_ConSoFar,_State,_InLocalState,BestLocalStateSoFar,Res) :- |
533 | | Res = BestLocalStateSoFar. |
534 | | |
535 | | explore_node(Id,Children) :- |
536 | | stored_formula(Id,Formula), |
537 | | check_if_example_node(Id,Formula), |
538 | | get_subformulas(Formula,Subs,Kind), |
539 | | assert( expanded(Id) ), |
540 | | (Kind = explanation |
541 | | -> assert_as_explanation(Id,ExplId), Children = [ExplId|Children1], |
542 | | register_formulas(Subs,Id,Children1) |
543 | | ; register_formulas(Subs,Id,Children)). |
544 | | |
545 | | assert_as_explanation(Parent,Id) :- |
546 | | assert(explanation_parent(Parent)), |
547 | | % add a text line; showing that we did an equivalence rewrite |
548 | | get_new_id(Id), |
549 | | assert( stored_formula(Id,textnode('\x21D4\',[])) ), % unicode translation |
550 | | assert( subnode(Parent,Id) ), |
551 | | assert( supernode(Id,Parent) ). |
552 | | |
553 | | bv_is_explanation_node(NodeId) :- |
554 | | supernode(NodeId,ParentId), |
555 | | explanation_parent(ParentId). |
556 | | |
557 | | % the following predicates determine whether the node introduces |
558 | | % example values and stores that information in example_node/1. |
559 | | check_if_example_node(Id,Formula) :- |
560 | | is_example_node(Formula),!, |
561 | | assert( example_node(Id) ). |
562 | | check_if_example_node(_Id,_Formula). |
563 | | is_example_node(TFormula) :- |
564 | | is_texpr(TFormula),!, |
565 | | get_texpr_expr(TFormula,Formula), |
566 | | is_example_node2(Formula). |
567 | | is_example_node(guard(_Name,[_|_],_Guard)). |
568 | | is_example_node(guard_theorems(_Name,[_|_],_Guard,_Theorems)). |
569 | | is_example_node2(exists(_Ids,_Cond)). |
570 | | is_example_node2(forall(_Ids,_Pre,_Cond)). |
571 | | is_example_node2(let_predicate(_Ids,_E,_Cond)). |
572 | | |
573 | | % subformula_rule/4 defines wich subformulas should be |
574 | | % shown in an evaluation tree for a formula. If no |
575 | | % rule matches, the standard subformulas are used |
576 | | subformula_rule(equal(A,B),TF,[Sub1,Sub2],explanation) :- |
577 | | get_texpr_type(A,T),T=set(SType), |
578 | | \+ (kernel_objects:max_cardinality(SType,Max),number(Max),Max<10), % sets can never be very large |
579 | | is_not_bvexpr(TF), % do not apply to explanation expressions |
580 | | no_empty_set(A),no_empty_set(B), |
581 | | !, |
582 | | create_bvexpr(set_subtraction(A,B),T,AminusB), |
583 | | create_bvexpr(set_subtraction(B,A),T,BminusA), |
584 | | create_bvexpr(empty_set,T,Empty), |
585 | | create_bvexpr(equal(AminusB,Empty),pred,Sub1), |
586 | | create_bvexpr(equal(BminusA,Empty),pred,Sub2). |
587 | | subformula_rule(subset(A,B),_,[Equals],explanation) :- |
588 | | subset_rule(A,B,Equals). |
589 | | subformula_rule(subset_strict(A,B),_,[AmBEmpty,NotEquals],explanation) :- |
590 | | subset_rule(A,B,AmBEmpty), |
591 | | get_texpr_type(A,T), |
592 | | create_bvexpr(set_subtraction(B,A),T,BminusA), |
593 | | create_bvexpr(empty_set,T,Empty), |
594 | | create_bvexpr(not_equal(BminusA,Empty),pred,NotEquals). |
595 | | subformula_rule(not_subset(A,B),_,Subs,Kind) :- |
596 | | subformula_rule(subset(A,B),_,Subs,Kind). % it is an equivalent rewrite to the negation |
597 | | subformula_rule(not_subset_strict(A,B),_,Subs,Kind) :- |
598 | | subformula_rule(subset_strict(A,B),_,Subs,Kind). % it is an equivalent rewrite to the negation |
599 | | subformula_rule(forall(Ids,P,R),_,Subs,quantifier) :- |
600 | | append(Ids,[P,R],Subs). |
601 | | subformula_rule(let_predicate(Ids,AssignmentExprs,Pred),_,Subs,quantifier) :- |
602 | | create_exists_for_let(Ids,AssignmentExprs,Pred,Equalities,_ExistsPred), |
603 | | append(Equalities,[Pred],EP), % show equalities and then one subnode for the predicate |
604 | | append(Ids,EP,Subs). |
605 | | subformula_rule(exists(Ids,P),_,Subs,quantifier) :- |
606 | | conjunction_to_list(P,PL), |
607 | | append(Ids,PL,Subs). |
608 | | subformula_rule(conjunct(A,B),_,Subs,normal) :- |
609 | | safe_create_texpr(conjunct(A,B),pred,E), |
610 | | conjunction_to_list(E,Subs). |
611 | | subformula_rule(disjunct(A,B),_,Subs,normal) :- |
612 | | disjunction_to_list(A,B,Subs). |
613 | | subformula_rule(member(TM,TS),_,Children,explanation) :- |
614 | | get_texpr_expr(TS,S), |
615 | | subformula_member_rule(S,TM,TS,Children),!. |
616 | | |
617 | | subset_rule(A,B,Equals) :- |
618 | | get_texpr_type(A,T), |
619 | | create_bvexpr(set_subtraction(A,B),T,AminusB), |
620 | | create_bvexpr(empty_set,T,Empty), |
621 | | create_bvexpr(equal(AminusB,Empty),pred,Equals). |
622 | | |
623 | | :- use_module(bsyntaxtree,[is_just_type/1]). |
624 | | |
625 | | subformula_member_rule(partial_function(TDom,TRan),TM,TS,[TDoubles]) :- |
626 | | is_just_type(TDom), |
627 | | is_just_type(TRan), |
628 | | !, |
629 | | % this rule describes the plain function check, without |
630 | | % checking domains |
631 | | texpr_function_type(TS,FunctionType,DomType,RanType), |
632 | | create_texpr(identifier(d_1),DomType,[],TDomId), |
633 | | create_texpr(identifier(r_1),RanType,[],TRanId1), |
634 | | create_texpr(identifier(r_2),RanType,[],TRanId2), |
635 | | create_texpr(comprehension_set([TDomId,TRanId1],TExists),FunctionType,[],TDoubles), |
636 | | % create_exists([TRanId2],TPred,TExists1), % moved below so that used ids can be computed |
637 | | create_texpr(couple(TDomId,TRanId1),couple(DomType,RanType),[],TCouple1), |
638 | | create_texpr(couple(TDomId,TRanId2),couple(DomType,RanType),[],TCouple2), |
639 | | safe_create_texpr(not_equal(TRanId1,TRanId2),pred,Unequal), |
640 | | create_texpr(member(TCouple1,TM),pred,[],TMember1), |
641 | | create_texpr(member(TCouple2,TM),pred,[],TMember2), |
642 | | conjunct_predicates([Unequal,TMember1,TMember2],TPred), |
643 | | create_exists([TRanId2],TPred,TExists1), % now also computes used identifiers; cleanup no longer required ? |
644 | | % This is necessary to register the used identifiers |
645 | | clean_up_pred(TExists1,[],TExists). |
646 | | subformula_member_rule(partial_function(TA,TB),TM,TS,[TFunCheck|SetChecks]) :- |
647 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
648 | | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). |
649 | | subformula_member_rule(total_function(TA,TB),TM,TS,[TFunCheck|SetChecks]) :- |
650 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
651 | | create_total_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). |
652 | | subformula_member_rule(partial_injection(TA,TB),TM,TS,[TFunCheck,TInjCheck|SetChecks]) :- |
653 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
654 | | create_injection_check(TM,TS,TInjCheck), |
655 | | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). |
656 | | subformula_member_rule(total_injection(TA,TB),TM,TS,[TFunCheck,TInjCheck|SetChecks]) :- |
657 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
658 | | create_injection_check(TM,TS,TInjCheck), |
659 | | create_total_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). |
660 | | subformula_member_rule(partial_surjection(TA,TB),TM,TS,Children) :- |
661 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
662 | | create_texpr(equal(TRange,TB),pred,[],TRanCheck), |
663 | | create_optional_subset_check(TDomain,TA,DomChecks), |
664 | | append([TFunCheck|DomChecks],[TRanCheck],Children). |
665 | | subformula_member_rule(total_surjection(TA,TB),TM,TS,[TFunCheck,TDomCheck,TRanCheck]) :- |
666 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
667 | | create_texpr(equal(TDomain,TA),pred,[],TDomCheck), |
668 | | create_texpr(equal(TRange,TB),pred,[],TRanCheck). |
669 | | subformula_member_rule(total_bijection(TA,TB),TM,TS,[TFunCheck,TInjCheck,TDomCheck,TRanCheck]) :- |
670 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
671 | | create_injection_check(TM,TS,TInjCheck), |
672 | | create_texpr(equal(TDomain,TA),pred,[],TDomCheck), |
673 | | create_texpr(equal(TRange,TB),pred,[],TRanCheck). |
674 | | subformula_member_rule(partial_bijection(TA,TB),TM,TS,Children) :- |
675 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange), |
676 | | create_injection_check(TM,TS,TInjCheck), |
677 | | create_optional_subset_check(TDomain,TA,DomChecks), |
678 | | create_texpr(equal(TRange,TB),pred,[],TRanCheck), |
679 | | append([TFunCheck,TInjCheck|DomChecks],[TRanCheck],Children). |
680 | | subformula_member_rule(pow_subset(TA),TM,_TS,[NewCheck]) :- |
681 | | % TM : POW(TA) <=> TM \ TA = {} |
682 | | get_texpr_type(TM,Type), |
683 | | create_bvexpr(set_subtraction(TM,TA),Type,Diff), |
684 | | create_bvexpr(empty_set,Type,Empty), |
685 | | create_bvexpr(equal(Diff,Empty),pred,NewCheck). |
686 | | % TO DO: add rules for <:, <<:, FIN, POW1, FIN1 |
687 | | |
688 | | create_function_check(TM,TS,TFunCheck,TDomain,TRange) :- |
689 | | texpr_function_type(TS,FunctionType,DomType,RanType), |
690 | | translate:set_type_to_maximal_texpr(DomType,TDom), |
691 | | translate:set_type_to_maximal_texpr(RanType,TRan), |
692 | | create_bvexpr(partial_function(TDom,TRan),set(FunctionType),TFun), |
693 | | create_bvexpr(member(TM,TFun),pred,TFunCheck), |
694 | | create_bvexpr(domain(TM),set(DomType),TDomain), |
695 | | create_bvexpr(range(TM),set(RanType),TRange). |
696 | | |
697 | | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks) :- |
698 | | create_optional_subset_check(TDomain,TA,DomCheck), |
699 | | create_optional_subset_check(TRange,TB,RanCheck), |
700 | | append(DomCheck,RanCheck,SetChecks). |
701 | | create_total_domain_range_checks(TDomain,TRange,TA,TB,[TIsTotal|RanCheck]) :- |
702 | | create_texpr(equal(TDomain,TA),pred,[],TIsTotal), |
703 | | create_optional_subset_check(TRange,TB,RanCheck). |
704 | | create_optional_subset_check(TSubset,TSuperset,Check) :- |
705 | | ( is_just_type(TSuperset) -> |
706 | | Check = [] |
707 | | ; otherwise -> |
708 | | create_texpr(subset(TSubset,TSuperset),pred,[],TPred), |
709 | | Check = [TPred]). |
710 | | |
711 | | create_injection_check(TM,TS,TCheckExpr) :- |
712 | | texpr_function_type(TS,FunctionType,DomType,RanType), |
713 | | create_texpr(identifier(d_1),DomType,[],TDomId1), |
714 | | create_texpr(identifier(d_2),DomType,[],TDomId2), |
715 | | create_texpr(identifier(r_1),RanType,[],TRanId), |
716 | | create_texpr(comprehension_set([TDomId1,TRanId],TExists),FunctionType,[bv_function_check(TM)],TCheckExpr), |
717 | | %create_exists([TDomId2],TPred,TExists1), |
718 | | create_texpr(couple(TDomId1,TRanId),couple(DomType,RanType),[],TCouple1), |
719 | | create_texpr(couple(TDomId2,TRanId),couple(DomType,RanType),[],TCouple2), |
720 | | create_texpr(not_equal(TDomId1,TDomId2),pred,[],Unequal), |
721 | | create_texpr(member(TCouple1,TM),pred,[],TMember1), |
722 | | create_texpr(member(TCouple2,TM),pred,[],TMember2), |
723 | | conjunct_predicates([Unequal,TMember1,TMember2],TPred), |
724 | | create_exists([TDomId2],TPred,TExists1), % now also computes used identifiers; cleanup no longer required ? |
725 | | % This is necessary to register the used identifiers |
726 | | clean_up_pred(TExists1,[],TExists). |
727 | | |
728 | | texpr_function_type(TFun,FunType,DomType,RanType) :- |
729 | | get_texpr_type(TFun,set(FunType)), |
730 | | FunType = set(couple(DomType,RanType)). |
731 | | |
732 | | |
733 | | create_bvexpr(Expr,Type,TExpr) :- |
734 | | create_texpr(Expr,Type,[bvisual],TExpr). |
735 | | is_not_bvexpr(TExpr) :- |
736 | | get_texpr_info(TExpr,Infos),nonmember(bvisual,Infos). |
737 | | %is_bvexpr(TExpr) :- get_texpr_info(TExpr,Infos),memberchk(bvisual,Infos). |
738 | | |
739 | | no_empty_set(E) :- \+ is_empty_set(E). |
740 | | |
741 | | is_empty_set(b(E,_,_)) :- is_empty_set_aux(E). |
742 | | is_empty_set_aux(empty_set). |
743 | | is_empty_set_aux(empty_sequence). |
744 | | is_empty_set_aux(value(X)) :- X==[]. |
745 | | |
746 | | get_subformulas(TFormula,Subs,Kind) :- |
747 | | is_texpr(TFormula), |
748 | | get_texpr_expr(TFormula,Formula), |
749 | | subformula_rule(Formula,TFormula,Subs,Kind),!. |
750 | | get_subformulas(TFormula,Subs,syntaxtraversion) :- |
751 | | is_texpr(TFormula),!, |
752 | | syntaxtraversion(TFormula,_,_,_,Subs1,Names), |
753 | | ( Names = [] -> |
754 | | filter_trivial_expressions(Subs1,Subs) |
755 | | ; otherwise -> Subs = []). |
756 | | get_subformulas(textnode(_,Subs),Subs,textnode) :- !. |
757 | | get_subformulas(guard(_Name,Parameters,Guard),Subs,guard) :- !, |
758 | | conjunction_to_list(Guard,GuardSubs), |
759 | | append(Parameters,GuardSubs,Subs). |
760 | | get_subformulas(variant(_Name,_ConvOrAnt,Variant),Subs,variant) :- !, |
761 | | Subs = [Variant]. |
762 | | get_subformulas(guard_theorems(_Name,[],_Guard,Theorems),Subs,guard_theorems) :- !, |
763 | | conjunction_to_list(Theorems,Subs). |
764 | | get_subformulas(guard_theorems(_Name,Parameters,Guard,Theorems),Subs,guard_theorems) :- !, |
765 | | append(Parameters,[b(implication(Guard,Theorems),pred,[])],Subs). |
766 | | %get_subformulas(cbc_path(_,Path,_),Subs) :- !, |
767 | | % append(Path,[X],XPath), |
768 | | % findall(cbc_path(LastStateID,XPath,X), sap:cb_path(LastStateID,XPath,_), Subs). |
769 | | get_subformulas(_,[],none). |
770 | | |
771 | | filter_trivial_expressions([],[]). |
772 | | filter_trivial_expressions([TI|Irest],Out) :- |
773 | | get_texpr_expr(TI,I),get_texpr_info(TI,Info), |
774 | | ( is_trivial(I,Info) -> Out = Orest |
775 | | ; otherwise -> Out = [TI|Orest]), |
776 | | filter_trivial_expressions(Irest,Orest). |
777 | | |
778 | | % is_trivial/2 is true for expressions that should not appear as single nodes |
779 | | % in the evaluation tree, because they are too simple. |
780 | | % The first argument is the expression, the second its information list |
781 | | is_trivial(integer(_),_). |
782 | | is_trivial(integer_set(_),_). |
783 | | is_trivial(empty_set,_). |
784 | | is_trivial(boolean_true,_). |
785 | | is_trivial(boolean_false,_). |
786 | | is_trivial(bool_set,_). |
787 | | is_trivial(truth,_). |
788 | | is_trivial(falsity,_). |
789 | | is_trivial(identifier(_),Info) :- |
790 | | memberchk(given_set,Info). |
791 | | is_trivial(identifier(_),Info) :- |
792 | | memberchk(enumerated_set_element,Info). |
793 | | % TO DO: treat value(_) ? |
794 | | |
795 | | :- use_module(tools_strings,[ajoin/2]). |
796 | | :- use_module(specfile,[animation_minor_mode/1, csp_mode/0, b_or_z_mode/0, get_specification_description/2]). |
797 | | get_node_label(inv,invariants) :- animation_minor_mode(eventb),!. |
798 | | get_node_label(inv,I):- !, get_specification_description(invariant,I). |
799 | | get_node_label(axioms,axioms) :- animation_minor_mode(eventb),!. |
800 | | get_node_label(axioms,S):- !, get_specification_description(properties,S). |
801 | | get_node_label(variants,variants) :- animation_minor_mode(eventb),!. |
802 | | get_node_label(variants,'VARIANT') :- !. % not used there |
803 | | get_node_label(theoremsc,'theorems (on constants)') :- animation_minor_mode(eventb),!. |
804 | | get_node_label(theoremsc,'ASSUME (on constants)') :- animation_minor_mode(tla),!. |
805 | | get_node_label(theoremsc,'ALL ASSERTIONS (on CONSTANTS)') :- b_get_assertion_count(static,AllNr,MainNr), MainNr < AllNr, !. |
806 | | get_node_label(theoremsc,'ASSERTIONS (on CONSTANTS)') :- !. |
807 | | get_node_label(theoremscm,'MAIN ASSERTIONS (on CONSTANTS)') :- !. % should only trigger in B mode at the moment |
808 | | get_node_label(theoremsv,'theorems (on variables)') :- animation_minor_mode(eventb),!. |
809 | | get_node_label(theoremsv,'ALL ASSERTIONS (on VARIABLES)') :- b_get_assertion_count(dynamic,AllNr,MainNr), MainNr < AllNr, !. |
810 | | get_node_label(theoremsv,'ASSERTIONS (on VARIABLES)') :- !. |
811 | | get_node_label(theoremsvm,'MAIN ASSERTIONS (on VARIABLES)') :- !. % should only trigger in B mode at the moment |
812 | | get_node_label(sets,'sets') :- animation_minor_mode(eventb),!. |
813 | | get_node_label(sets,'SETS'). |
814 | | get_node_label(freetypes,'inductive datatypes') :- animation_minor_mode(eventb),!. |
815 | | get_node_label(freetypes,'FREETYPES'). |
816 | | get_node_label(goal,'GOAL'). |
817 | | get_node_label(variables,'variables') :- animation_minor_mode(eventb),!. |
818 | | get_node_label(variables,'VARIABLES'). |
819 | | get_node_label(constants,'constants') :- animation_minor_mode(eventb),!. |
820 | | get_node_label(constants,'CONSTANTS'). |
821 | | get_node_label(guards,'event guards') :- animation_minor_mode(eventb),!. |
822 | | get_node_label(guards,'ACTIONS (guards)') :- animation_minor_mode(tla),!. |
823 | | get_node_label(guards,'OPERATIONS (guards/preconditions)') :- !. % GUARDS/PRE |
824 | | get_node_label(guard_theorems,'theorems (in guards)') :- !. |
825 | | get_node_label(user_formulas,'USER FORMULAS') :- !. |
826 | | get_node_label(definitions,'DEFINITIONS') :- !. |
827 | | %get_node_label(cbc_tests,'CBC_TESTS') :- !. |
828 | | get_node_label(channels,'channel'). |
829 | | get_node_label(datatypes,'datatype'). |
830 | | get_node_label(subtypes,'subtype'). |
831 | | get_node_label(Id,Label) :- |
832 | | stored_formula(Id,Formula), |
833 | | get_node_label2(Formula,Label). |
834 | | |
835 | | get_node_label2(textnode(Text,_),Text) :- !. |
836 | | get_node_label2(bind(TID,_),ID) :- !, |
837 | | (is_texpr(TID),get_texpr_id(TID,R) -> ID = R ; ID = TID). |
838 | | get_node_label2(guard(Name,_Parameters,_Guard),Name) :- !. |
839 | | get_node_label2(guard_theorems(Name,_Parameters,_Guard,_Theorems),Name) :- !. |
840 | | get_node_label2(variant(OpName,ConvOrAnt,_Variant),Name) :- !, |
841 | | ajoin([OpName,' |-> ',ConvOrAnt],Name). |
842 | | get_node_label2(TExpr,Label) :- |
843 | | is_texpr(TExpr),!, |
844 | | bvisual2_translation_mode(Mode), |
845 | | translate_subst_or_bexpr_in_mode(Mode,TExpr,Label). % use unicode, latex or ascii; but unicode_mode makes Viewer very slow |
846 | | get_node_label2(Term,Label) :- |
847 | | functor(Term,F,Arity), |
848 | | ajoin(['unknown node type: ',F,'/',Arity],Label). |
849 | | |
850 | | :- dynamic bvisual2_translation_mode/1. |
851 | | bvisual2_translation_mode(unicode). % or ascii or latex |
852 | | set_bvisual2_translation_mode(X) :- retractall(bvisual2_translation_mode(_)), |
853 | | assert(bvisual2_translation_mode(X)). |
854 | | |
855 | | |
856 | | register_top_level :- register_top_level(_). |
857 | | register_top_level(Id) :- |
858 | ? | top_level2(Id,Formula,Subs), % print(register(Id,Subs)),nl, |
859 | | register_top_level_formula(Id,Formula,Subs), |
860 | | fail. |
861 | | register_top_level(_Id). |
862 | | |
863 | | |
864 | | :- use_module(specfile,[b_or_z_mode/0]). |
865 | | :- use_module(b_global_sets,[all_elements_of_type/2]). |
866 | | :- use_module(bmachine,[b_get_machine_goal/1]). |
867 | | :- use_module(specfile,[spec_file_has_been_successfully_loaded/0]). |
868 | | b_or_z_successsful_mode :- b_or_z_mode, |
869 | | true. %spec_file_has_been_successfully_loaded. % make unit test fail |
870 | | |
871 | | top_level2(variables,textnode('',Variables),Variables) :- b_or_z_successsful_mode, |
872 | | variables_should_be_included, |
873 | | b_get_machine_variables(Variables). |
874 | | top_level2(constants,textnode('',Constants),Constants) :- b_or_z_successsful_mode, |
875 | | variables_should_be_included, |
876 | | b_get_machine_constants(Constants). |
877 | | top_level2(sets,textnode('',Sets),Sets) :- b_or_z_successsful_mode, |
878 | | findall(bind(S,All), |
879 | | top_level_set(S,All),Sets), Sets \= []. |
880 | | top_level2(freetypes,textnode('',Sets),Sets) :- b_or_z_successsful_mode, |
881 | | findall(bind(S,All), top_level_freetype(S,All),Sets), Sets \= []. |
882 | | top_level2(goal,Goal,Subs) :- b_or_z_successsful_mode, |
883 | | b_get_machine_goal(Goal), |
884 | | conjunction_to_list(Goal,Subs). |
885 | | top_level2(inv,Invariant,Subs) :- b_or_z_successsful_mode, |
886 | | b_get_invariant_from_machine(Invariant), |
887 | | conjunction_to_list(Invariant,Subs). |
888 | | top_level2(variants,textnode('',Variants),Variants) :- animation_minor_mode(eventb), |
889 | | spec_file_has_been_successfully_loaded, |
890 | | findall(variant(Name,ConvOrAnt,Variant), |
891 | | b_get_operation_variant(Name,ConvOrAnt,Variant), |
892 | | Variants), |
893 | | Variants = [_|_]. |
894 | | top_level2(axioms,Props,Subs) :- b_or_z_successsful_mode, |
895 | | b_machine_has_constants_or_properties, |
896 | | b_get_properties_from_machine(Props), |
897 | | conjunction_to_list(Props,Subs). |
898 | | top_level2(theoremsc,Pred,Assertions) :- b_or_z_successsful_mode, |
899 | | b_get_static_assertions_from_machine(Assertions),Assertions\=[], |
900 | | conjunct_predicates(Assertions,Pred). |
901 | | top_level2(theoremscm,Pred,Assertions) :- b_or_z_successsful_mode, |
902 | | b_get_assertions_from_main_machine(static,Assertions), |
903 | | %Assertions\=[], % in case we have less: show that there are none |
904 | | b_get_assertion_count(static,AllNr,MainNr), MainNr < AllNr, |
905 | | conjunct_predicates(Assertions,Pred). |
906 | | top_level2(theoremsv,Pred,Assertions) :- b_or_z_successsful_mode, |
907 | | b_get_dynamic_assertions_from_machine(Assertions),Assertions\=[], |
908 | | conjunct_predicates(Assertions,Pred). |
909 | | top_level2(theoremsvm,Pred,Assertions) :- b_or_z_successsful_mode, |
910 | | b_get_assertions_from_main_machine(dynamic,Assertions), |
911 | | %Assertions\=[], % in case we have less: show that there are none |
912 | | b_get_assertion_count(dynamic,AllNr,MainNr), MainNr < AllNr, |
913 | | conjunct_predicates(Assertions,Pred). |
914 | | top_level2(guards,textnode('',EventGuards),EventGuards) :- b_or_z_successsful_mode, |
915 | | findall(guard(Name,Params,Guard), |
916 | | get_guard(Name,Params,Guard),EventGuards), |
917 | | EventGuards = [_|_]. |
918 | | top_level2(guard_theorems,textnode('',EventGuards),EventGuards) :- b_or_z_successsful_mode, |
919 | | findall(guard_theorems(Name,Params,Guard,GuardTheorems), |
920 | | ( b_get_machine_operation(Name,_,_,TBody), |
921 | | get_texpr_expr(TBody,Body), |
922 | | Body = rlevent(_Name,_Section,_Status,Params,Guard,Theorems, |
923 | | _Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents), |
924 | | Theorems \= [], |
925 | | conjunct_predicates(Theorems,GuardTheorems) |
926 | | ), |
927 | | EventGuards), |
928 | | EventGuards = [_|_]. |
929 | | top_level2(user_formulas,textnode('',UserPredicates),UserPredicates) :- b_or_z_successsful_mode, |
930 | | findall(UP,subnode(user_formulas,UP),UserPredicates), UserPredicates\=[]. |
931 | | top_level2(definitions,textnode('',Defs),Defs) :- b_or_z_successsful_mode, |
932 | | findall(Node,get_definition(Node),Defs), Defs\=[]. |
933 | | top_level2(channels,textnode('',Channels),Channels) :- csp_mode, spec_file_has_been_successfully_loaded, |
934 | | findall(Node,get_csp_channel(Node),Cs), Cs\=[], sort(Cs,Channels). |
935 | | top_level2(datatypes,textnode('',DT),DT) :- csp_mode, spec_file_has_been_successfully_loaded, |
936 | | findall(Node,get_csp_datatype(Node),Cs), Cs\=[], sort(Cs,DT). |
937 | | top_level2(subtypes,textnode('',DT),DT) :- csp_mode, spec_file_has_been_successfully_loaded, |
938 | | findall(Node,get_csp_subtype(Node),Cs), Cs\=[], sort(Cs,DT). |
939 | | % we are now using a custom tree_inspector for the CBC Tests |
940 | | /* top_level2(cbc_tests,textnode('',Paths),Paths) :- b_or_z_mode, |
941 | | get_preference(user_is_an_expert_with_accessto_source_distribution,true), |
942 | | %sap:cb_path(_,[_],_), % we have generated at least one test-case |
943 | | % TO DO: we need a way to refresh this information after test-cases have been generated |
944 | | % currently the only way seems to close the evaluation view, reload, generate the tests and then open the view |
945 | | Paths = [cbc_path(root,[],'INITIALISATION')]. |
946 | | */ |
947 | | |
948 | | :- use_module(probcspsrc(haskell_csp),[channel_type_list/2, dataTypeDef/2, subTypeDef/2]). |
949 | | :- use_module(translate,[translate_cspm_expression/2]). |
950 | | get_csp_channel(bind(Channel,string(TypeString))) :- |
951 | | channel_type_list(Channel,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] |
952 | | translate_cspm_expression(dotTuple(TypeList),TypeString). |
953 | | get_csp_datatype(bind(DT,string(TypeString))) :- |
954 | | dataTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] |
955 | | translate_cspm_expression(dataTypeDef(TypeList),TypeString). |
956 | | get_csp_subtype(bind(DT,string(TypeString))) :- |
957 | | subTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] |
958 | | translate_cspm_expression(dataTypeDef(TypeList),TypeString). |
959 | | |
960 | | :- use_module(bmachine). |
961 | | :- use_module(pref_definitions,[b_get_set_pref_definition/3]). |
962 | | get_definition(textnode('GOAL',Subs)) :- b_get_machine_goal(Goal), conjunction_to_list(Goal,Subs). |
963 | | get_definition(bind('SCOPE',string(S))) :- b_get_machine_searchscope(S). |
964 | | get_definition(textnode('HEURISTIC_FUNCTION',[F])) :- b_get_machine_heuristic_function(F). |
965 | | get_definition(textnode('ANIMATION_EXPRESSION',[F])) :- b_get_machine_animation_expression(F). |
966 | | get_definition(textnode(Name,[F])) :- b_get_machine_animation_function(F,Nr), |
967 | | number_codes(Nr,NC), append("ANIMATION_FUNCTION",NC,C), atom_codes(Name,C). |
968 | | get_definition(textnode(Name,[Term])) :- b_get_machine_setscope(SetName,Term), |
969 | | atom_codes(SetName,NC), append("scope_",NC,C), atom_codes(Name,C). |
970 | | get_definition(textnode(Name,[b(integer(Nr),integer,[])])) :- b_get_machine_operation_max(OpName,Nr), |
971 | | atom_codes(OpName,NC), append("MAX_OPERATIONS_",NC,C), atom_codes(Name,C). |
972 | | get_definition(bind(Name,string(F))) :- |
973 | | b_get_definition_string_from_machine(Name,F), atom_codes(Name,C), \+ append("SET_PREF_",_,C). |
974 | | get_definition(Res) :- |
975 | ? | b_get_set_pref_definition(DefName,_String,F), |
976 | ? | (extract_value(F,Val) -> Res = bind(DefName,Val) ; Res = textnode(DefName,[F])). |
977 | | |
978 | | extract_value(b(string(S),_,_),string(S)). |
979 | | extract_value(b(integer(S),_,_),int(S)). |
980 | | extract_value(b(boolean_true,_,_),pred_true). |
981 | | extract_value(b(boolean_false,_,_),pred_false). |
982 | | |
983 | | :- use_module(predicate_debugger,[get_unsimplified_operation_enabling_condition/5]). |
984 | | get_guard(OpName,Params,Guard) :- |
985 | ? | get_unsimplified_operation_enabling_condition(OpName,Params,Guard,_BecomesSuchVars,_Precise), |
986 | | \+ is_initialisation_op(OpName). |
987 | | |
988 | | is_initialisation_op('$setup_constants'). |
989 | | is_initialisation_op('$initialise_machine'). |
990 | | |
991 | | :- use_module(custom_explicit_sets,[construct_interval_closure/3]). |
992 | | :- use_module(kernel_freetypes,[registered_freetype/2]). |
993 | | :- use_module(bmachine,[b_get_machine_set/2]). |
994 | ? | top_level_set(TSet,AllEls) :- b_or_z_mode, |
995 | ? | b_get_machine_set(Set,TSet), |
996 | | all_elements_of_type(Set,AllEls). |
997 | | top_level_set('INT',INTVAL) :- % we can return both typed ids and atomic ids |
998 | | b_or_z_mode, |
999 | | \+ animation_minor_mode(_), % INT only exists in pure B mode |
1000 | | get_preference(maxint,MAXINT), get_preference(minint,MININT), |
1001 | | construct_interval_closure(MININT,MAXINT,INTVAL). |
1002 | | |
1003 | | top_level_freetype(Set,AllCases) :- |
1004 | | animation_minor_mode(eventb), % here types contain Prolog variables (polymorphism) + we have the constant(_) type |
1005 | | registered_freetype(SetP,Cases), |
1006 | | functor(SetP,Set,_), |
1007 | | %print(cases(Cases)),nl, |
1008 | | findall(string(CaseString), |
1009 | | (member(case(CaseP,T),Cases),functor(CaseP,Case,_), %print(t(T)),nl, |
1010 | | translate:pretty_type(T,TS), tools:ajoin([Case,':',TS],CaseString) |
1011 | | ),AllCases). |
1012 | | top_level_freetype(Set,AllCases) :- b_or_z_mode, \+ animation_minor_mode(eventb), |
1013 | | registered_freetype(Set,Cases), |
1014 | | % TO DO: improve presentation, maybe use translate:type_set(_Type,TDom); we also have constant(_) type here |
1015 | | findall(field(Case,closure(['_zzzz_unary'],[T],b(truth,pred,[]))), |
1016 | | member(case(Case,T),Cases), |
1017 | | Fields), |
1018 | | AllCases = struct(Fields). |
1019 | | |
1020 | | register_top_level_formula(Id,Formula,Subs) :- |
1021 | | assert( stored_formula(Id,Formula) ), |
1022 | | register_formulas(Subs,Id,_), |
1023 | | assert( top_level_node(Id) ), |
1024 | | assert( expanded(Id) ). |
1025 | | |
1026 | | register_formulas([],_Parent,[]). |
1027 | | register_formulas([Formula|Frest],Parent,[SubId|Srest]) :- |
1028 | | register_formula(Formula,Parent,SubId), |
1029 | | register_formulas(Frest,Parent,Srest). |
1030 | | register_formula(Formula,Parent,Id) :- |
1031 | | get_new_id(Id), |
1032 | | assert( stored_formula(Id,Formula) ), |
1033 | | assert( subnode(Parent,Id) ), |
1034 | | assert( supernode(Id,Parent) ). |
1035 | | |
1036 | | get_new_id(Id) :- |
1037 | | ( retract( id_counter(Old) ) -> true |
1038 | | ; otherwise -> Old = 0), |
1039 | | Id is Old+1, |
1040 | | assert( id_counter(Id) ). |
1041 | | |
1042 | | |
1043 | | disjunction_to_list(A,B,Out) :- |
1044 | | disjunction_to_list2(A,[B],Out,[]). |
1045 | | disjunction_to_list2(Expr,Rest) --> |
1046 | | {get_texpr_expr(Expr,disjunct(A,B)),!}, |
1047 | | disjunction_to_list2(A,[B|Rest]). |
1048 | | disjunction_to_list2(Expr,Rest) --> |
1049 | | [Expr],disjunction_to_list3(Rest). |
1050 | | disjunction_to_list3([]) --> !. |
1051 | | disjunction_to_list3([H|T]) --> disjunction_to_list2(H,T). |
1052 | | |
1053 | | |
1054 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1055 | | % some predicates for the support of the Tcl/Tk UI |
1056 | | |
1057 | | :- meta_predicate call_with_temp_preference(*,*,0). |
1058 | | call_with_temp_preference(Prefs,Values,Call) :- |
1059 | | maplist(get_preference,Prefs,OldValues), |
1060 | | maplist(set_preference,Prefs,Values), |
1061 | | call_cleanup(Call,maplist(set_preference,Prefs,OldValues)),!. |
1062 | | |
1063 | | bv_get_value_unlimited(Id,StateId,Value) :- |
1064 | | visited_expression(StateId,State),!, |
1065 | | get_preference(time_out,Timeout), |
1066 | | assert(get_unlimited_value), |
1067 | | call_cleanup(call_with_temp_preference([expand_avl_upto],[-1],bv_get_value(Id,State,StateId,Timeout,Value)), |
1068 | | retractall(get_unlimited_value)). |
1069 | | bv_get_value_unlimited(_Id,_StateId,e('unknown state')). |
1070 | | |
1071 | | bv_get_value_unlimited_and_unprocessed(Id,StateId,Value) :- |
1072 | | visited_expression(StateId,State),!, |
1073 | | get_preference(time_out,Timeout), |
1074 | | call_with_temp_preference([expand_avl_upto],[-1],bv_get_value_unprocessed(Id,State,StateId,Timeout,Value)). |
1075 | | bv_get_value_unlimited_and_unprocessed(_Id,_StateId,e('unknown state')). |
1076 | | |
1077 | | :- use_module(tools_commands,[edit_file/2]). |
1078 | | :- use_module(probsrc(error_manager),[extract_file_line_col/6,extract_span_description/2]). |
1079 | | bv_show_formula_origin(Id,Desc) :- |
1080 | | bv_get_stored_formula_expr(Id,Formula), |
1081 | | extract_file_line_col(Formula,FILE,LINE,_COL,_Erow,_Ecol), |
1082 | | extract_span_description(Formula,Desc), |
1083 | | edit_file(FILE,LINE). |
1084 | | |
1085 | | :- use_module(probsrc(bsyntaxtree),[get_texpr_description/2]). |
1086 | | bv_formula_description(Id,Desc) :- |
1087 | | bv_get_stored_formula_expr(Id,Formula), |
1088 | | is_texpr(Formula), |
1089 | | get_texpr_description(Formula,Desc). |
1090 | | % ; Desc = 'No description available via @desc pragma'). |
1091 | | |
1092 | | bv_is_typed_formula(Id) :- bv_get_stored_formula_expr(Id,Formula), is_texpr(Formula). |
1093 | | bv_is_typed_predicate(Id) :- bv_get_stored_formula_expr(Id,Formula), Formula = b(_,pred,_). |
1094 | | bv_is_typed_identifier(Id,IDName) :- bv_get_stored_formula_expr(Id,Formula), Formula = b(identifier(IDName),_,_). |
1095 | | |
1096 | | bv_get_stored_formula_expr(Id,Formula) :- |
1097 | | stored_formula(Id,Stored), |
1098 | | extract_typed_formua(Stored,Formula). |
1099 | | |
1100 | | extract_typed_formua(bind(LHS,_),Formula) :- !, Formula=LHS. |
1101 | | extract_typed_formua(guard(_Name,Parameters,Guard),Formula) :- !, get_guard_formula(Parameters,Guard,Formula). |
1102 | | extract_typed_formua(variant(_Name,_ConvOrAnt,Variant),Formula) :- !, Formula=Variant. |
1103 | | extract_typed_formua(TF,TF). |
1104 | | |
1105 | | get_guard_formula([],Guard,Res) :- !, Res=Guard. |
1106 | | get_guard_formula(Parameters,Guard,Expr) :- create_exists(Parameters,Guard,Expr). |
1107 | | get_guard_theorems_formula([],_Guard,Theorems,Res) :- !, Res=Theorems. |
1108 | | get_guard_theorems_formula(Parameters,Guard,Theorems,Expr) :- |
1109 | | create_forall(Parameters,b(implication(Guard,Theorems),pred,[]),Expr). |
1110 | | |
1111 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1112 | | % |
1113 | | :- use_module(tools_io). |
1114 | | bv_print_to_file(IdList,StateId,Filename) :- |
1115 | | call_with_temp_preference([expand_avl_upto],[-1],bv_print_to_file_aux(IdList,StateId,Filename)). |
1116 | | bv_print_to_file_aux(IdList,StateId,Filename) :- |
1117 | | safe_open_file(Filename,write,S,[]), |
1118 | | bv_print_to_stream_l(IdList,S,StateId,false), |
1119 | | close(S). |
1120 | | |
1121 | | bv_print_to_stream_l([],_S,_StateId,_WriteAnd). |
1122 | | bv_print_to_stream_l([Id|Rest],S,StateId,WriteAnd) :- |
1123 | | bv_print_to_stream(Id,S,StateId,OutType,WriteAnd), |
1124 | | ( OutType=predicate -> WriteAnd2=true |
1125 | | ; otherwise -> WriteAnd2=WriteAnd), |
1126 | | bv_print_to_stream_l(Rest,S,StateId,WriteAnd2). |
1127 | | |
1128 | | bv_print_to_stream(Id,S,StateId,predicate,WriteAnd) :- |
1129 | | stored_formula(Id,Formula), |
1130 | | bv_print_formula_to_stream(Formula,Id,S,StateId,WriteAnd),!,nl(S). |
1131 | | bv_print_to_stream(Id,S,StateId,other,_WriteAnd) :- |
1132 | | get_node_label(Id,Label), |
1133 | | bv_get_values([Id],StateId,[Value]), |
1134 | | write(S,'/* '),write(S,Label),write(S,': '), |
1135 | | bv_print_std_value(Value,S),write(S,' */\n'). |
1136 | | bv_print_std_value(e(Msg),S) :- write(S,'ERROR( '), write(S,Msg), write(S,' )'). |
1137 | | bv_print_std_value(p(Value),S) :- write(S,Value). |
1138 | | bv_print_std_value(v(Value),S) :- write(S,Value). |
1139 | | bv_print_std_value(i,S) :- write(S,'INACTIVE'). |
1140 | | |
1141 | | bv_print_formula_to_stream(Formula,Id,S,StateId,WriteAnd) :- |
1142 | | is_texpr(Formula), |
1143 | | get_texpr_type(Formula,Type), |
1144 | | bv_get_value_unlimited_and_unprocessed(Id,StateId,Value), |
1145 | | bv_print_formula_to_stream2(Type,Formula,Value,S,WriteAnd). |
1146 | | |
1147 | | bv_print_formula_to_stream2(pred,Formula,p(Value),S,WriteAnd) :- !, |
1148 | | bv_print_predicate_to_stream(Value,Formula,S,WriteAnd). |
1149 | | bv_print_formula_to_stream2(Type,Formula,btvalue(Value,_),S,WriteAnd) :- !, |
1150 | | create_texpr(value(Value),Type,[],TValue), |
1151 | | create_texpr(equal(Formula,TValue),pred,[],Equal), |
1152 | | write_bexpression(S,Equal,WriteAnd). |
1153 | | |
1154 | | bv_print_predicate_to_stream(true,Formula,S,WriteAnd) :- |
1155 | | write_bexpression(S,Formula,WriteAnd). |
1156 | | bv_print_predicate_to_stream(false,Formula,S,WriteAnd) :- |
1157 | | create_texpr(negation(Formula),pred,[],NegatedFormula), |
1158 | | write(S,' /* FALSE */ '),write_bexpression(S,NegatedFormula,WriteAnd). |
1159 | | |
1160 | | write_bexpression(Stream,Expression,WriteAnd) :- |
1161 | | ( WriteAnd = true -> write(Stream,' & \n') |
1162 | | ; otherwise -> true), |
1163 | | translate_bexpression_to_codes(Expression,Codes), |
1164 | | put_codes(Codes,Stream). |
1165 | | |
1166 | | bv_write_all_variables_and_constants(StateId,Filename) :- |
1167 | | call_with_temp_preference([expand_avl_upto],[-1],bv_write_all_variables_and_constants_aux(StateId,Filename)). |
1168 | | bv_write_all_variables_and_constants_aux(StateId,Filename) :- |
1169 | | bv_expand_formula(constants,_CLabel,ConstNodes), |
1170 | | bv_expand_formula(variables,_VLabel,VarNodes), |
1171 | | append(ConstNodes,VarNodes,Subnodes),expand_all(Subnodes), |
1172 | | append([constants|ConstNodes],[variables|VarNodes],Nodes), |
1173 | | bv_print_to_file(Nodes,StateId,Filename). |
1174 | | expand_all(Subnodes) :- |
1175 | | member(Node,Subnodes), |
1176 | | bv_expand_formula(Node,_,_), |
1177 | | fail. |
1178 | | expand_all(_Subnodes). |
1179 | | |
1180 | | |
1181 | | :- use_module(eventhandling,[register_event_listener/3]). |
1182 | | :- register_event_listener(clear_specification,clear_bvisual, |
1183 | | 'Clear module bvisual2.'). |
1184 | | :- register_event_listener(specification_initialised,reset_bvisual, |
1185 | | 'Initialise module bvisual2.'). |
1186 | | :- register_event_listener(change_of_animation_mode,reset_bvisual, |
1187 | | 'Initialise module bvisual2.'). |
1188 | | |
1189 | | :- use_module(self_check). |
1190 | | % a very small use-case: |
1191 | | :- assert_must_succeed(( |
1192 | | reset_bvisual, |
1193 | | bv_get_top_level(T), %print(top(T)),nl, |
1194 | | %T == [variables,constants,inv], |
1195 | | member(inv,T), |
1196 | | bv_expand_formula(inv,Text,Sub), |
1197 | | %print(expand(Text,Sub)),nl, |
1198 | | Text == 'INVARIANT', |
1199 | | Sub = [H|_], |
1200 | | bv_expand_formula(H,_Text1,_Sub1), |
1201 | | %print(expand1(Text1,Sub1)),nl, |
1202 | | bv_get_values(Sub,root,Values), |
1203 | | %print(values(Values)),nl, % should be [i,...] or e('unknown state') |
1204 | | Values = [VI|_], (VI=i ; VI=e(_)), |
1205 | | reset_bvisual |
1206 | | )). |
1207 | | |
1208 | | % example bv_get_top_level_formula(theoremsc,Txt,Labels,Vals) |
1209 | | |
1210 | | bv_get_top_level_formula(Category,CatText,Labels,Values) :- |
1211 | | current_state_id(StateId), |
1212 | | bv_get_top_level_formula(Category,CatText,StateId,Labels,Values). |
1213 | | bv_get_top_level_formula(Category,CatText,StateId,Labels,Values) :- |
1214 | | bv_get_top_level(TL), |
1215 | | member(Category,TL), |
1216 | | bv_expand_formula(Category,CatText,Subs), |
1217 | | maplist(get_node_label,Subs,Labels), |
1218 | | bv_get_values(Subs,StateId,Values). |
1219 | | |
1220 | | % ------------------------------------ |
1221 | | |
1222 | | % provide HTML output of operation guards upto MaxLevel |
1223 | | % TO DO: provide option to provide parameter values, output to Latex,... |
1224 | | html_debug_operation_for_stateid(Stream,OpName,StateId,MaxLevel) :- |
1225 | | stored_formula(Id,guard(OpName,_,_)), |
1226 | | enter_level(Stream,0), |
1227 | | traverse(Stream,StateId,0,MaxLevel,Id), |
1228 | | exit_level(Stream,0). |
1229 | | |
1230 | | :- use_module(tools,[html_escape/2]). |
1231 | | traverse(_,_StateId,Level,MaxLevel,_Id) :- Level>MaxLevel,!. |
1232 | | traverse(Stream,StateId,Level,MaxLevel,Id) :- |
1233 | | bv_expand_formula(Id,Label,Children), html_escape(Label,ELabel), |
1234 | | bv_get_values([Id],StateId,[Value]), |
1235 | | translate_value(Value,ValueS), html_escape(ValueS,EValueS), |
1236 | | % format('~w : ~w = ~w [~w] (level ~w)~n',[Id,Label,Value,ValueS,Level]), |
1237 | | stored_formula(Id,Formula), |
1238 | | (color_based_on_value(Value,Col) -> format(Stream,'<font color="~w">',[Col]) ; true), |
1239 | | (Formula = guard(_,_,_) |
1240 | | -> format(Stream,'<li>Guard of ~w = ~w</li>~n',[ELabel,EValueS]) |
1241 | | ; format(Stream,'<li>~w = ~w</li>~n',[ELabel,EValueS]) |
1242 | | ), |
1243 | | (color_based_on_value(Value,_) -> format(Stream,'</font>',[]) ; true), |
1244 | | (Level < MaxLevel |
1245 | | -> L1 is Level+1, |
1246 | | enter_level(Stream,L1), |
1247 | | maplist(traverse(Stream,StateId,L1,MaxLevel),Children), |
1248 | | exit_level(Stream,L1) |
1249 | | ; true). |
1250 | | |
1251 | | color_based_on_value(p(false),'INDIANRED'). |
1252 | | color_based_on_value(p(true),'DARKGREEN'). |
1253 | | color_based_on_value(e(_),red). |
1254 | | color_based_on_value(i,gray). |
1255 | | |
1256 | | enter_level(Stream,L1) :- indent_ws(Stream,L1), format(Stream,'<ul>~n',[]). |
1257 | | exit_level(Stream,L1) :- indent_ws(Stream,L1), format(Stream,'</ul>~n',[]). |
1258 | | |
1259 | | indent_ws(_,X) :- X<1,!. |
1260 | | indent_ws(Stream,X) :- write(Stream,' '), X1 is X-1, indent_ws(Stream,X1). |
1261 | | |
1262 | | |
1263 | | translate_value(p(V),R) :- !,R=V. |
1264 | | translate_value(v(V),R) :- R=V. |
1265 | | translate_value(e(M),R) :- !, ajoin(['ERROR(',M,')'],R). |
1266 | | translate_value(i,R) :- !, R='INACTIVE'. |
1267 | | translate_value(V,V). |
1268 | | |
1269 | | % -------------------------------- |
1270 | | |
1271 | | :- use_module(probsrc(error_manager),[add_error/3]). |
1272 | | :- use_module(probsrc(bmachine),[b_parse_machine_predicate_from_codes_open/5, b_parse_machine_formula_from_codes/7]). |
1273 | | tcltk_register_new_user_formula(F) :- tcltk_register_new_user_formula(formula,F). |
1274 | | tcltk_register_new_user_formula(Kind,F) :- |
1275 | | atom_codes(F,Codes), |
1276 | | TypingScope=[prob_ids(visible),variables], |
1277 | | (Kind=open_predicate |
1278 | | -> b_parse_machine_predicate_from_codes_open(exists,Codes,[],TypingScope,Typed) |
1279 | | ; b_parse_machine_formula_from_codes(Kind,Codes,TypingScope,Typed,_Type,true,Error) |
1280 | | ), |
1281 | | (Error=none -> true |
1282 | | ; add_error(tcltk_register_new_user_formula,'Error occured while parsing formula: ',Error),fail), |
1283 | | bv_insert_formula(Typed,user_formulas,_), |
1284 | | (top_level_node(user_formulas) -> true ; register_top_level(user_formulas) ). |
1285 | | %retractall(expanded(user_formulas)), |
1286 | | %bv_insert_formula(Typed,user,_),. |
1287 | | |
1288 | | % -------------------------------- |
1289 | | |
1290 | | |