1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | ||
6 | :- module(bvisual2,[ %reset_bvisual/0, | |
7 | bv_get_top_level/1 | |
8 | , bv_expand_formula/3 % also used to get string of entry | |
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_get_values_unlimited/3 | |
15 | , bv_is_explanation_node/1 | |
16 | , bv_print_to_file/3 | |
17 | , bv_write_all_variables_and_constants/2 | |
18 | , set_bvisual2_translation_mode/1 | |
19 | , bvisual2_translation_mode/1 | |
20 | , bv_get_top_level_formula/4 | |
21 | , bv_get_top_level_formula/5 | |
22 | , bv_value_to_atom/2 | |
23 | , bv_show_formula_origin/2 | |
24 | , bv_formula_description/2 | |
25 | , bv_formula_extended_description/2 | |
26 | , bv_formula_discharged_info/2 | |
27 | , bv_get_formula_functor_symbol/2 | |
28 | , bv_get_btvalue/4 | |
29 | , bv_is_child_formula/1 | |
30 | , bv_formula_labels/2 | |
31 | , bv_is_typed_formula/1 | |
32 | , bv_is_typed_predicate/1 | |
33 | , bv_is_typed_identifier/2 | |
34 | , bv_get_stored_formula_expr/2 | |
35 | , tcltk_register_new_user_formula/1 | |
36 | , html_debug_operation_for_stateid/4 | |
37 | , bv_top_level_set/2 | |
38 | ]). | |
39 | ||
40 | :- meta_predicate bv_time_out_call(0,-,-,-). | |
41 | :- meta_predicate call_with_temp_preference(*,*,0). | |
42 | :- meta_predicate with_bvisual2_translation_mode(0). | |
43 | ||
44 | :- use_module(probsrc(module_information),[module_info/2]). | |
45 | :- module_info(group,ast). | |
46 | :- module_info(description,'This module contains functionality to analyse B expressions and predicates by evaluating and decomposing them into substructures.'). | |
47 | ||
48 | :- use_module(library(lists)). | |
49 | :- use_module(library(codesio)). | |
50 | %:- use_module(library(timeout)). | |
51 | ||
52 | :- use_module(probsrc(bmachine), [ b_machine_has_constants_or_properties/0 | |
53 | , b_get_machine_variables_in_original_order/1 | |
54 | , b_get_machine_constants/1 | |
55 | , b_get_machine_operation/4 | |
56 | , b_get_properties_from_machine/1 | |
57 | , b_machine_additional_property/1 | |
58 | , get_invariant_list_with_proof_info/1 | |
59 | , b_get_static_assertions_from_machine/1 | |
60 | , b_get_assertions_from_main_machine/2 | |
61 | , b_get_dynamic_assertions_from_machine/1 | |
62 | , b_get_assertion_count/3 | |
63 | , b_get_operation_variant/3 | |
64 | , b_get_operation_description/2 | |
65 | ]). | |
66 | :- use_module(probsrc(specfile),[ state_corresponds_to_initialised_b_machine/2 | |
67 | , state_corresponds_to_set_up_constants/2 | |
68 | ]). | |
69 | :- use_module(probsrc(state_space), [ visited_expression/2 | |
70 | , current_state_id/1 | |
71 | , invariant_not_yet_checked/1 | |
72 | , invariant_violated/1 | |
73 | , transition/3 | |
74 | ]). | |
75 | :- use_module(probsrc(store),[ empty_state/1 | |
76 | , normalise_store/2 | |
77 | ]). | |
78 | :- use_module(probsrc(b_interpreter),[ | |
79 | b_not_test_boolean_expression_cs/5 | |
80 | , b_test_boolean_expression_for_ground_state/5 | |
81 | , b_test_boolean_expression/4 | |
82 | , b_compute_expression_nowf/6 | |
83 | , set_up_typed_localstate/6 | |
84 | , properties_were_filtered/1 | |
85 | ]). | |
86 | :- use_module(probsrc(translate),[ translate_bexpression_to_codes/2 | |
87 | , translate_subst_or_bexpr_with_limit/3 | |
88 | , get_texpr_top_level_symbol/4 | |
89 | , translate_bvalue_for_expression_with_limit/4 | |
90 | , translate_bvalue_for_expression/3 | |
91 | , translate_bvalue_with_type_and_limit/4 | |
92 | , translate_bvalue/2 | |
93 | , translate_any_state/2 | |
94 | , translate_prolog_exception/2 | |
95 | , translate_eventb_direct_definition_header/3 | |
96 | , translate_eventb_direct_definition_body/2 | |
97 | ]). | |
98 | :- use_module(probsrc(bsyntaxtree),[ get_texpr_expr/2 | |
99 | , get_texpr_type/2 | |
100 | , get_texpr_info/2 | |
101 | , get_texpr_id/2 | |
102 | , is_texpr/1 | |
103 | , create_texpr/4 | |
104 | , safe_create_texpr/3 | |
105 | , syntaxtraversion/6 | |
106 | , conjunction_to_list/2 | |
107 | , conjunct_predicates/2 | |
108 | , create_exists/3 | |
109 | , create_or_merge_exists/3 | |
110 | , create_forall/3 | |
111 | , texpr_contains_wd_condition/1 | |
112 | %, find_identifier_uses/3 | |
113 | ]). | |
114 | :- use_module(probsrc(b_ast_cleanup),[ clean_up_pred/3 | |
115 | ]). | |
116 | :- use_module(probsrc(error_manager),[ get_all_errors_and_clear/1 | |
117 | , time_out_with_enum_warning_one_solution/3 | |
118 | ]). | |
119 | :- use_module(probsrc(preferences), [ get_preference/2 | |
120 | , set_preference/2 | |
121 | ]). | |
122 | :- use_module(probsrc(kernel_waitflags), [ init_wait_flags_with_call_stack/2 | |
123 | , ground_wait_flags/1]). | |
124 | :- use_module(probsrc(b_enumerate),[ b_tighter_enumerate_values_in_ctxt/3 ]). | |
125 | :- use_module(probsrc(tools_files),[ put_codes/2]). | |
126 | :- use_module(probsrc(tools_strings),[ strip_newlines/2]). | |
127 | :- use_module(probltlsrc(ltl),[get_ltl_formula_strings/2]). % did lead to SPIO_E_TOO_MANY_OPEN_FILES | |
128 | :- use_module(probltlsrc(ltl_translate),[pp_ltl_formula/2, get_ltl_sub_formulas/3]). | |
129 | :- use_module(probltlsrc(ltl_propositions), [is_atomic_ltl_property/1, check_atomic_property_formula/2]). | |
130 | :- use_module(probltlsrc(ltl_tools),[temporal_parser/3]). | |
131 | ||
132 | :- use_module(probsrc(bmachine_eventb), [ stored_operator_direct_definition/8]). | |
133 | :- use_module(probsrc(debug), [debug_format/3, debug_mode/1]). | |
134 | ||
135 | :- set_prolog_flag(double_quotes, codes). | |
136 | ||
137 | :- dynamic top_level_node/1, subnode/2, supernode/2. | |
138 | :- dynamic stored_formula/2, expanded/1, explanation_parent/1. | |
139 | :- dynamic id_counter/1. | |
140 | :- dynamic formula_cache/3. | |
141 | % We store the information whether a node can introduce new values as an (counter-)example | |
142 | % in example_node/1; the value is computed in explore_node/2. | |
143 | % For such nodes, the found examples are stored in local_state/3. | |
144 | :- dynamic example_node/1,local_state/3. | |
145 | ||
146 | ||
147 | ||
148 | bv_value_to_atom(p(P),R) :- !, % a predicate value | |
149 | (P=true -> R='TRUE' ; P=false -> R='FALSE' ; R=P). | |
150 | bv_value_to_atom(e(_),R) :- !, R='ERROR'. | |
151 | bv_value_to_atom(v(V),R) :- !, R=V. % a value, already pretty-printed !?? | |
152 | bv_value_to_atom(i,R) :- !, R='INACTIVE'. | |
153 | bv_value_to_atom(bv_info(V),R) :- !, R=V. | |
154 | bv_value_to_atom(V,V). | |
155 | ||
156 | ||
157 | :- dynamic variables_should_be_included/0. | |
158 | variables_should_be_included. | |
159 | %bv_include_variables :- | |
160 | % (variables_should_be_included -> true ; assertz(variables_should_be_included)). | |
161 | ||
162 | clear_bvisual :- | |
163 | retractall(top_level_node(_)), | |
164 | retractall(subnode(_,_)), % TO DO: do not delete user formulas for a simple re-load ?! | |
165 | retractall(supernode(_,_)), | |
166 | retractall(stored_formula(_,_)), | |
167 | retractall(expanded(_)), | |
168 | retractall(explanation_parent(_)), | |
169 | retractall(formula_cache(_,_,_)), | |
170 | retractall(example_node(_)), | |
171 | retractall(local_state(_,_,_)). | |
172 | % This predicate should be called after loading a new specification | |
173 | % and before using the other predicates below | |
174 | reset_bvisual :- | |
175 | clear_bvisual, | |
176 | register_top_level. | |
177 | ||
178 | :- public portray_bvisual/0. % debugging utility | |
179 | portray_bvisual :- %listing(top_level_node/1), listing(subnode/2), listing(stored_formula/2) | |
180 | top_level_node(N), bv_portray(N,1),fail. | |
181 | portray_bvisual. | |
182 | bv_portray(ID,Level) :- | |
183 | (stored_formula(ID,Form) -> functor(Form,F,_) ; F = '??'), | |
184 | (expanded(ID) -> E=expanded ; E = 'not_expanded'), | |
185 | indent(Level),format('~w -> ~w [~w]~n',[ID,F,E]), | |
186 | L1 is Level+1, | |
187 | subnode(ID,ID2), | |
188 | bv_portray(ID2,L1). | |
189 | indent(0) :- !. | |
190 | indent(N) :- N>0,!, N1 is N-1, print(' '), indent(N1). | |
191 | ||
192 | % returns the top-level nodes as a list of IDs | |
193 | bv_get_top_level(Tops) :- | |
194 | findall( Id, top_level_node(Id), Tops ). | |
195 | ||
196 | % bv_expand_formula(+FormulaID,-LabelAtom,-) | |
197 | % Input: Id | |
198 | % Output: Label of Formula, list of children | |
199 | bv_expand_formula(Id,Label,Children) :- | |
200 | expanded(Id),!, | |
201 | get_node_label(Id,Label), | |
202 | findall(C, subnode(Id,C), Children). | |
203 | bv_expand_formula(Id,Label,Children) :- | |
204 | get_node_label(Id,Label), | |
205 | explore_node(Id,Children). | |
206 | ||
207 | % bv_get_values in current state | |
208 | bv_get_values(Ids,Values) :- | |
209 | current_state_id(StateId), | |
210 | bv_get_values(Ids,StateId,Values). | |
211 | ||
212 | :- use_module(probsrc(specfile),[prepare_state_for_specfile_trans/3]). | |
213 | :- use_module(probsrc(tools),[start_ms_timer/1,get_elapsed_runtime/2]). | |
214 | ||
215 | % bv_get_values(+IdsOfFormulas,+CurrentStateID,-ValuesOfFormulas) | |
216 | bv_get_values(Ids,StateId,Values) :- | |
217 | visited_expression(StateId,State),!, | |
218 | prepare_state_for_specfile_trans(State,StateId,PreparedState), | |
219 | bv_get_default_formula_timeout(Timeout), | |
220 | start_ms_timer(Timer), | |
221 | bv_get_values2(Ids,PreparedState,StateId,Timeout,Timer,Values). | |
222 | bv_get_values(Ids,_StateId,Values) :- | |
223 | % in case that the state ID cannot be resolved, we | |
224 | % return an error for each formula | |
225 | same_length(Ids,Values), | |
226 | same_value(Values,e('unknown state')). | |
227 | same_value([],_). | |
228 | same_value([V|Rest],V) :- same_value(Rest,V). | |
229 | ||
230 | % get timeout for standard formula evaluation of an entry in the bvisual2 table: | |
231 | bv_get_default_formula_timeout(BVTimeout) :- | |
232 | get_preference(time_out,Timeout), | |
233 | (Timeout =< 1200 -> BVTimeout = Timeout | |
234 | ; BVTimeout is 1200 + (Timeout-1000)// 5). | |
235 | ||
236 | % Insert a new formula | |
237 | % bv_insert_formula(+TypeCheckedExpression,+ParentID,-IDofNewFormula) | |
238 | bv_insert_formula(TExpr,ParentId,Id) :- %print(bv_insert_formula(TExpr,ParentId)),nl, | |
239 | get_new_id(Id), | |
240 | assertz( stored_formula(Id,TExpr) ), | |
241 | assertz( subnode(ParentId,Id) ), | |
242 | assertz( supernode(Id,ParentId) ), | |
243 | (ParentId == top -> assertz(top_level_node(Id)) ; true). | |
244 | ||
245 | bv_time_out_call(Call,ValueFromCall,Timeout,Value) :- | |
246 | catch(bv_time_out_call2(Call,ValueFromCall,Timeout,Value),Exception, | |
247 | (Value=e(ErrStr),translate_prolog_exception(Exception,ErrStr))). | |
248 | bv_time_out_call2(Call,ValueFromCall,Timeout,Value) :- | |
249 | (time_out_with_enum_warning_one_solution( Call, | |
250 | Timeout, | |
251 | Result) | |
252 | -> | |
253 | ( Result == success -> Value = ValueFromCall | |
254 | ; 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 | |
255 | ; 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 ... | |
256 | ; Value = e(timeout)) | |
257 | ). | |
258 | ||
259 | % compute a local timeout based on how long the bv_get_values command has been running thus far: | |
260 | get_local_formula_timeout(DefaultTimeout,TimerSinceStart,FormulaTimeout) :- | |
261 | get_elapsed_runtime(TimerSinceStart,Delta), | |
262 | (Delta > 2*DefaultTimeout % then reduce timeout | |
263 | -> Factor is Delta / DefaultTimeout, | |
264 | debug_format(19,'Reducing timeout by factor of ~w (runtime thus far: ~w, default timeout: ~w)~n',[Factor,Delta,DefaultTimeout]), | |
265 | FormulaTimeout is integer(DefaultTimeout / Factor) | |
266 | ; FormulaTimeout=DefaultTimeout). | |
267 | ||
268 | bv_get_values2([],_,_,_,_,[]). | |
269 | bv_get_values2([Id|Irest],State,StateId,Timeout,TimerSinceStart,[Value|Vrest]) :- | |
270 | get_local_formula_timeout(Timeout,TimerSinceStart,FormulaTimeout), | |
271 | bv_get_value(Id,State,StateId,FormulaTimeout,Value), | |
272 | bv_get_values2(Irest,State,StateId,Timeout,TimerSinceStart,Vrest). | |
273 | ||
274 | bv_get_value(Id,State1,StateId,Timeout,FinalValue) :- | |
275 | bv_get_value_unprocessed(Id,State1,StateId,Timeout,Value), | |
276 | value_post_processing(Value,FinalValue). | |
277 | bv_get_value_unprocessed(Id,State1,StateId,Timeout,Value) :- | |
278 | is_active(Id,StateId,State1,State,LocalState),!, %print(is_active(Id)), debug:nl_time, | |
279 | ( is_cached(Id,StateId,State1,Value1) -> | |
280 | FromCache = true | |
281 | ; bv_get_value1(Id,StateId,State,LocalState,Timeout,Value1) -> | |
282 | FromCache = false %, print(evaluated),debug:nl_time | |
283 | ; | |
284 | Value1 = e('evaluation failed'), | |
285 | FromCache = false), | |
286 | handle_errors(Value1,Value), | |
287 | (FromCache==false, should_be_cached(Id) -> write_to_cache(Id,StateId,State1,Value) ; true). | |
288 | bv_get_value_unprocessed(_Id,_State1,_StateId,_Timeout,i). % INACTIVE | |
289 | ||
290 | bv_get_value1(Id,StateId,State,LocalState,Timeout,Value) :- | |
291 | stored_formula(Id,Formula), | |
292 | bv_get_value2(Formula,Id,StateId,State,LocalState,Timeout,Value). | |
293 | ||
294 | bv_get_value2(Formula,Id,_,State,LocalState,Timeout,Value) :- | |
295 | is_texpr(Formula),!, | |
296 | get_texpr_type(Formula,Type), | |
297 | bv_get_texpr_value3(Type,Id,Formula,LocalState,State,Timeout,Value). | |
298 | bv_get_value2(named_subformula(_,Formula),Id,StateId,State,LocalState,Timeout,Value) :- !, | |
299 | bv_get_value2(Formula,Id,StateId,State,LocalState,Timeout,Value). | |
300 | bv_get_value2(bind(_ID,Value),_,_,_,_,_,btvalue(Value)). | |
301 | bv_get_value2(textnode(Value,_),_,_,_State,_LS,_,v(Value)). | |
302 | bv_get_value2(textnode3(_,Value,_),_,_,_State,_LS,_,ResValue) :- | |
303 | (color_based_on_value(Value,_) -> ResValue = Value % already using encoding | |
304 | ; ResValue = v(Value)). | |
305 | %bv_get_value2(cbc_path(_LastStateID,Path,_Last),_,_,_State,_LS,_,v(NrOfPaths)) :- | |
306 | % append(Path,_,Prefix), | |
307 | % findall(Last,sap:cb_path(_,Prefix,Last),AllPathsWithPrefix), | |
308 | % length(AllPathsWithPrefix,NrOfPaths). | |
309 | bv_get_value2(variant(_Name,_ConvOrAnt,Variant),Id,StateId,State,LocalState,Timeout,Value) :- !, | |
310 | bv_get_value2(Variant,Id,StateId,State,LocalState,Timeout,Value). | |
311 | bv_get_value2(ltl_named_formula(_Name,String),_Id,_StateId,_,_LocalState,_Timeout,Value) :- !, | |
312 | strip_newlines(String,String2), Value=v(String2). | |
313 | bv_get_value2(ltl_formula(_,Tree),_Id,StateId,_,_LocalState,_Timeout,Value) :- !, | |
314 | (is_atomic_ltl_property(Tree) -> | |
315 | (check_atomic_property_formula(Tree,StateId) -> Value = p(true) ; Value=p(false)) | |
316 | ; Value = v('-')). % TO DO: we could evaluate the formulas on back and forward history; ap(enabled(E)) | |
317 | bv_get_value2(guard(_Name,Parameters,Guard),Id,StateId,State,LocalState,Timeout,Value) :- !, | |
318 | get_guard_formula(Parameters,Guard,Expr), | |
319 | bv_get_value2(Expr,Id,StateId,State,LocalState,Timeout,Value). | |
320 | bv_get_value2(guard_theorems(_Name,Parameters,Guard,Theorems),FID,StateId,State,LocalState,Timeout,Value) :- !, | |
321 | get_guard_theorems_formula(Parameters,Guard,Theorems,Expr), | |
322 | bv_get_value2(Expr,FID,StateId,State,LocalState,Timeout,Value). | |
323 | bv_get_value2(raw_state_pp,_,_,State,_LS,_,v(Value)) :- !, % raw pretty printed stated | |
324 | translate_any_state(State,Value). | |
325 | bv_get_value2(Node,_,_,_State,_LS,_,e(unknown)) :- | |
326 | format('Unknown bvisual2 node: ~w~n',[Node]). | |
327 | ||
328 | bv_get_texpr_value3(pred,Id,Formula,LocalState,State,Timeout,Value) :- | |
329 | !, | |
330 | % print('CHECKING PREDICATE: '), translate:print_bexpr(Formula),nl, | |
331 | CS = 'state view table', | |
332 | (bv_time_out_call(b_test_boolean_expression_for_ground_state(Formula,LocalState,State,CS,Id),true,Timeout,ValuePos) -> true ; ValuePos=false), | |
333 | ( get_preference(double_evaluation_when_analysing,true) -> | |
334 | CS2 = 'state view table (negated)', | |
335 | (bv_time_out_call(b_not_test_boolean_expression_cs(Formula,LocalState,State,CS2,Id),true,Timeout,ValueNeg) | |
336 | -> true ; ValueNeg=false), | |
337 | combine_predicate_values(ValuePos,ValueNeg,Value) | |
338 | ; encode_predicate_value(ValuePos,Value)). | |
339 | bv_get_texpr_value3(_,Id,Formula,LocalState,State,Timeout,Res) :- | |
340 | CS = 'state view table', | |
341 | (bv_time_out_call(b_compute_expression_nowf(Formula,LocalState,State,FValue,CS,Id),FValue,Timeout,Value) | |
342 | -> ( Value = e(E) -> Res = e(E) % e for exception or timeout | |
343 | ; Res = btvalue(Value,Formula) | |
344 | ) | |
345 | ; texpr_contains_wd_condition(Formula) -> Res = e(undefined) | |
346 | ). | |
347 | ||
348 | ||
349 | encode_predicate_value(e(Error),e(Error)). | |
350 | encode_predicate_value(bv_info(Error),bv_info(Error)). | |
351 | encode_predicate_value(true,p(true)). | |
352 | encode_predicate_value(false,p(false)). | |
353 | combine_predicate_values(e(_Error),true,p(false)) :- | |
354 | print('### Ignoring Timeout in Positive Case of DOUBLE_EVALUATION as Negated Predicate is TRUE'),nl. | |
355 | combine_predicate_values(e(_Error),false,p(true)) :- | |
356 | print('### Ignoring Timeout in Positive Case of DOUBLE_EVALUATION as Negated Predicate is FALSE'),nl. | |
357 | combine_predicate_values(e(Error),e(_),e(Error)). | |
358 | combine_predicate_values(true,false,p(true)). | |
359 | combine_predicate_values(false,true,p(false)). | |
360 | combine_predicate_values(true,true,e('both true and false')). | |
361 | combine_predicate_values(false,false,e(undefined)). | |
362 | combine_predicate_values(true,e(_Error),p(true)) :- | |
363 | print('### Ignoring Timeout in Negative Case of DOUBLE_EVALUATION'),nl. | |
364 | combine_predicate_values(false,e(_Error),p(false)) :- | |
365 | print('### Ignoring Timeout in Negative Case of DOUBLE_EVALUATION'),nl. | |
366 | ||
367 | :- dynamic get_unlimited_value/0. | |
368 | ||
369 | ||
370 | value_post_processing(In,Out) :- | |
371 | with_bvisual2_translation_mode( | |
372 | (value_post_processing2(In,O) -> O=Out ; Out=e('internal error: failed to post-process value'))). | |
373 | value_post_processing2(v(Value),v(Value)). | |
374 | value_post_processing2(p(Value),p(Value)). | |
375 | value_post_processing2(e(Error),e(Error)). | |
376 | value_post_processing2(i,i). | |
377 | value_post_processing2(bv_info(I),bv_info(I)). | |
378 | value_post_processing2(btvalue(BValue,Expr),v(Value)) :- | |
379 | (get_unlimited_value -> translate_bvalue_for_expression(BValue,Expr,Value) | |
380 | ; translate_bvalue_for_expression_with_limit(BValue,Expr,600,Value) % one can always use bv_get_value_unlimited | |
381 | ). | |
382 | value_post_processing2(btvalue(BValue),v(Value)) :- | |
383 | % TO DO: get type for variables and constants | |
384 | (get_unlimited_value -> translate_bvalue(BValue,Value) | |
385 | ; translate_bvalue_with_type_and_limit(BValue,any,600,Value)). | |
386 | ||
387 | ||
388 | ||
389 | ||
390 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
391 | % caching of some values | |
392 | :- use_module(probsrc(store),[no_value_for_variable/2]). | |
393 | ||
394 | % we do not compute the theorems node, only its subnodes | |
395 | is_cached(theoremsc,_,_,v('')) :- !. | |
396 | is_cached(theoremscm,_,_,v('')) :- !. | |
397 | is_cached(theoremsv,_,_,v('')) :- !. | |
398 | is_cached(theoremsvm,_,_,v('')) :- !. | |
399 | is_cached(goal,_,_,v('')) :- !. | |
400 | % we use the invariant_violated flag of the state space as a kind of cache | |
401 | is_cached(inv,StateId,_State,Value) :- | |
402 | \+ invariant_not_yet_checked(StateId), | |
403 | (invariant_violated(StateId) -> Value=p(false) ; Value=p(true)). | |
404 | % axioms are usually true in the constants' state | |
405 | is_cached(axioms,StateId,concrete_constants(State),R) :- !, | |
406 | is_cached_constants_state(StateId,State,R). | |
407 | is_cached(axioms,StateId,[_|_],R) :- !, % states consisting of just a list are either constructed by | |
408 | % find valid state, state-based MC,... or when there are no constants | |
409 | % We assume PROPERTIES/axioms to be true; by constructing these commands have to satisfy the properties | |
410 | is_cached_constants_state(StateId,[],R). | |
411 | % this formula was already computed and cached for the given state | |
412 | is_cached(FormulaId,StateId,_State,Value) :- | |
413 | formula_cache(FormulaId,StateId,Value),!. | |
414 | % in case of axiom, we can look at the reverences constants' state | |
415 | is_cached(FormulaId,_,expanded_const_and_vars(ConstId,_,_,_),Value) :- is_cached_axiom(FormulaId,ConstId,Value). | |
416 | is_cached(FormulaId,_,const_and_vars(ConstId,_),Value) :- is_cached_axiom(FormulaId,ConstId,Value). | |
417 | is_cached_axiom(FormulaId,ConstId,Value) :- | |
418 | is_axiom_or_static_theorem(FormulaId), | |
419 | visited_expression(ConstId,ConstState), | |
420 | % we could avoid unpacking, but constants state are not packed anyway; full value is only used for partial_setup_constants below; TO DO avoid extracting ConstState | |
421 | is_cached(FormulaId,ConstId,ConstState,Value),!. | |
422 | ||
423 | is_cached_constants_state(StateId,State,R) :- | |
424 | % only if a partial_setup_constants event led to that | |
425 | % state, then something did not work | |
426 | ( transition(root,'$partial_setup_constants',StateId) -> | |
427 | (member(bind(_,Val),State), no_value_for_variable(Val,_) | |
428 | -> R = e('some constants have no values') | |
429 | ; properties_were_filtered(Nr), Nr>0 | |
430 | -> get_node_label(axioms,Axioms), | |
431 | ajoin(['some ',Axioms, ' (',Nr,') were ignored'],Msg), R = e(Msg) | |
432 | ; animation_minor_mode(eventb) -> R = e('some axioms may be false') | |
433 | ; R = e('some properties may be false') | |
434 | ) | |
435 | ; R = p(true)). | |
436 | ||
437 | should_be_cached(FormulaId) :- | |
438 | is_axiom_or_static_theorem(FormulaId). | |
439 | ||
440 | write_to_cache(FormulaId,_StateId,const_and_vars(ConstId,_),Value) :- | |
441 | is_axiom_or_static_theorem(FormulaId),!, | |
442 | visited_expression(ConstId,ConstState), | |
443 | write_to_cache(FormulaId,ConstId,ConstState,Value). | |
444 | write_to_cache(FormulaId,StateId,_State,Value) :- | |
445 | assertz(formula_cache(FormulaId,StateId,Value)). | |
446 | ||
447 | is_axiom_or_static_theorem(axioms) :- !. | |
448 | is_axiom_or_static_theorem(theoremsc) :- !. | |
449 | is_axiom_or_static_theorem(theoremscm) :- !. | |
450 | is_axiom_or_static_theorem(FormulaId) :- | |
451 | supernode(FormulaId,Parent),is_axiom_or_static_theorem(Parent). | |
452 | ||
453 | :- use_module(probsrc(tools_strings),[atom_codes_with_limit/3]). | |
454 | handle_errors(_,e(ErrorMsg)) :- | |
455 | get_all_errors_and_clear([Error|_]),!, % TO DO: use proper error scoping and do not trigger when error stored before calling bvisual2 | |
456 | write_to_codes(Error,ErrorCodes), | |
457 | atom_codes_with_limit(ErrorMsg,200,ErrorCodes). | |
458 | handle_errors(Value,Value). | |
459 | ||
460 | ||
461 | % is_active(+FormulaID,+InState,-PossiblyExpandedState) | |
462 | % says if a FormulaID makes sense for the current state, if not: it will be grayed out | |
463 | is_active(user,StateId,InState,OutState,LocalState) :- !, | |
464 | is_active(inv,StateId,InState,OutState,LocalState). | |
465 | is_active(inv,_StateId,InState,OutState,LocalState) :- !, | |
466 | empty_state(LocalState), | |
467 | state_corresponds_to_initialised_b_machine(InState,OutState). | |
468 | is_active(axioms,_StateId,InState,OutState,LocalState) :- !, | |
469 | InState \= root, | |
470 | empty_state(LocalState), | |
471 | state_corresponds_to_set_up_constants(InState,OutState), | |
472 | !. | |
473 | is_active(variants,StateId,InState,OutState,LocalState) :- !, | |
474 | is_active(inv,StateId,InState,OutState,LocalState). | |
475 | is_active(theoremsc,StateId,InState,OutState,LocalState) :- !, | |
476 | is_active(axioms,StateId,InState,OutState,LocalState). | |
477 | is_active(theoremscm,StateId,InState,OutState,LocalState) :- !, | |
478 | is_active(axioms,StateId,InState,OutState,LocalState). | |
479 | is_active(theoremsv,StateId,InState,OutState,LocalState) :- !, | |
480 | is_active(inv,StateId,InState,OutState,LocalState). | |
481 | is_active(theoremsvm,StateId,InState,OutState,LocalState) :- !, | |
482 | is_active(inv,StateId,InState,OutState,LocalState). | |
483 | is_active(guards_top_level,StateId,InState,OutState,LocalState) :- !, | |
484 | is_active(inv,StateId,InState,OutState,LocalState). | |
485 | is_active(guards_subsidiary,StateId,InState,OutState,LocalState) :- !, | |
486 | is_active(inv,StateId,InState,OutState,LocalState). | |
487 | is_active(guard_theorems,StateId,InState,OutState,LocalState) :- !, | |
488 | is_active(inv,StateId,InState,OutState,LocalState). | |
489 | is_active(variables,StateId,InState,OutState,LocalState) :- !, | |
490 | is_active(inv,StateId,InState,OutState,LocalState). | |
491 | is_active(constants,StateId,InState,OutState,LocalState) :- !, | |
492 | is_active(axioms,StateId,InState,OutState,LocalState). | |
493 | is_active(sets,_StateId,InState,OutState,LocalState) :- !, b_or_z_successsful_mode, | |
494 | empty_state(LocalState), InState=OutState. | |
495 | is_active(freetypes,_StateId,InState,OutState,LocalState) :- !, | |
496 | empty_state(LocalState), InState=OutState. | |
497 | is_active(goal,StateId,InState,OutState,LocalState) :- !, | |
498 | is_active(inv,StateId,InState,OutState,LocalState). | |
499 | is_active(user_formulas,StateId,InState,OutState,LocalState) :- !, | |
500 | is_active(inv,StateId,InState,OutState,LocalState). | |
501 | is_active(definitions,StateId,InState,OutState,LocalState) :- !, | |
502 | is_active(inv,StateId,InState,OutState,LocalState). | |
503 | is_active(ltl_formulas,StateId,InState,OutState,LocalState) :- !, | |
504 | is_active(inv,StateId,InState,OutState,LocalState). | |
505 | is_active(channels,_StateId,S,OutState,LocalState) :- !, | |
506 | csp_mode, OutState=S,empty_state(LocalState). | |
507 | is_active(datatypes,_StateId,S,OutState,LocalState) :- !, | |
508 | csp_mode, OutState=S,empty_state(LocalState). | |
509 | is_active(subtypes,_StateId,S,OutState,LocalState) :- !, | |
510 | csp_mode, OutState=S,empty_state(LocalState). | |
511 | is_active(raw_state,_StateId,S,OutState,LocalState) :- !, | |
512 | \+ b_or_z_mode, % maybe we should extract it for csp_and_b ? | |
513 | OutState=S,empty_state(LocalState). | |
514 | %is_active(cbc_tests,_StateId,_InState,_OutState,_LocalState) :- !, | |
515 | % sap:cb_path(_,[_],_). % show cbc_tests if we ran CBC test-case generator | |
516 | is_active(NodeId,StateId,InState,OutState,LocalState) :- | |
517 | supernode(NodeId,Super), | |
518 | is_active(Super,StateId,InState,OutState,InLocalState), | |
519 | % check if the parent node introduces example values (e.g. in a exists-clause) | |
520 | % If yes, the local state is extended by the values | |
521 | ( example_node(Super) -> | |
522 | find_example(Super,StateId,OutState,InLocalState,LocalState) | |
523 | ; | |
524 | InLocalState = LocalState). | |
525 | ||
526 | find_example(NodeId,StateId,_State,_InLocalState,LocalState) :- | |
527 | % check if the value was computed and cached before | |
528 | local_state(NodeId,StateId,Result),!, | |
529 | % if Result is not of the form example/1, no example | |
530 | % was found. Just fail to show inactive state | |
531 | Result = example(LocalState). | |
532 | find_example(NodeId,StateId,State,InLocalState,LocalState) :- | |
533 | % how the example is computed depends on the expression (e.g. exists) | |
534 | % and the outcome of the parent node (true or false) | |
535 | bv_get_values([NodeId],StateId,[V]),!, | |
536 | stored_formula(NodeId,Formula), | |
537 | ( find_example1(Formula,V,State,InLocalState,LocalState) -> | |
538 | Result = example(LocalState) | |
539 | ; | |
540 | Result = not_found), | |
541 | % currently we just ignore errors | |
542 | handle_errors(_,_), | |
543 | assertz( local_state(NodeId,StateId,Result) ), | |
544 | Result = example(_). | |
545 | find_example1(TExpr,V,State,InLocalState,LocalState) :- | |
546 | is_texpr(TExpr),!, | |
547 | get_texpr_expr(TExpr,Expr), | |
548 | find_example2(Expr,V,State,InLocalState,LocalState). | |
549 | find_example1(guard(_Name,Parameters,Guard),V,State,InLocalState,LocalState) :- | |
550 | create_or_merge_exists(Parameters,Guard,Exists), | |
551 | find_example1(Exists,V,State,InLocalState,LocalState). | |
552 | find_example1(guard_theorems(_Name,Parameters,Guard,Theorems),V,State,InLocalState,LocalState) :- | |
553 | create_forall(Parameters,b(implication(Guard,Theorems),pred,[]),ForAll), | |
554 | find_example1(ForAll,V,State,InLocalState,LocalState). | |
555 | find_example2(let_predicate(Ids,AssignmentExprs,Pred),Status,State,InLocalState,LocalState) :- | |
556 | % translate LET back to exists | |
557 | create_exists_for_let(Ids,AssignmentExprs,Pred,_,ExistsPred), | |
558 | find_example2(exists(Ids,ExistsPred),Status,State,InLocalState,LocalState). | |
559 | find_example2(let_expression(Ids,AssignmentExprs,_Expr),_Status,State,InLocalState,LocalState) :- | |
560 | % translate LET expression to exists to find solution for assignments | |
561 | % _Status is typically v(Value) | |
562 | create_exists_for_let(Ids,AssignmentExprs,b(truth,pred,[]),_,ExistsPred), | |
563 | find_example2(exists(Ids,ExistsPred),p(true),State,InLocalState,LocalState). | |
564 | find_example2(exists(Ids,Predicate),p(true),State,InLocalState,LocalState) :- | |
565 | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState). | |
566 | find_example2(exists(Ids,Predicate),p(false),State,InLocalState,LocalState) :- | |
567 | Predicate = b(conjunct(_,_),pred,_), % we have a false conjunct: try and find maximal prefix that is satisfiable | |
568 | conjunction_to_list(Predicate,PredList), | |
569 | maxsat_conjunct(Ids,PredList,[],State,InLocalState,no_solution,LocalState), | |
570 | LocalState \= no_solution, | |
571 | !. | |
572 | find_example2(exists(Ids,Predicate),p(false),State,InLocalState,LocalState) :- | |
573 | safe_create_texpr(negation(Predicate),pred,Negation), | |
574 | find_solution_for_predicate(Ids,Negation,State,InLocalState,LocalState). | |
575 | find_example2(forall(Ids,Pre,Condition),p(false),State,InLocalState,LocalState) :- | |
576 | safe_create_texpr(negation(Condition),pred,Negation), | |
577 | conjunct_predicates([Pre,Negation],Predicate), | |
578 | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState). | |
579 | find_example2(forall(Ids,Pre,Condition),p(true),State,InLocalState,LocalState) :- | |
580 | conjunct_predicates([Pre,Condition],Predicate), | |
581 | find_solution_for_predicate(Ids,Predicate,State,InLocalState,LocalState), | |
582 | !. | |
583 | find_example2(forall(Ids,Pre,_),p(true),State,InLocalState,LocalState) :- | |
584 | % the LHS of the forall is never true; try find maximal subsequence for it: | |
585 | find_example2(exists(Ids,Pre),p(false),State,InLocalState,LocalState). | |
586 | find_example2(comprehension_set(Ids,Predicate),v(VS),State,InLocalState,LocalState) :- | |
587 | (empty_val_str(VS) -> PVal=false ; PVal=true), | |
588 | find_example2(exists(Ids,Predicate),p(PVal),State,InLocalState,LocalState). | |
589 | empty_val_str(VS) :- (VS = '{}' -> true ; atom(VS),atom_codes(VS,[8709])). % unicode empty set | |
590 | ||
591 | find_solution_for_predicate(Ids,Predicate,State,InLocalState,NormedLocalState) :- | |
592 | get_preference(time_out,Timeout), | |
593 | set_up_typed_localstate(Ids,_FreshVars,TypedVals,InLocalState,LocalState,positive), | |
594 | (time_out_with_enum_warning_one_solution( | |
595 | (init_wait_flags_with_call_stack(WF,[prob_command_context(find_solution_for_predicate,unknown)]), | |
596 | b_tighter_enumerate_values_in_ctxt(TypedVals,Predicate,WF), | |
597 | b_test_boolean_expression(Predicate,LocalState,State,WF), | |
598 | ground_wait_flags(WF)), | |
599 | Timeout,Result) | |
600 | -> Result == success, | |
601 | normalise_store(LocalState,NormedLocalState) | |
602 | ). | |
603 | ||
604 | create_exists_for_let(Ids,AssignmentExprs,Pred,Equalities,ExistsPred) :- | |
605 | maplist(create_equality,Ids,AssignmentExprs,Equalities), | |
606 | append(Equalities,[Pred],L), | |
607 | conjunct_predicates(L,ExistsPred). | |
608 | ||
609 | create_equality(ID,Expr,Equality) :- | |
610 | safe_create_texpr(equal(ID,Expr),pred,Equality). | |
611 | ||
612 | % find maximal subsequence of conjuncts that are satisfiable and return LocalState solution found | |
613 | maxsat_conjunct(Ids,[LHS|Rest],ConSoFar,State,InLocalState,_BestLocalStateSoFar,ResLocalState) :- | |
614 | append(ConSoFar,[LHS],NewConjunctList), | |
615 | %print('TRY: '), translate:print_bexpr(LHS),nl, | |
616 | conjunct_predicates(NewConjunctList,NewConjunct), | |
617 | find_solution_for_predicate(Ids,NewConjunct,State,InLocalState,LocalState), | |
618 | !, % print('+'), | |
619 | maxsat_conjunct(Ids,Rest,NewConjunctList,State,InLocalState, LocalState,ResLocalState). | |
620 | maxsat_conjunct(Ids,[_|Rest],ConSoFar,State,InLocalState,BestLocalStateSoFar,Res) :- !, % allows skipping conjuncts | |
621 | maxsat_conjunct(Ids,Rest,ConSoFar,State,InLocalState,BestLocalStateSoFar,Res). | |
622 | maxsat_conjunct(_Ids,_Rest,_ConSoFar,_State,_InLocalState,BestLocalStateSoFar,Res) :- | |
623 | Res = BestLocalStateSoFar. | |
624 | ||
625 | explore_node(Id,Children) :- | |
626 | stored_formula(Id,Formula), | |
627 | check_if_example_node(Id,Formula), | |
628 | get_subformulas(Formula,Subs,Kind), | |
629 | assertz( expanded(Id) ), | |
630 | (Kind = explanation(Operator) | |
631 | -> assert_as_explanation(Id,ExplId,Operator), Children = [ExplId|Children1], | |
632 | register_formulas(Subs,Id,Children1) | |
633 | ; register_formulas(Subs,Id,Children)). | |
634 | ||
635 | assert_as_explanation(Parent,Id,Operator) :- | |
636 | assertz(explanation_parent(Parent)), | |
637 | % add a text line; showing that we did an equivalence rewrite | |
638 | get_new_id(Id), | |
639 | assertz( stored_formula(Id,textnode3('\x21D4\',bv_info(Operator),[])) ), % unicode translation | |
640 | assertz( subnode(Parent,Id) ), | |
641 | assertz( supernode(Id,Parent) ). | |
642 | ||
643 | bv_is_explanation_node(NodeId) :- | |
644 | supernode(NodeId,ParentId), | |
645 | explanation_parent(ParentId). | |
646 | ||
647 | % the following predicates determine whether the node introduces | |
648 | % example values and stores that information in example_node/1. | |
649 | check_if_example_node(Id,Formula) :- | |
650 | is_example_node(Formula),!, | |
651 | assertz( example_node(Id) ). | |
652 | check_if_example_node(_Id,_Formula). | |
653 | is_example_node(TFormula) :- | |
654 | is_texpr(TFormula),!, | |
655 | get_texpr_expr(TFormula,Formula), | |
656 | is_example_node2(Formula). | |
657 | is_example_node(guard(_Name,[_|_],_Guard)). | |
658 | is_example_node(guard_theorems(_Name,[_|_],_Guard,_Theorems)). | |
659 | is_example_node2(exists(_Ids,_Cond)). | |
660 | is_example_node2(forall(_Ids,_Pre,_Cond)). | |
661 | is_example_node2(let_predicate(_Ids,_E,_Cond)). | |
662 | is_example_node2(let_expression(_Ids,_E,_Cond)). | |
663 | is_example_node2(comprehension_set(_Ids,_Cond)). | |
664 | ||
665 | % subformula_rule/4 defines wich subformulas should be | |
666 | % shown in an evaluation tree for a formula. If no | |
667 | % rule matches, the standard subformulas are used | |
668 | subformula_rule(forall(Ids,P,R),_,Subs,quantifier) :- | |
669 | append(Ids,[P,R],Subs). | |
670 | subformula_rule(let_predicate(Ids,AssignmentExprs,Pred),_,Subs,quantifier) :- | |
671 | % see create_exists_for_let(Ids,AssignmentExprs,Pred,Equalities,_ExistsPred), | |
672 | maplist(create_equality,Ids,AssignmentExprs,Equalities), | |
673 | append(Equalities,[Pred],EP), % show equalities and then one subnode for the predicate | |
674 | append(Ids,EP,Subs). | |
675 | subformula_rule(exists(Ids,P),_,Subs,quantifier) :- | |
676 | conjunction_to_list(P,PL), | |
677 | append(Ids,PL,Subs). | |
678 | subformula_rule(comprehension_set(Ids,P),_,Subs,quantifier) :- | |
679 | conjunction_to_list(P,PL), | |
680 | append(Ids,PL,Subs). | |
681 | subformula_rule(conjunct(A,B),_,Subs,normal) :- | |
682 | safe_create_texpr(conjunct(A,B),pred,E), | |
683 | conjunction_to_list(E,Subs). | |
684 | subformula_rule(disjunct(A,B),_,Subs,normal) :- | |
685 | disjunction_to_list(A,B,Subs). | |
686 | subformula_rule(let_expression(Ids,AssignmentExprs,Expr),_,Subs,quantifier) :- | |
687 | maplist(create_equality,Ids,AssignmentExprs,Equalities), | |
688 | append(Equalities,[Expr],EP), % show equalities and then one subnode for the expression | |
689 | append(Ids,EP,Subs). | |
690 | subformula_rule(Formula,TFormula,Subs,Kind) :- | |
691 | get_preference(show_bvisual_formula_explanations,true), | |
692 | subformula_explanation_rule(Formula,TFormula,Subs,Kind). | |
693 | ||
694 | subformula_explanation_rule(equal(A,B),TF,[Sub1,Sub2],explanation(equal)) :- | |
695 | get_texpr_type(A,T),T=set(SType), | |
696 | \+ (kernel_objects:max_cardinality(SType,Max),number(Max),Max<10), % sets can never be very large | |
697 | is_not_bvexpr(TF), % do not apply to explanation expressions | |
698 | no_empty_set(A),no_empty_set(B), | |
699 | !, | |
700 | create_bvexpr(set_subtraction(A,B),T,AminusB), | |
701 | create_bvexpr(set_subtraction(B,A),T,BminusA), | |
702 | create_bvexpr(empty_set,T,Empty), | |
703 | create_bvexpr(equal(AminusB,Empty),pred,Sub1), | |
704 | create_bvexpr(equal(BminusA,Empty),pred,Sub2). | |
705 | subformula_explanation_rule(subset(A,B),_,[Equals],explanation(subset)) :- | |
706 | subset_rule(A,B,Equals). | |
707 | subformula_explanation_rule(subset_strict(A,B),_,[AmBEmpty,NotEquals],explanation(subset_strict)) :- | |
708 | subset_rule(A,B,AmBEmpty), | |
709 | get_texpr_type(A,T), | |
710 | create_bvexpr(set_subtraction(B,A),T,BminusA), | |
711 | create_bvexpr(empty_set,T,Empty), | |
712 | create_bvexpr(not_equal(BminusA,Empty),pred,NotEquals). | |
713 | subformula_explanation_rule(not_subset(A,B),_,Subs,Kind) :- | |
714 | subformula_explanation_rule(subset(A,B),_,Subs,Kind). % it is an equivalent rewrite to the negation | |
715 | subformula_explanation_rule(not_subset_strict(A,B),_,Subs,Kind) :- | |
716 | subformula_explanation_rule(subset_strict(A,B),_,Subs,Kind). % it is an equivalent rewrite to the negation | |
717 | subformula_explanation_rule(member(TM,TS),_,Children,explanation(Func)) :- | |
718 | get_texpr_expr(TS,S), | |
719 | subformula_member_rule(S,TM,TS,Children),!, | |
720 | functor(S,Func,_). | |
721 | ||
722 | subset_rule(A,B,Equals) :- % A<:B <=> A\B = {} | |
723 | get_texpr_type(A,T), | |
724 | create_bvexpr(set_subtraction(A,B),T,AminusB), | |
725 | create_bvexpr(empty_set,T,Empty), | |
726 | create_bvexpr(equal(AminusB,Empty),pred,Equals1), | |
727 | add_texpr_description(Equals1,'Subset check: find elements in left not in right set',Equals). | |
728 | ||
729 | :- use_module(probsrc(bsyntaxtree),[is_just_type/1,add_texpr_description/3]). | |
730 | ||
731 | subformula_member_rule(partial_function(TDom,TRan),TM,TS,[TDoubles]) :- | |
732 | is_just_type(TDom), | |
733 | is_just_type(TRan), | |
734 | !, | |
735 | % this rule describes the plain function check, without | |
736 | % checking domains | |
737 | texpr_function_type(TS,FunctionType,DomType,RanType), | |
738 | create_texpr(identifier(d),DomType,[],TDomId), | |
739 | create_texpr(identifier(r1),RanType,[],TRanId1), | |
740 | create_texpr(identifier(r2),RanType,[],TRanId2), | |
741 | create_texpr(comprehension_set([TDomId,TRanId1],TExists),FunctionType,[],TDoubles0), | |
742 | % create_exists([TRanId2],TPred,TExists1), % moved below so that used ids can be computed | |
743 | create_texpr(couple(TDomId,TRanId1),couple(DomType,RanType),[],TCouple1), | |
744 | create_texpr(couple(TDomId,TRanId2),couple(DomType,RanType),[],TCouple2), | |
745 | safe_create_texpr(not_equal(TRanId1,TRanId2),pred,Unequal), | |
746 | create_texpr(member(TCouple1,TM),pred,[],TMember1), | |
747 | create_texpr(member(TCouple2,TM),pred,[],TMember2), | |
748 | conjunct_predicates([Unequal,TMember1,TMember2],TPred), | |
749 | create_exists([TRanId2],TPred,TExists1), % now also computes used identifiers; cleanup no longer required ? | |
750 | % This is necessary to register the used identifiers | |
751 | clean_up_pred(TExists1,[],TExists), | |
752 | add_texpr_description(TDoubles0,'Partial function check: find counter-example pairs for functionality',TDoubles). | |
753 | subformula_member_rule(partial_function(TA,TB),TM,TS,[TFunCheck|SetChecks]) :- | |
754 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
755 | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). | |
756 | subformula_member_rule(total_function(TA,TB),TM,TS,[TFunCheck|SetChecks]) :- | |
757 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
758 | create_total_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). | |
759 | subformula_member_rule(partial_injection(TA,TB),TM,TS,[TFunCheck,TInjCheck|SetChecks]) :- | |
760 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
761 | create_injection_check(TM,TS,TInjCheck), | |
762 | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). | |
763 | subformula_member_rule(total_injection(TA,TB),TM,TS,[TFunCheck,TInjCheck|SetChecks]) :- | |
764 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
765 | create_injection_check(TM,TS,TInjCheck), | |
766 | create_total_domain_range_checks(TDomain,TRange,TA,TB,SetChecks). | |
767 | subformula_member_rule(partial_surjection(TA,TB),TM,TS,Children) :- | |
768 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
769 | create_texpr(equal(TRange,TB),pred,[],TRanCheck), | |
770 | create_optional_subset_check(TDomain,TA,DomChecks), | |
771 | append([TFunCheck|DomChecks],[TRanCheck],Children). | |
772 | subformula_member_rule(total_surjection(TA,TB),TM,TS,[TFunCheck,TDomCheck,TRanCheck]) :- | |
773 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
774 | create_texpr(equal(TDomain,TA),pred,[],TDomCheck), | |
775 | create_texpr(equal(TRange,TB),pred,[],TRanCheck). | |
776 | subformula_member_rule(total_bijection(TA,TB),TM,TS,[TFunCheck,TInjCheck,TDomCheck,TRanCheck]) :- | |
777 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
778 | create_injection_check(TM,TS,TInjCheck), | |
779 | create_texpr(equal(TDomain,TA),pred,[],TDomCheck), | |
780 | create_texpr(equal(TRange,TB),pred,[],TRanCheck). | |
781 | subformula_member_rule(partial_bijection(TA,TB),TM,TS,Children) :- | |
782 | create_function_check(TM,TS,TFunCheck,TDomain,TRange), | |
783 | create_injection_check(TM,TS,TInjCheck), | |
784 | create_optional_subset_check(TDomain,TA,DomChecks), | |
785 | create_texpr(equal(TRange,TB),pred,[],TRanCheck), | |
786 | append([TFunCheck,TInjCheck|DomChecks],[TRanCheck],Children). | |
787 | subformula_member_rule(pow_subset(TA),TM,_TS,[NewCheck]) :- | |
788 | % TM : POW(TA) <=> TM \ TA = {} | |
789 | get_texpr_type(TM,Type), | |
790 | create_bvexpr(set_subtraction(TM,TA),Type,Diff), | |
791 | create_bvexpr(empty_set,Type,Empty), | |
792 | create_bvexpr(equal(Diff,Empty),pred,NewCheck). | |
793 | % TO DO: add rules for <:, <<:, FIN, POW1, FIN1 | |
794 | ||
795 | :- use_module(probsrc(typing_tools),[create_maximal_type_set/2]). | |
796 | ||
797 | create_function_check(TM,TS,TFunCheck,TDomain,TRange) :- | |
798 | texpr_function_type(TS,FunctionType,DomType,RanType), | |
799 | create_maximal_type_set(DomType,TDom), % we could use typeset/0, but requires going through ast_cleanup | |
800 | create_maximal_type_set(RanType,TRan), % ditto | |
801 | create_bvexpr(partial_function(TDom,TRan),set(FunctionType),TFun), | |
802 | create_bvexpr(member(TM,TFun),pred,TFunCheck0), | |
803 | create_bvexpr(domain(TM),set(DomType),TDomain), | |
804 | create_bvexpr(range(TM),set(RanType),TRange), | |
805 | add_texpr_description(TFunCheck0,'Check partial function',TFunCheck). | |
806 | ||
807 | create_domain_range_checks(TDomain,TRange,TA,TB,SetChecks) :- | |
808 | create_optional_subset_check(TDomain,TA,DomCheck), | |
809 | create_optional_subset_check(TRange,TB,RanCheck), | |
810 | append(DomCheck,RanCheck,SetChecks). | |
811 | create_total_domain_range_checks(TDomain,TRange,TA,TB,[TIsTotal|RanCheck]) :- | |
812 | create_texpr(equal(TDomain,TA),pred,[description('Check domain of total function')],TIsTotal), | |
813 | create_optional_subset_check(TRange,TB,RanCheck). | |
814 | create_optional_subset_check(TSubset,TSuperset,Check) :- | |
815 | ( is_just_type(TSuperset) -> | |
816 | Check = [] | |
817 | ; | |
818 | create_texpr(subset(TSubset,TSuperset),pred,[description('Check domain/range of function')],TPred), | |
819 | Check = [TPred]). | |
820 | ||
821 | create_injection_check(TM,TS,TCheckExpr) :- | |
822 | texpr_function_type(TS,FunctionType,DomType,RanType), | |
823 | create_texpr(identifier(d1),DomType,[],TDomId1), | |
824 | create_texpr(identifier(d2),DomType,[],TDomId2), | |
825 | create_texpr(identifier(r1),RanType,[],TRanId), | |
826 | create_texpr(comprehension_set([TDomId1,TRanId],TExists),FunctionType,[bv_function_check(TM)],TCheckExpr), | |
827 | %create_exists([TDomId2],TPred,TExists1), | |
828 | create_texpr(couple(TDomId1,TRanId),couple(DomType,RanType),[],TCouple1), | |
829 | create_texpr(couple(TDomId2,TRanId),couple(DomType,RanType),[],TCouple2), | |
830 | create_texpr(not_equal(TDomId1,TDomId2),pred,[],Unequal), | |
831 | create_texpr(member(TCouple1,TM),pred,[],TMember1), | |
832 | create_texpr(member(TCouple2,TM),pred,[],TMember2), | |
833 | conjunct_predicates([Unequal,TMember1,TMember2],TPred), | |
834 | create_exists([TDomId2],TPred,TExists1), % now also computes used identifiers; cleanup no longer required ? | |
835 | % This is necessary to register the used identifiers | |
836 | clean_up_pred(TExists1,[],TExists2), | |
837 | add_texpr_description(TExists2,'Find counter-example pairs for injectivity',TExists). | |
838 | ||
839 | texpr_function_type(TFun,FunType,DomType,RanType) :- | |
840 | get_texpr_type(TFun,set(FunType)), | |
841 | FunType = set(couple(DomType,RanType)). | |
842 | ||
843 | ||
844 | create_bvexpr(Expr,Type,TExpr) :- | |
845 | create_texpr(Expr,Type,[bvisual],TExpr). | |
846 | is_not_bvexpr(TExpr) :- | |
847 | get_texpr_info(TExpr,Infos),nonmember(bvisual,Infos). | |
848 | %is_bvexpr(TExpr) :- get_texpr_info(TExpr,Infos),memberchk(bvisual,Infos). | |
849 | ||
850 | no_empty_set(E) :- \+ is_empty_set(E). | |
851 | ||
852 | is_empty_set(b(E,_,_)) :- is_empty_set_aux(E). | |
853 | is_empty_set_aux(empty_set). | |
854 | is_empty_set_aux(empty_sequence). | |
855 | is_empty_set_aux(value(X)) :- X==[]. | |
856 | ||
857 | get_subformulas(TFormula,Subs,Kind) :- | |
858 | is_texpr(TFormula), | |
859 | get_texpr_expr(TFormula,Formula), | |
860 | subformula_rule(Formula,TFormula,Subs,Kind),!. | |
861 | get_subformulas(TFormula,Subs,syntaxtraversion) :- | |
862 | is_texpr(TFormula),!, | |
863 | bv_syntaxtraversion(TFormula,Subs). | |
864 | get_subformulas(named_subformula(_,TFormula),Subs,Kind) :- !, | |
865 | (get_subformulas(TFormula,TSubs,Kind),TSubs \= [] | |
866 | -> Subs = [TFormula] | |
867 | ; Kind=syntaxtraversion, Subs=[]). | |
868 | get_subformulas(textnode(_,Subs),Subs,textnode) :- !. | |
869 | get_subformulas(textnode3(_,_,Subs),Subs,textnode) :- !. | |
870 | get_subformulas(guard(_Name,Parameters,Guard),Subs,guard) :- !, | |
871 | conjunction_to_list(Guard,GuardSubs), | |
872 | append(Parameters,GuardSubs,Subs). | |
873 | get_subformulas(variant(_Name,_ConvOrAnt,Variant),Subs,variant) :- !, | |
874 | Subs = [Variant]. | |
875 | get_subformulas(ltl_named_formula(_,String),Subs,ltl_formula) :- !, | |
876 | temporal_parser(String,ltl,Formula), | |
877 | Subs = [ltl_formula(String,Formula)]. | |
878 | get_subformulas(ltl_formula(_,Formula),Subs,ltl_formula) :- !, | |
879 | get_bv_ltl_sub_formulas(Formula,Subs). | |
880 | get_subformulas(guard_theorems(_Name,[],_Guard,Theorems),Subs,guard_theorems) :- !, | |
881 | conjunction_to_list(Theorems,Subs). | |
882 | get_subformulas(guard_theorems(_Name,Parameters,Guard,Theorems),Subs,guard_theorems) :- !, | |
883 | append(Parameters,[b(implication(Guard,Theorems),pred,[])],Subs). | |
884 | %get_subformulas(cbc_path(_,Path,_),Subs) :- !, | |
885 | % append(Path,[X],XPath), | |
886 | % findall(cbc_path(LastStateID,XPath,X), sap:cb_path(LastStateID,XPath,_), Subs). | |
887 | get_subformulas(bind(_,_),S,K) :- !,S=[], K=none. | |
888 | get_subformulas(Node,[],none) :- format('No subformulas for ~w~n',[Node]). | |
889 | ||
890 | bv_syntaxtraversion(b(rec(Fields),_,_),Subs) :- | |
891 | maplist(transform_field,Fields,Subs1),!, | |
892 | Subs = Subs1. % Note: there are no new quantified names/identifiers; just field names | |
893 | bv_syntaxtraversion(TFormula,Subs) :- | |
894 | syntaxtraversion(TFormula,_,_,_,Subs1,Names), | |
895 | (Names = [] -> filter_trivial_expressions(Subs1,Subs) ; Subs = []). | |
896 | ||
897 | transform_field(field(Name,TVal),named_subformula(Name,TVal)). | |
898 | ||
899 | :- use_module(probsrc(preferences),[get_prob_application_type/1]). | |
900 | filter_trivial_expressions([],[]). | |
901 | filter_trivial_expressions([TI|Irest],Out) :- | |
902 | get_texpr_expr(TI,I),get_texpr_info(TI,Info), | |
903 | ( get_preference(show_bvisual_formula_functor_from,Lim), Lim>=0 -> Out = [TI|Orest] | |
904 | % only functor shown when expanding; we should show all sub formulas; otherwise it is confusing to the user | |
905 | ; get_prob_application_type(Type), Type \= tcltk -> Out = [TI|Orest] % in ProB2 we always just show the functor now | |
906 | ; is_trivial(I,Info) -> Out = Orest | |
907 | ; Out = [TI|Orest]), | |
908 | filter_trivial_expressions(Irest,Orest). | |
909 | ||
910 | % is_trivial/2 is true for expressions that should not appear as single nodes | |
911 | % in the evaluation tree, because they are too simple. | |
912 | % The first argument is the expression, the second its information list | |
913 | is_trivial(integer(_),_). | |
914 | is_trivial(integer_set(_),_). | |
915 | is_trivial(empty_set,_). | |
916 | is_trivial(boolean_true,_). | |
917 | is_trivial(boolean_false,_). | |
918 | is_trivial(bool_set,_). | |
919 | is_trivial(truth,_). | |
920 | is_trivial(falsity,_). | |
921 | is_trivial(identifier(_),Info) :- | |
922 | memberchk(given_set,Info). | |
923 | is_trivial(identifier(_),Info) :- | |
924 | memberchk(enumerated_set_element,Info). | |
925 | % TO DO: treat value(_) ? | |
926 | ||
927 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
928 | :- use_module(probsrc(specfile),[animation_minor_mode/1, csp_mode/0, b_or_z_mode/0, | |
929 | get_specification_description/2]). | |
930 | get_node_label(inv,invariants) :- animation_minor_mode(eventb),!. | |
931 | get_node_label(inv,I):- !, get_specification_description(invariant,I). | |
932 | get_node_label(axioms,axioms) :- animation_minor_mode(eventb),!. | |
933 | get_node_label(axioms,S):- !, get_specification_description(properties,S). | |
934 | get_node_label(variants,variants) :- animation_minor_mode(eventb),!. | |
935 | get_node_label(variants,'VARIANT') :- !. % not used there | |
936 | get_node_label(theoremsc,'theorems (on constants)') :- animation_minor_mode(eventb),!. | |
937 | get_node_label(theoremsc,'ASSUME (on constants)') :- animation_minor_mode(tla),!. | |
938 | get_node_label(theoremsc,'ALL ASSERTIONS (on CONSTANTS)') :- b_get_assertion_count(static,AllNr,MainNr), MainNr < AllNr, !. | |
939 | get_node_label(theoremsc,'ASSERTIONS (on CONSTANTS)') :- !. | |
940 | get_node_label(theoremscm,'MAIN ASSERTIONS (on CONSTANTS)') :- !. % should only trigger in B mode at the moment | |
941 | get_node_label(theoremsv,'theorems (on variables)') :- animation_minor_mode(eventb),!. | |
942 | get_node_label(theoremsv,'ALL ASSERTIONS (on VARIABLES)') :- b_get_assertion_count(dynamic,AllNr,MainNr), MainNr < AllNr, !. | |
943 | get_node_label(theoremsv,'ASSERTIONS (on VARIABLES)') :- !. | |
944 | get_node_label(theoremsvm,'MAIN ASSERTIONS (on VARIABLES)') :- !. % should only trigger in B mode at the moment | |
945 | get_node_label(sets,'sets') :- animation_minor_mode(eventb),!. | |
946 | get_node_label(sets,'SETS') :- !. | |
947 | get_node_label(freetypes,'inductive datatypes') :- animation_minor_mode(eventb),!. | |
948 | get_node_label(freetypes,'FREETYPES') :- !. | |
949 | get_node_label(goal,'GOAL') :- !. | |
950 | get_node_label(variables,'variables') :- animation_minor_mode(eventb),!. | |
951 | get_node_label(variables,'VARIABLES') :- !. | |
952 | get_node_label(constants,'constants') :- animation_minor_mode(eventb),!. | |
953 | get_node_label(constants,'CONSTANTS') :- !. | |
954 | get_node_label(guards_top_level,'event guards') :- animation_minor_mode(eventb),!. | |
955 | get_node_label(guards_top_level,'ACTIONS (guards)') :- animation_minor_mode(tla),!. | |
956 | get_node_label(guards_top_level,'OPERATIONS (guards/preconditions)') :- !. % GUARDS/PRE | |
957 | get_node_label(guards_subsidiary,'subsidiary event guards') :- animation_minor_mode(eventb),!. | |
958 | get_node_label(guards_subsidiary,'SUBSIDIARY ACTIONS (guards)') :- animation_minor_mode(tla),!. | |
959 | get_node_label(guards_subsidiary,'SUBSIDIARY OPERATIONS (guards/preconditions)') :- !. % GUARDS/PRE | |
960 | get_node_label(guard_theorems,'theorems (in guards)') :- !. | |
961 | get_node_label(user_formulas,'USER FORMULAS') :- !. | |
962 | get_node_label(definitions,'theory operators') :- animation_minor_mode(eventb),!. | |
963 | get_node_label(definitions,'DEFINITIONS') :- !. | |
964 | get_node_label(ltl_formulas,'LTL Formulas') :- !. | |
965 | %get_node_label(cbc_tests,'CBC_TESTS') :- !. | |
966 | get_node_label(channels,'channel') :- !. | |
967 | get_node_label(datatypes,'datatype') :- !. | |
968 | get_node_label(subtypes,'subtype') :- !. | |
969 | get_node_label(raw_state,'raw_state') :- !. | |
970 | get_node_label(Id,Label) :- | |
971 | stored_formula(Id,Formula),!, | |
972 | get_node_label2(Formula,Label). | |
973 | get_node_label(Id,'??') :- format('Unknown node: ~w~n',[Id]). | |
974 | ||
975 | get_node_label2(textnode(Text,_),Text) :- !. | |
976 | get_node_label2(textnode3(Text,_,_),Text) :- !. | |
977 | get_node_label2(bind(TID,_),ID) :- !, | |
978 | (is_texpr(TID),get_texpr_id(TID,R) -> ID = R ; ID = TID). | |
979 | get_node_label2(named_subformula(Name,_),Res) :- !, Res=Name. | |
980 | get_node_label2(guard(Name,_Parameters,_Guard),Name) :- !. | |
981 | get_node_label2(guard_theorems(Name,_Parameters,_Guard,_Theorems),Name) :- !. | |
982 | get_node_label2(variant(OpName,ConvOrAnt,_Variant),Name) :- !, | |
983 | ajoin([OpName,' |-> ',ConvOrAnt],Name). | |
984 | get_node_label2(ltl_named_formula(Name,_),Res) :- !, Res=Name. | |
985 | get_node_label2(ltl_formula(String,_Tree),Name) :- !, strip_newlines(String,Name). | |
986 | get_node_label2(TExpr,Label) :- | |
987 | is_texpr(TExpr),!, | |
988 | % Mode = unicode, latex or ascii; but unicode_mode makes Viewer slower | |
989 | with_bvisual2_translation_mode(get_node_label3(TExpr,Label)). | |
990 | get_node_label2(Term,Label) :- | |
991 | functor(Term,F,Arity), | |
992 | ajoin(['unknown node type: ',F,'/',Arity],Label). | |
993 | ||
994 | get_node_label3(TExpr,Label) :- | |
995 | with_bvisual2_translation_mode(translate_subst_or_bexpr_with_limit(TExpr,500,TS)), | |
996 | ( get_preference(show_bvisual_formula_functor_from,Lim), Lim>=0, | |
997 | get_texpr_top_level_symbol(TExpr,Functor,_,_OpType), | |
998 | %(OpType=infix ; OpType=postfix), | |
999 | (Lim=0 -> true ; atom_length(TS,Len), Len>=Lim) | |
1000 | -> %ajoin([Functor,' \x25AB\ ',TS],Label) % unicode small block / box | |
1001 | ajoin(['[',Functor, '] ',TS],Label0) | |
1002 | ; Label0=TS | |
1003 | ), | |
1004 | (animation_minor_mode(eventb), %maybe in future we also have proof info for Classical B | |
1005 | get_preference(show_bvisual_proof_info_icons,true), | |
1006 | get_discharged_info(TExpr,Proven,_) | |
1007 | -> (Proven=proven -> ajoin(['\x2705\ ',Label0],Label) % alternatives \x2705\ \x2713\ \x2714\ | |
1008 | ; ajoin([' \x25EF\ ',Label0],Label)) % x2B55 | |
1009 | ; Label=Label0). | |
1010 | ||
1011 | ||
1012 | :- dynamic bvisual2_translation_mode/1. | |
1013 | bvisual2_translation_mode(unicode). % any mode accepted by translate:set_translation_mode | |
1014 | set_bvisual2_translation_mode(X) :- retractall(bvisual2_translation_mode(_)), | |
1015 | assertz(bvisual2_translation_mode(X)). | |
1016 | ||
1017 | :- use_module(probsrc(translate), [with_translation_mode/2]). | |
1018 | :- use_module(probsrc(preferences), [temporary_set_preference/3,reset_temporary_preference/2]). | |
1019 | with_bvisual2_translation_mode(Call) :- | |
1020 | bvisual2_translation_mode(Mode), | |
1021 | temporary_set_preference(expand_avl_upto,5000,Chng), | |
1022 | call_cleanup(with_translation_mode(Mode,Call), | |
1023 | reset_temporary_preference(expand_avl_upto,Chng)). | |
1024 | ||
1025 | ||
1026 | register_top_level :- register_top_level(_). | |
1027 | register_top_level(Id) :- | |
1028 | ? | top_level2(Id,Formula,Subs), % print(register(Id,Subs)),nl, |
1029 | register_top_level_formula(Id,Formula,Subs), | |
1030 | fail. | |
1031 | register_top_level(_Id). | |
1032 | ||
1033 | ||
1034 | :- use_module(probsrc(specfile),[b_or_z_mode/0, classical_b_mode/0,spec_file_has_been_successfully_loaded/0]). | |
1035 | :- use_module(probsrc(b_global_sets),[all_elements_of_type/2, b_get_fd_type_bounds/3]). | |
1036 | :- use_module(probsrc(bmachine),[b_get_machine_goal/1]). | |
1037 | b_or_z_successsful_mode :- b_or_z_mode, | |
1038 | true. %spec_file_has_been_successfully_loaded. % make unit test fail | |
1039 | ||
1040 | % top_level2(SectionID, ValueNode, ListOfSubs) | |
1041 | top_level2(variables,textnode('',Variables),Variables) :- b_or_z_successsful_mode, | |
1042 | variables_should_be_included, | |
1043 | b_get_machine_variables_in_original_order(Variables). | |
1044 | top_level2(constants,textnode('',Constants),Constants) :- b_or_z_successsful_mode, | |
1045 | variables_should_be_included, | |
1046 | b_get_machine_constants(Constants). | |
1047 | top_level2(sets,textnode('',Sets),Sets) :- b_or_z_successsful_mode, | |
1048 | findall(bind(S,All), | |
1049 | bv_top_level_set(S,All),Sets), Sets \= []. | |
1050 | top_level2(freetypes,textnode('',Sets),Sets) :- b_or_z_successsful_mode, | |
1051 | findall(All, top_level_freetype(_Set,All),Sets), Sets \= []. | |
1052 | top_level2(goal,Goal,Subs) :- b_or_z_successsful_mode, | |
1053 | b_get_machine_goal(Goal), | |
1054 | conjunction_to_list(Goal,Subs). | |
1055 | top_level2(inv,Invariant,Subs) :- b_or_z_successsful_mode, | |
1056 | get_invariant_list_with_proof_info(Subs), | |
1057 | conjunct_predicates(Subs,Invariant). | |
1058 | top_level2(variants,textnode('',Variants),Variants) :- animation_minor_mode(eventb), | |
1059 | spec_file_has_been_successfully_loaded, | |
1060 | findall(variant(Name,ConvOrAnt,Variant), | |
1061 | b_get_operation_variant(Name,ConvOrAnt,Variant), | |
1062 | Variants), | |
1063 | Variants = [_|_]. | |
1064 | top_level2(axioms,Props,AllSubs) :- b_or_z_successsful_mode, | |
1065 | b_machine_has_constants_or_properties, | |
1066 | b_get_properties_from_machine(Props), | |
1067 | conjunction_to_list(Props,Subs), | |
1068 | findall(AddPred,b_machine_additional_property(AddPred),VSubs), % could be VALUES clause | |
1069 | (VSubs=[] -> AllSubs = Subs ; append(Subs,VSubs,AllSubs)). | |
1070 | top_level2(theoremsc,Pred,Assertions) :- b_or_z_successsful_mode, | |
1071 | b_get_static_assertions_from_machine(Assertions),Assertions\=[], | |
1072 | conjunct_predicates(Assertions,Pred). | |
1073 | top_level2(theoremscm,Pred,Assertions) :- b_or_z_successsful_mode, | |
1074 | b_get_assertions_from_main_machine(static,Assertions), | |
1075 | %Assertions\=[], % in case we have less: show that there are none | |
1076 | ? | b_get_assertion_count(static,AllNr,MainNr), MainNr < AllNr, |
1077 | conjunct_predicates(Assertions,Pred). | |
1078 | top_level2(theoremsv,Pred,Assertions) :- b_or_z_successsful_mode, | |
1079 | b_get_dynamic_assertions_from_machine(Assertions),Assertions\=[], | |
1080 | conjunct_predicates(Assertions,Pred). | |
1081 | top_level2(theoremsvm,Pred,Assertions) :- b_or_z_successsful_mode, | |
1082 | b_get_assertions_from_main_machine(dynamic,Assertions), | |
1083 | %Assertions\=[], % in case we have less: show that there are none | |
1084 | b_get_assertion_count(dynamic,AllNr,MainNr), MainNr < AllNr, | |
1085 | conjunct_predicates(Assertions,Pred). | |
1086 | top_level2(guards_top_level,textnode('',EventGuards),EventGuards) :- b_or_z_successsful_mode, | |
1087 | findall(guard(Name,Params,Guard), | |
1088 | get_top_level_guard(Name,Params,Guard),EventGuards), | |
1089 | EventGuards = [_|_]. | |
1090 | top_level2(guards_subsidiary,textnode('',EventGuards),EventGuards) :- b_or_z_successsful_mode, | |
1091 | findall(guard(Name,Params,Guard), | |
1092 | get_subsidiary_guard(Name,Params,Guard),EventGuards), | |
1093 | EventGuards = [_|_]. | |
1094 | top_level2(guard_theorems,textnode('',EventGuards),EventGuards) :- b_or_z_successsful_mode, | |
1095 | findall(guard_theorems(Name,Params,Guard,GuardTheorems), | |
1096 | ( b_get_machine_operation(Name,_,_,TBody), | |
1097 | get_texpr_expr(TBody,Body), | |
1098 | Body = rlevent(_Name,_Section,_Status,Params,Guard,Theorems, | |
1099 | _Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents), | |
1100 | Theorems \= [], | |
1101 | conjunct_predicates(Theorems,GuardTheorems) | |
1102 | ), | |
1103 | EventGuards), | |
1104 | EventGuards = [_|_]. | |
1105 | top_level2(user_formulas,textnode('',UserPredicates),UserPredicates) :- b_or_z_successsful_mode, | |
1106 | findall(UP,subnode(user_formulas,UP),UserPredicates), UserPredicates\=[]. | |
1107 | top_level2(definitions,textnode('',Defs),Defs) :- b_or_z_successsful_mode, | |
1108 | findall(Node,get_definition(Node),Defs), Defs\=[]. | |
1109 | top_level2(ltl_formulas,textnode('',Defs),Defs) :- b_or_z_successsful_mode, | |
1110 | findall(Node,get_ltl_named_formula(Node),Defs), Defs\=[]. | |
1111 | top_level2(channels,textnode('',Channels),Channels) :- csp_mode, spec_file_has_been_successfully_loaded, | |
1112 | findall(Node,get_csp_channel(Node),Cs), Cs\=[], sort(Cs,Channels). | |
1113 | top_level2(datatypes,textnode('',DT),DT) :- csp_mode, spec_file_has_been_successfully_loaded, | |
1114 | findall(Node,get_csp_datatype(Node),Cs), Cs\=[], sort(Cs,DT). | |
1115 | top_level2(subtypes,textnode('',DT),DT) :- csp_mode, spec_file_has_been_successfully_loaded, | |
1116 | findall(Node,get_csp_subtype(Node),Cs), Cs\=[], sort(Cs,DT). | |
1117 | top_level2(raw_state,raw_state_pp,[]) :- \+ b_or_z_mode, | |
1118 | spec_file_has_been_successfully_loaded. | |
1119 | % we are now using a custom tree_inspector for the CBC Tests | |
1120 | /* top_level2(cbc_tests,textnode('',Paths),Paths) :- b_or_z_mode, | |
1121 | get_preference(user_is_an_expert_with_accessto_source_distribution,true), | |
1122 | %sap:cb_path(_,[_],_), % we have generated at least one test-case | |
1123 | % TO DO: we need a way to refresh this information after test-cases have been generated | |
1124 | % currently the only way seems to close the evaluation view, reload, generate the tests and then open the view | |
1125 | Paths = [cbc_path(root,[],'INITIALISATION')]. | |
1126 | */ | |
1127 | ||
1128 | :- use_module(probcspsrc(haskell_csp),[channel_type_list/2, dataTypeDef/2, subTypeDef/2]). | |
1129 | :- use_module(probsrc(translate),[translate_cspm_expression/2]). | |
1130 | get_csp_channel(bind(Channel,string(TypeString))) :- | |
1131 | channel_type_list(Channel,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1132 | translate_cspm_expression(dotTuple(TypeList),TypeString). | |
1133 | get_csp_datatype(bind(DT,string(TypeString))) :- | |
1134 | dataTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1135 | translate_cspm_expression(dataTypeDef(TypeList),TypeString). | |
1136 | get_csp_subtype(bind(DT,string(TypeString))) :- | |
1137 | subTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1138 | translate_cspm_expression(dataTypeDef(TypeList),TypeString). | |
1139 | ||
1140 | :- use_module(probsrc(bmachine)). | |
1141 | :- use_module(probsrc(pref_definitions),[b_get_set_pref_definition/3]). | |
1142 | get_definition(textnode('GOAL',Subs)) :- b_get_machine_goal(Goal), conjunction_to_list(Goal,Subs). | |
1143 | get_definition(bind('SCOPE',string(S))) :- b_get_machine_searchscope(S). | |
1144 | get_definition(textnode('HEURISTIC_FUNCTION',[F])) :- b_get_machine_heuristic_function(F). | |
1145 | get_definition(textnode(STR,[F])) :- b_get_machine_animation_expression(STR,F). | |
1146 | get_definition(textnode(Name,[F])) :- b_get_machine_animation_function(F,Nr), | |
1147 | number_codes(Nr,NC), append("ANIMATION_FUNCTION",NC,C), atom_codes(Name,C). | |
1148 | get_definition(textnode(Name,[Term])) :- b_get_machine_setscope(SetName,Term), | |
1149 | atom_codes(SetName,NC), append("scope_",NC,C), atom_codes(Name,C). | |
1150 | get_definition(textnode(Name,[b(integer(Nr),integer,[])])) :- b_get_machine_operation_max(OpName,Nr), | |
1151 | atom_codes(OpName,NC), append("MAX_OPERATIONS_",NC,C), atom_codes(Name,C). | |
1152 | get_definition(bind(Name,string(F))) :- | |
1153 | ? | b_get_definition_string_from_machine(Name,F), atom_codes(Name,C), \+ append("SET_PREF_",_,C). |
1154 | get_definition(textnode(Prefix,Subs)) :- | |
1155 | ? | member(Prefix,['CUSTOM_GRAPH_EDGES', 'CUSTOM_GRAPH_NODES', |
1156 | 'VISB_SVG_OBJECTS', 'VISB_SVG_UPDATES', | |
1157 | 'VISB_SVG_EVENTS', 'VISB_SVG_HOVERS']), | |
1158 | findall(named_subformula(DefName,Body), | |
1159 | get_useful_definition_for_bvisual2(expression,Prefix,DefName,_Pos,Body), | |
1160 | Subs), Subs \= []. | |
1161 | get_definition(named_subformula(DefName,Body)) :- | |
1162 | ? | member(DefName,['CUSTOM_GRAPH', |
1163 | 'VISB_SVG_BOX', 'VISB_SVG_CONTENTS']), % require exact match, VISB_JSON_FILE shown above | |
1164 | get_useful_definition_for_bvisual2(expression,DefName,DefName,_Pos,Body). | |
1165 | get_definition(Res) :- | |
1166 | ? | b_get_set_pref_definition(DefName,_String,F), |
1167 | ? | (extract_value(F,Val) -> Res = bind(DefName,Val) ; Res = textnode(DefName,[F])). |
1168 | get_definition(textnode3(Header,DefBodyStr, | |
1169 | [textnode3('Theory',FullThName,[]), | |
1170 | textnode3('Body',DefBodyStr,[]) | Tail | |
1171 | ])) :- | |
1172 | ? | stored_operator_direct_definition(Name,ProjName,TheoryName,Parameters,RawDefBody,RawWD,ParaTypes,_Kind), |
1173 | ajoin([ProjName,'.',TheoryName],FullThName), | |
1174 | translate_eventb_direct_definition_header(Name,Parameters,Header), | |
1175 | with_bvisual2_translation_mode(translate_eventb_direct_definition_body(RawDefBody,DefBodyStr)), | |
1176 | (ParaTypes = [] -> Tail = Tail2 | |
1177 | ; debug_mode(off), \+ ground(ParaTypes) -> Tail=Tail2 % non-ground types are for destructors, ... are not useful for average user | |
1178 | ; Tail = [textnode3('Type Parameters',TypeParaStr,[])|Tail2], | |
1179 | write_term_to_codes(ParaTypes,PC,[]), | |
1180 | atom_codes(TypeParaStr,PC) | |
1181 | ), | |
1182 | (RawWD=truth(_) -> Tail2=[] | |
1183 | ; Tail2 = [textnode3('WD Condition',WDStr,[])], | |
1184 | with_bvisual2_translation_mode(translate_eventb_direct_definition_body(RawWD,WDStr)) | |
1185 | ). | |
1186 | % TODO: show mapped Event-B and recursive operators; also: above still shown as string and type paras not shown | |
1187 | % TO DO: we could try and get more complex definitions if get_preference(type_check_definitions,true), see type_check_definitions; or we could just pretty print the RAW ast using transform_raw; | |
1188 | % NOTE: special definitions are also declared in | |
1189 | % - procDoSyntaxColouring in main_prob_tcltk_gui.tcl | |
1190 | % - isProBSpecialDefinitionName in Utils.java in de.be4.classicalb.core.parser.util | |
1191 | extract_value(b(string(S),_,_),string(S)). | |
1192 | extract_value(b(integer(S),_,_),int(S)). | |
1193 | extract_value(b(boolean_true,_,_),pred_true). | |
1194 | extract_value(b(boolean_false,_,_),pred_false). | |
1195 | ||
1196 | get_useful_definition_for_bvisual2(Type,Prefix,DefName,DefPos,Body) :- | |
1197 | b_sorted_b_definition_prefixed(Type,Prefix,DefName,DefPos), | |
1198 | b_get_typed_definition(DefName,[variables],Body). | |
1199 | ||
1200 | ||
1201 | % ASSERT_LTL | |
1202 | % at the top-level we generate named formulas; we only parse when expanding later | |
1203 | % solves issues e.g., in CSP-B mode where the formulas use CSP constructs but the csp-guide has not been added yet | |
1204 | % see tests 1257, 1259, 1644, 1647 | |
1205 | get_ltl_named_formula(ltl_named_formula(FullName,FormulaAsString)) :- | |
1206 | get_ltl_formula_strings(Names,Strings), | |
1207 | nth1(Nr,Names,Name), | |
1208 | ajoin(['ASSERT_LTL',Name],FullName), % in CSP mode this would actually be assert Main |= LTL "formula" | |
1209 | (nth1(Nr,Strings,FormulaAsString) -> true). | |
1210 | ||
1211 | gen_ltl_bv_sub(Tree,ltl_formula(String,Tree)) :- | |
1212 | pp_ltl_formula(Tree,String). | |
1213 | ||
1214 | get_bv_ltl_sub_formulas(ap(bpred(Pred)),Subs) :- !, Subs = [Pred]. | |
1215 | get_bv_ltl_sub_formulas(LTLTee,BV_Subs) :- | |
1216 | get_ltl_sub_formulas(LTLTee,_,LTLSubs),!, | |
1217 | maplist(gen_ltl_bv_sub,LTLSubs,BV_Subs). | |
1218 | get_bv_ltl_sub_formulas(_,[]). | |
1219 | ||
1220 | ||
1221 | :- use_module(probsrc(b_operation_guards),[get_unsimplified_operation_enabling_condition/5]). | |
1222 | :- use_module(probsrc(bmachine),[b_top_level_operation/1]). | |
1223 | get_top_level_guard(OpName,Params,Guard) :- | |
1224 | ? | b_top_level_operation(OpName), |
1225 | get_unsimplified_operation_enabling_condition(OpName,Params,Guard,_BecomesSuchVars,_Precise), | |
1226 | \+ is_initialisation_op(OpName). | |
1227 | get_subsidiary_guard(OpName,Params,Guard) :- % get guards for non-top-level operations | |
1228 | ? | get_unsimplified_operation_enabling_condition(OpName,Params,Guard,_BecomesSuchVars,_Precise), |
1229 | \+ b_top_level_operation(OpName), | |
1230 | \+ is_initialisation_op(OpName). | |
1231 | ||
1232 | is_initialisation_op('$setup_constants'). | |
1233 | is_initialisation_op('$initialise_machine'). | |
1234 | ||
1235 | :- use_module(probsrc(custom_explicit_sets),[construct_interval_closure/3]). | |
1236 | :- use_module(probsrc(kernel_freetypes),[registered_freetype/2]). | |
1237 | :- use_module(probsrc(bmachine),[b_get_machine_set/2]). | |
1238 | :- use_module(probsrc(b_global_sets),[b_replaced_global_set/2]). | |
1239 | bv_top_level_set(TSet,AllEls) :- b_or_z_mode, | |
1240 | ? | b_get_machine_set(Set,TSet), |
1241 | (b_get_fd_type_bounds(Set,_Low,inf) | |
1242 | -> %L1 is Low+1, L2 is Low+2, | |
1243 | %AllEls= [fd(Low,Set),fd(L1,Set),fd(L2,Set),string('...')] % TODO: avoid type error | |
1244 | AllEls = string('infinite deferred set') | |
1245 | ; all_elements_of_type(Set,AllEls)). | |
1246 | bv_top_level_set(b(identifier(ID),any,[]),string(TS)) :- % replaced by record construction /detection | |
1247 | ? | b_replaced_global_set(ID,NewTypeExpr), |
1248 | with_bvisual2_translation_mode(translate_subst_or_bexpr_with_limit(NewTypeExpr,500,TS)). | |
1249 | bv_top_level_set(b(identifier('INT'),set(integer),[]),INTVAL) :- % we can return both typed ids and atomic ids | |
1250 | ? | classical_b_mode, % INT only exists in pure B mode |
1251 | get_preference(maxint,MAXINT), get_preference(minint,MININT), | |
1252 | construct_interval_closure(MININT,MAXINT,INTVAL). | |
1253 | ||
1254 | top_level_freetype(Set,textnode3(TopSet,'',AllCases)) :- | |
1255 | animation_minor_mode(eventb), % here types contain Prolog variables (polymorphism) + we have the constant(_) type | |
1256 | ? | registered_freetype(SetP,Cases), |
1257 | (SetP =.. [Set|TypeParas] -> true ; add_error(bvisual2,'Cannot instantiate type paras:',SetP)), | |
1258 | get_freetype_params(Set,TypeParaNames,TypeParas), | |
1259 | (TypeParaNames = [] -> TopSet = Set ; ajoin_with_sep(TypeParaNames,',',Ps),ajoin([Set,'(',Ps,')'],TopSet)), | |
1260 | findall(textnode3(Case,CaseString,Subs), | |
1261 | (member(case(CaseP,T),Cases),functor(CaseP,Case,_), | |
1262 | bv_pretty_type(T,TS), ajoin([Case,':',TS],CaseString), | |
1263 | findall(textnode3(Destructor,TD,[]),get_destructor_for_freetype(SetP,Case,Destructor,TD),Subs) | |
1264 | ),AllCases). | |
1265 | top_level_freetype(Set,AllCases) :- b_or_z_mode, \+ animation_minor_mode(eventb), | |
1266 | ? | registered_freetype(Set,Cases), |
1267 | % TO DO: improve presentation, maybe use translate:type_set(_Type,TDom) | |
1268 | findall(field(Case,Value), | |
1269 | (member(case(Case,T),Cases),gen_case_value(T,Value)), | |
1270 | Fields), | |
1271 | AllCases = bind(Set,struct(Fields)). | |
1272 | ||
1273 | get_freetype_params(Set,TypeParaNames,VirtualParaTypes) :- | |
1274 | (stored_operator_direct_definition(Set,_Proj,_Theory,TypeParaNames,_Def,_WD,_TypeParas, datatype_definition) | |
1275 | -> maplist(convert_name_to_type,TypeParaNames,VirtualParaTypes) | |
1276 | ; add_error(bvisual2,'Unknown freetype:',Set),TypeParaNames=[]). | |
1277 | convert_name_to_type(ParaName,global(ParaName)) :- atom(ParaName),!. % so that pretty_type works | |
1278 | convert_name_to_type(Type,_) :- add_error(bvisual,'Cannot convert parameter type:',Type). | |
1279 | get_destructor_for_freetype(Set,Case,Name,TypeAsString) :- | |
1280 | ? | stored_operator_direct_definition(Name,_Proj,_Theory,[argument(Case,_CType)],_Def,_WD,_TypeParameters, |
1281 | destructor(Set,ReturnType)), | |
1282 | bv_pretty_type(ReturnType,TypeAsString). | |
1283 | ||
1284 | :- use_module(probsrc(b_global_sets),[b_type2_set/2]). | |
1285 | gen_case_value(constant(List),Res) :- List=[_], !, Res=[]. % the constant has no arguments, provide empty set | |
1286 | gen_case_value(Type,Value) :- b_type2_set(Type,Value). | |
1287 | ||
1288 | bv_pretty_type(Type,Res) :- with_bvisual2_translation_mode(pretty_type(Type,TS)),!,Res=TS. | |
1289 | bv_pretty_type(Type,Res) :- add_error(bvisual2,'Cannot convert type:',Type), Res='?'. | |
1290 | ||
1291 | register_top_level_formula(Id,Formula,Subs) :- | |
1292 | assertz( stored_formula(Id,Formula) ), | |
1293 | register_formulas(Subs,Id,_), | |
1294 | assertz( top_level_node(Id) ), | |
1295 | assertz( expanded(Id) ). | |
1296 | ||
1297 | register_formulas([],_Parent,[]). | |
1298 | register_formulas([Formula|Frest],Parent,[SubId|Srest]) :- | |
1299 | register_formula(Formula,Parent,SubId), | |
1300 | register_formulas(Frest,Parent,Srest). | |
1301 | register_formula(Formula,Parent,Id) :- | |
1302 | get_new_id(Id), | |
1303 | assertz( stored_formula(Id,Formula) ), | |
1304 | assertz( subnode(Parent,Id) ), | |
1305 | assertz( supernode(Id,Parent) ). | |
1306 | ||
1307 | get_new_id(Id) :- | |
1308 | (retract(id_counter(Old)) -> true ; Old = 0), | |
1309 | Id is Old+1, | |
1310 | assertz( id_counter(Id) ). | |
1311 | ||
1312 | ||
1313 | disjunction_to_list(A,B,Out) :- | |
1314 | disjunction_to_list2(A,[B],Out,[]). | |
1315 | disjunction_to_list2(Expr,Rest) --> | |
1316 | {get_texpr_expr(Expr,disjunct(A,B)),!}, | |
1317 | disjunction_to_list2(A,[B|Rest]). | |
1318 | disjunction_to_list2(Expr,Rest) --> | |
1319 | [Expr],disjunction_to_list3(Rest). | |
1320 | disjunction_to_list3([]) --> !. | |
1321 | disjunction_to_list3([H|T]) --> disjunction_to_list2(H,T). | |
1322 | ||
1323 | ||
1324 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
1325 | % some predicates for the support of the Tcl/Tk UI | |
1326 | ||
1327 | call_with_temp_preference(Prefs,Values,Call) :- | |
1328 | maplist(get_preference,Prefs,OldValues), | |
1329 | maplist(set_preference,Prefs,Values), | |
1330 | call_cleanup(Call,maplist(set_preference,Prefs,OldValues)),!. | |
1331 | ||
1332 | bv_get_values_unlimited(Ids,StateId,Values) :- | |
1333 | assertz(get_unlimited_value), | |
1334 | call_cleanup(call_with_temp_preference([expand_avl_upto],[-1],bv_get_values(Ids,StateId,Values)), | |
1335 | retractall(get_unlimited_value)). | |
1336 | ||
1337 | bv_get_value_unlimited(Id,StateId,Value) :- | |
1338 | visited_expression(StateId,State),!, | |
1339 | get_preference(time_out,Timeout), | |
1340 | assertz(get_unlimited_value), | |
1341 | call_cleanup(call_with_temp_preference([expand_avl_upto],[-1],bv_get_value(Id,State,StateId,Timeout,Value)), | |
1342 | retractall(get_unlimited_value)). | |
1343 | bv_get_value_unlimited(_Id,_StateId,e('unknown state')). | |
1344 | ||
1345 | bv_get_value_unlimited_and_unprocessed(Id,StateId,Value) :- | |
1346 | visited_expression(StateId,State),!, | |
1347 | get_preference(time_out,Timeout), | |
1348 | call_with_temp_preference([expand_avl_upto],[-1],bv_get_value_unprocessed(Id,State,StateId,Timeout,Value)). | |
1349 | bv_get_value_unlimited_and_unprocessed(_Id,_StateId,e('unknown state')). | |
1350 | ||
1351 | % get the raw value in Prolog encoding | |
1352 | bv_get_btvalue(Id,StateId,BExpr,BValue) :- | |
1353 | bv_get_value_unlimited_and_unprocessed(Id,StateId,V),!, | |
1354 | (V=btvalue(Value,E) | |
1355 | -> BExpr=E,BValue=Value | |
1356 | ; V=i -> add_error(bvisual2,'Cannot obtain value of inactive entry:',Id),fail | |
1357 | ; add_error(bvisual2,'Cannot extract value of entry:',Id:V),fail). | |
1358 | bv_get_btvalue(Id,_,_,_) :- | |
1359 | add_error(bvisual2,'Unknown identifier or section, cannot find value:',Id),fail. | |
1360 | ||
1361 | ||
1362 | :- use_module(probsrc(tools_commands),[edit_file/2]). | |
1363 | :- use_module(probsrc(error_manager),[extract_file_line_col/6,extract_span_description/2]). | |
1364 | bv_show_formula_origin(Id,Desc) :- | |
1365 | bv_get_stored_formula_expr(Id,Formula), | |
1366 | extract_file_line_col(Formula,FILE,LINE,_COL,_Erow,_Ecol), | |
1367 | extract_span_description(Formula,Desc), | |
1368 | edit_file(FILE,LINE). | |
1369 | ||
1370 | :- use_module(probsrc(bsyntaxtree),[get_texpr_description/2, get_texpr_labels/2]). | |
1371 | bv_formula_description(Id,Desc) :- | |
1372 | bv_get_stored_formula_expr(Id,Formula), | |
1373 | is_texpr(Formula), | |
1374 | get_texpr_description(Formula,Desc). | |
1375 | ||
1376 | % Extended description with additional information, | |
1377 | % such as the formula label and the number of sub-elements. | |
1378 | % Tcl/Tk displays this description in the context menu in the evaluation view. | |
1379 | % The ProB 2 UI displays similar information in tooltips in the state view, | |
1380 | % but those tooltips are constructed on the Java side. | |
1381 | bv_formula_extended_description(Id,Desc) :- | |
1382 | bvisual2_translation_mode(Mode), | |
1383 | with_translation_mode(Mode, bv_formula_extended_description_aux(Id,Desc)). | |
1384 | bv_formula_extended_description_aux(Id,Desc) :- | |
1385 | bv_get_stored_formula_expr(Id,Formula), | |
1386 | is_texpr(Formula), | |
1387 | (get_texpr_description(Formula,Desc0) | |
1388 | -> (get_first_label(Formula,Label) -> ajoin(['@',Label,': ',Desc0],Desc1) | |
1389 | ; Desc1=Desc0 | |
1390 | ) | |
1391 | ; get_first_label(Formula,Desc1) | |
1392 | % ; Desc = 'No description available via @desc pragma') | |
1393 | ; Desc1 = '' | |
1394 | ), | |
1395 | (bv_formula_discharged_description(Id,DInfo) | |
1396 | -> ajoin_with_nl(Desc1,DInfo,Desc2) | |
1397 | ; Desc2 = Desc1), | |
1398 | (bv_formula_size_description(Id,SzeD) | |
1399 | -> ajoin_with_nl(Desc2,SzeD,Desc3) | |
1400 | ; Desc3 = Desc2), | |
1401 | (texpr_contains_wd_condition(Formula) | |
1402 | -> ajoin_with_nl(Desc3,'Formula has wd condition',Desc4) | |
1403 | ; Desc4 = Desc3), | |
1404 | (display_type(Formula,TS) | |
1405 | -> ajoin(['Type: ',TS],TTS), ajoin_with_nl(Desc4,TTS,Desc) | |
1406 | ; Desc = Desc4), | |
1407 | Desc \= ''. | |
1408 | ||
1409 | :- use_module(probsrc(translate),[pretty_type/2]). | |
1410 | display_type(b(_,T,_),TS) :- \+ do_not_show_type(T), bv_pretty_type(T,TS). | |
1411 | % ltl | |
1412 | do_not_show_type(pred). | |
1413 | do_not_show_type(subst). | |
1414 | do_not_show_type(op(_)). | |
1415 | ||
1416 | ajoin_with_nl('',D2,Res) :- !, Res=D2. | |
1417 | ajoin_with_nl(D1,D2,Res) :- ajoin([D1,'\n',D2],Res). | |
1418 | ||
1419 | ||
1420 | bv_formula_discharged_info(Id,DischargedInfo) :- | |
1421 | bv_formula_discharged_info(Id,_,DischargedInfo). | |
1422 | bv_formula_discharged_info(Id,Proven,DischargedInfo) :- | |
1423 | bv_get_stored_formula_expr(Id,Formula), | |
1424 | get_discharged_info(Formula,Proven,DischargedInfo). | |
1425 | ||
1426 | get_discharged_info(Formula,Proven,DischargedInfo) :- | |
1427 | is_texpr(Formula), | |
1428 | get_texpr_info(Formula,I), | |
1429 | member(proof_status(Proven,DischargedInfo),I),!. | |
1430 | ||
1431 | :- use_module(probsrc(tools_strings),[ajoin_with_sep/3]). | |
1432 | bv_formula_discharged_description(Id,Desc) :- | |
1433 | bv_formula_discharged_info(Id,Proven,L), | |
1434 | ajoin_with_sep(L,',',DInfo), | |
1435 | ajoin(['Proof status is ',Proven,': ',DInfo],Desc). | |
1436 | ||
1437 | % extract some info about size and top-level function symbol of an entry: | |
1438 | bv_formula_size_description(Id,Desc) :- | |
1439 | get_nr_of_subformulas(Id,Nr), Nr>=1, | |
1440 | (stored_formula(Id,F), is_texpr(F) | |
1441 | -> SubName = 'subformulas', | |
1442 | (get_texpr_top_level_symbol(F,Symbol,_,_) | |
1443 | -> ajoin(['Formula (',Symbol,')'],Entry) ; Entry='Formula') | |
1444 | ; atom(Id),get_node_label(Id,SubName) | |
1445 | -> Entry = 'Entry' | |
1446 | ; SubName = 'children', Entry = 'Entry' | |
1447 | ), | |
1448 | ajoin([Entry, ' contains ', Nr, ' ', SubName],Desc). | |
1449 | ||
1450 | % compute number of subformulas/entries of a node: | |
1451 | get_nr_of_subformulas(Id,Nr) :- expanded(Id),!, | |
1452 | findall(1, subnode(Id,_), L), | |
1453 | length(L,Nr). | |
1454 | get_nr_of_subformulas(Id,Nr) :- | |
1455 | bv_get_stored_formula_expr(Id,Formula), | |
1456 | findall(1,get_subformulas(Formula,_,_Kind),L), | |
1457 | length(L,Nr). | |
1458 | ||
1459 | % get the top-level symbol of a formula | |
1460 | bv_get_formula_functor_symbol(Id,Symbol) :- | |
1461 | stored_formula(Id,F), is_texpr(F), | |
1462 | \+ top_level_node(Id), | |
1463 | bvisual2_translation_mode(Mode), | |
1464 | with_translation_mode(Mode, get_texpr_top_level_symbol(F,Symbol,_,_)). | |
1465 | ||
1466 | bv_is_child_formula(Id) :- \+ bv_is_topmost_formula(Id). | |
1467 | % check if node is topmost formula, attached to a top_level_node | |
1468 | bv_is_topmost_formula(Id) :- | |
1469 | supernode(Id,Super), | |
1470 | top_level_node(Super). | |
1471 | ||
1472 | ||
1473 | bv_formula_labels(Id,Labels) :- | |
1474 | bv_get_stored_formula_expr(Id,Formula), | |
1475 | is_texpr(Formula), | |
1476 | (get_texpr_labels(Formula,Labels) -> true). | |
1477 | ||
1478 | get_first_label(Formula,Desc) :- get_texpr_labels(Formula,Lbls) -> [Desc|_]=Lbls. | |
1479 | ||
1480 | bv_is_typed_formula(Id) :- bv_get_stored_formula_expr(Id,Formula), is_texpr(Formula). | |
1481 | bv_is_typed_predicate(Id) :- bv_get_stored_formula_expr(Id,Formula), Formula = b(_,pred,_). | |
1482 | bv_is_typed_identifier(Id,IDName) :- bv_get_stored_formula_expr(Id,Formula), Formula = b(identifier(IDName),_,_). | |
1483 | ||
1484 | bv_get_stored_formula_expr(Id,Formula) :- | |
1485 | stored_formula(Id,Stored), | |
1486 | extract_typed_formua(Stored,Formula). | |
1487 | ||
1488 | extract_typed_formua(bind(LHS,_),Formula) :- !, Formula=LHS. | |
1489 | extract_typed_formua(guard(Name,Parameters,Guard),Formula) :- !, | |
1490 | get_guard_formula(Parameters,Guard,GF), | |
1491 | (b_get_operation_description(Name,Desc) -> add_texpr_description(GF,Desc,Formula) | |
1492 | ; Formula = GF). | |
1493 | extract_typed_formua(variant(_Name,_ConvOrAnt,Variant),Formula) :- !, Formula=Variant. | |
1494 | extract_typed_formua(named_subformula(_,Formula),Res) :- !, Res=Formula. | |
1495 | extract_typed_formua(TF,TF). | |
1496 | ||
1497 | get_guard_formula([],Guard,Res) :- !, Res=Guard. | |
1498 | get_guard_formula(Parameters,Guard,Expr) :- create_or_merge_exists(Parameters,Guard,Expr). | |
1499 | get_guard_theorems_formula([],_Guard,Theorems,Res) :- !, Res=Theorems. | |
1500 | get_guard_theorems_formula(Parameters,Guard,Theorems,Expr) :- | |
1501 | create_forall(Parameters,b(implication(Guard,Theorems),pred,[]),Expr). | |
1502 | ||
1503 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
1504 | % | |
1505 | :- use_module(probsrc(tools_io)). | |
1506 | bv_print_to_file(IdList,StateId,Filename) :- | |
1507 | call_with_temp_preference([expand_avl_upto],[-1],bv_print_to_file_aux(IdList,StateId,Filename)). | |
1508 | bv_print_to_file_aux(IdList,StateId,Filename) :- | |
1509 | safe_open_file(Filename,write,S,[encoding(utf8)]), | |
1510 | bv_print_to_stream_l(IdList,S,StateId,false), | |
1511 | close(S). | |
1512 | ||
1513 | bv_print_to_stream_l([],_S,_StateId,_WriteAnd). | |
1514 | bv_print_to_stream_l([Id|Rest],S,StateId,WriteAnd) :- | |
1515 | bv_print_to_stream(Id,S,StateId,OutType,WriteAnd), | |
1516 | (OutType=predicate -> WriteAnd2=true ; WriteAnd2=WriteAnd), | |
1517 | bv_print_to_stream_l(Rest,S,StateId,WriteAnd2). | |
1518 | ||
1519 | bv_print_to_stream(Id,S,StateId,predicate,WriteAnd) :- | |
1520 | stored_formula(Id,Formula), | |
1521 | bv_print_formula_to_stream(Formula,Id,S,StateId,WriteAnd),!,nl(S). | |
1522 | bv_print_to_stream(Id,S,StateId,other,_WriteAnd) :- | |
1523 | get_node_label(Id,Label), | |
1524 | bv_get_values([Id],StateId,[Value]), | |
1525 | write(S,'/* '),write(S,Label),write(S,': '), | |
1526 | bv_print_std_value(Value,S),write(S,' */\n'). | |
1527 | bv_print_std_value(e(Msg),S) :- write(S,'ERROR( '), write(S,Msg), write(S,' )'). | |
1528 | bv_print_std_value(p(Value),S) :- write(S,Value). | |
1529 | bv_print_std_value(v(Value),S) :- write(S,Value). | |
1530 | bv_print_std_value(i,S) :- write(S,'INACTIVE'). | |
1531 | bv_print_std_value(bv_info(I),S) :- write(S,I). | |
1532 | ||
1533 | bv_print_formula_to_stream(Formula,Id,S,StateId,WriteAnd) :- | |
1534 | is_texpr(Formula), | |
1535 | get_texpr_type(Formula,Type), | |
1536 | bv_get_value_unlimited_and_unprocessed(Id,StateId,Value), | |
1537 | bv_print_formula_to_stream2(Type,Formula,Value,S,WriteAnd). | |
1538 | ||
1539 | bv_print_formula_to_stream2(pred,Formula,p(Value),S,WriteAnd) :- !, | |
1540 | bv_print_predicate_to_stream(Value,Formula,S,WriteAnd). | |
1541 | bv_print_formula_to_stream2(Type,Formula,btvalue(Value,_),S,WriteAnd) :- !, | |
1542 | create_texpr(value(Value),Type,[],TValue), | |
1543 | create_texpr(equal(Formula,TValue),pred,[],Equal), | |
1544 | write_bexpression(S,Equal,WriteAnd). | |
1545 | ||
1546 | bv_print_predicate_to_stream(true,Formula,S,WriteAnd) :- | |
1547 | write_bexpression(S,Formula,WriteAnd). | |
1548 | bv_print_predicate_to_stream(false,Formula,S,WriteAnd) :- | |
1549 | create_texpr(negation(Formula),pred,[],NegatedFormula), | |
1550 | write(S,' /* FALSE */ '),write_bexpression(S,NegatedFormula,WriteAnd). | |
1551 | ||
1552 | write_bexpression(Stream,Expression,WriteAnd) :- | |
1553 | (WriteAnd = true -> write(Stream,' & \n') ; true), | |
1554 | translate_bexpression_to_codes(Expression,Codes), | |
1555 | put_codes(Codes,Stream). | |
1556 | ||
1557 | bv_write_all_variables_and_constants(StateId,Filename) :- | |
1558 | call_with_temp_preference([expand_avl_upto],[-1],bv_write_all_variables_and_constants_aux(StateId,Filename)). | |
1559 | bv_write_all_variables_and_constants_aux(StateId,Filename) :- | |
1560 | bv_expand_formula(constants,_CLabel,ConstNodes), | |
1561 | bv_expand_formula(variables,_VLabel,VarNodes), | |
1562 | append(ConstNodes,VarNodes,Subnodes),expand_all(Subnodes), | |
1563 | append([constants|ConstNodes],[variables|VarNodes],Nodes), | |
1564 | bv_print_to_file(Nodes,StateId,Filename). | |
1565 | expand_all(Subnodes) :- | |
1566 | member(Node,Subnodes), | |
1567 | bv_expand_formula(Node,_,_), | |
1568 | fail. | |
1569 | expand_all(_Subnodes). | |
1570 | ||
1571 | ||
1572 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
1573 | :- register_event_listener(clear_specification,clear_bvisual, | |
1574 | 'Clear module bvisual2.'). | |
1575 | :- register_event_listener(specification_initialised,reset_bvisual, | |
1576 | 'Initialise module bvisual2.'). | |
1577 | :- register_event_listener(change_of_animation_mode,reset_bvisual, | |
1578 | 'Initialise module bvisual2.'). | |
1579 | ||
1580 | :- use_module(probsrc(self_check)). | |
1581 | % a very small use-case: | |
1582 | :- assert_must_succeed(( | |
1583 | reset_bvisual, | |
1584 | bv_get_top_level(T), %print(top(T)),nl, | |
1585 | %T == [variables,constants,inv], | |
1586 | member(inv,T), | |
1587 | bv_expand_formula(inv,Text,Sub), | |
1588 | %print(expand(Text,Sub)),nl, | |
1589 | Text == 'INVARIANT', | |
1590 | Sub = [H|_], | |
1591 | bv_expand_formula(H,_Text1,_Sub1), | |
1592 | %print(expand1(Text1,Sub1)),nl, | |
1593 | bv_get_values(Sub,root,Values), | |
1594 | %print(values(Values)),nl, % should be [i,...] or e('unknown state') | |
1595 | Values = [VI|_], (VI=i ; VI=e(_)), | |
1596 | reset_bvisual | |
1597 | )). | |
1598 | ||
1599 | % example bv_get_top_level_formula(theoremsc,Txt,Labels,Vals) | |
1600 | ||
1601 | bv_get_top_level_formula(Category,CatText,Labels,Values) :- | |
1602 | current_state_id(StateId), | |
1603 | bv_get_top_level_formula(Category,CatText,StateId,Labels,Values). | |
1604 | bv_get_top_level_formula(Category,CatText,StateId,Labels,Values) :- | |
1605 | bv_get_top_level(TL), | |
1606 | member(Category,TL), | |
1607 | bv_expand_formula(Category,CatText,Subs), | |
1608 | maplist(get_node_label,Subs,Labels), | |
1609 | bv_get_values(Subs,StateId,Values). | |
1610 | ||
1611 | % ------------------------------------ | |
1612 | ||
1613 | % provide HTML output of operation guards upto MaxLevel | |
1614 | % TO DO: provide option to provide parameter values, output to Latex,... | |
1615 | html_debug_operation_for_stateid(Stream,OpName,StateId,MaxLevel) :- | |
1616 | stored_formula(Id,guard(OpName,_,_)), | |
1617 | enter_level(Stream,0), | |
1618 | traverse(Stream,StateId,0,MaxLevel,Id), | |
1619 | exit_level(Stream,0). | |
1620 | ||
1621 | :- use_module(probsrc(tools),[html_escape/2]). | |
1622 | traverse(_,_StateId,Level,MaxLevel,_Id) :- Level>MaxLevel,!. | |
1623 | traverse(Stream,StateId,Level,MaxLevel,Id) :- | |
1624 | bv_expand_formula(Id,Label,Children), html_escape(Label,ELabel), | |
1625 | bv_get_values([Id],StateId,[Value]), | |
1626 | translate_value(Value,ValueS), html_escape(ValueS,EValueS), | |
1627 | % format('~w : ~w = ~w [~w] (level ~w)~n',[Id,Label,Value,ValueS,Level]), | |
1628 | stored_formula(Id,Formula), | |
1629 | (color_based_on_value(Value,Col) -> format(Stream,'<font color="~w">',[Col]) ; true), | |
1630 | (Formula = guard(_,_,_) | |
1631 | -> format(Stream,'<li>Guard of ~w = ~w</li>~n',[ELabel,EValueS]) | |
1632 | ; format(Stream,'<li>~w = ~w</li>~n',[ELabel,EValueS]) | |
1633 | ), | |
1634 | (color_based_on_value(Value,_) -> format(Stream,'</font>',[]) ; true), | |
1635 | (Level < MaxLevel | |
1636 | -> L1 is Level+1, | |
1637 | enter_level(Stream,L1), | |
1638 | maplist(traverse(Stream,StateId,L1,MaxLevel),Children), | |
1639 | exit_level(Stream,L1) | |
1640 | ; true). | |
1641 | ||
1642 | color_based_on_value(p(false),'INDIANRED'). | |
1643 | color_based_on_value(p(true),'DARKGREEN'). | |
1644 | color_based_on_value(e(_),red). | |
1645 | color_based_on_value(i,gray). | |
1646 | color_based_on_value(bv_info(_),gray). | |
1647 | ||
1648 | enter_level(Stream,L1) :- indent_ws(Stream,L1), format(Stream,'<ul>~n',[]). | |
1649 | exit_level(Stream,L1) :- indent_ws(Stream,L1), format(Stream,'</ul>~n',[]). | |
1650 | ||
1651 | indent_ws(_,X) :- X<1,!. | |
1652 | indent_ws(Stream,X) :- write(Stream,' '), X1 is X-1, indent_ws(Stream,X1). | |
1653 | ||
1654 | ||
1655 | translate_value(p(V),R) :- !,R=V. | |
1656 | translate_value(v(V),R) :- R=V. | |
1657 | translate_value(e(M),R) :- !, ajoin(['ERROR(',M,')'],R). | |
1658 | translate_value(i,R) :- !, R='INACTIVE'. | |
1659 | translate_value(bv_info(I),R) :- !, R=I. | |
1660 | translate_value(V,V). | |
1661 | ||
1662 | % -------------------------------- | |
1663 | ||
1664 | :- use_module(probsrc(error_manager),[add_error/3]). | |
1665 | :- use_module(probsrc(bmachine),[b_parse_machine_predicate_from_codes_open/5, b_parse_machine_formula_from_codes/7]). | |
1666 | tcltk_register_new_user_formula(F) :- tcltk_register_new_user_formula(formula,F). | |
1667 | tcltk_register_new_user_formula(Kind,F) :- | |
1668 | atom_codes(F,Codes), | |
1669 | TypingScope=[prob_ids(visible),variables], | |
1670 | (Kind=open_predicate | |
1671 | -> b_parse_machine_predicate_from_codes_open(exists,Codes,[],TypingScope,Typed) | |
1672 | ; b_parse_machine_formula_from_codes(Kind,Codes,TypingScope,Typed,_Type,true,Error) | |
1673 | ), | |
1674 | (Error=none -> true | |
1675 | ; add_error(tcltk_register_new_user_formula,'Error occured while parsing formula: ',Error),fail), | |
1676 | bv_insert_formula(Typed,user_formulas,_), | |
1677 | (top_level_node(user_formulas) -> true ; register_top_level(user_formulas) ). | |
1678 | %retractall(expanded(user_formulas)), | |
1679 | %bv_insert_formula(Typed,user,_),. | |
1680 | ||
1681 | % -------------------------------- | |
1682 | ||
1683 |