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