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