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