1		% (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(xtl_interface, [open_xtl_file/1,
6		xtl_transition/3, xtl_transition/4,
7		xtl_transition_with_symbolic/3,
8		xtl_symbolic_transition_potentially_enabled/2,
9		xtl_transition_parameters/2, get_xtl_paras_as_identifiers/2,
10		xtl_property/2, xtl_invariant_violated/1,
11		xtl_nr_state_properties/1,
12		xtl_goal_found/1,
13		xtl_animation_function_result/2, xtl_animation_image/2,
14		xtl_heuristic_function_active/0,
15		xtl_heuristic_function_result/2,
16		xtl_animation_image_click_transition/6,
17		xtl_animation_image_right_click_transition/4,
18		xtl_get_definition_string/2,
19		xtl_game_info/3,
20
21		xtl_search_scope/1, xtl_set_search_scope/1,
22		xtl_main_file_name/1,
23
24		csp_initialisation_for_b/1,
25		csp_transition_for_b/5,
26		generate_b_operationargs_from_csp/2,
27
28		%open_promela_file/1, promela_transition/3, promela_property/2,
29		%open_smv_file/1, smv_transition/3, smv_property/2, % SMV mode broken
30
31		open_cspm_file/1, last_opened_cspm_file/1,
32		cspm_transition/3,
33		cspm_property/2,
34		set_cspm_main_process/1,
35
36		get_disprover_po/6,
37		reset_xtl_interface/0]).
38
39
40		:- use_module(module_information).
41		:- module_info(group,animator).
42		:- module_info(description,'Provides an interface to the non-B animators depending on animation-mode.').
43
44		/* Typically the XTL specifications reside in a .P file with the following predicates
45		start/1 -> defining the initial states
46		trans/3 -> defining the transitions between states transition(Action, StateBefore, StateAfter)
47		prop/2 -> defining properties of states
48
49		start/2, trans/4: same as start/1 and trans/3, but last argument allows to provide a list of
50		additional transition infos (stored in state_space), e.g. [description('Desc')]
51
52		For CSP specifications the interpreter is integrated into ProB
53
54		*/
55
56		/* --------------- XTL ----------------- */
57		:- volatile prop/2, trans/3, trans/4, trans_prop/2, start/1, start/2, symb_trans/3, symb_trans_enabled/2.
58		:- volatile nr_state_properties/1, animation_function_result/2, animation_image/2.
59		:- volatile animation_image_click_transition/6, animation_image_right_click_transition/3.
60		:- volatile animation_image_right_click_transition/4.
61		:- volatile heuristic_function_active/0, heuristic_function_result/2.
62		:- volatile prob_pragma_string/2, prob_game_info/3.
63		:- volatile xtl_search_scope/1, xtl_main_file_name/1.
64		:- volatile disprover_po/6.
65		:- dynamic prop/2.
66		:- dynamic trans/3, trans/4.
67		:- dynamic trans_prop/2.
68		:- dynamic symb_trans/3, symb_trans_enabled/2.
69		:- dynamic start/1, start/2.
70		:- dynamic nr_state_properties/1.
71		:- dynamic animation_function_result/2.
72		:- dynamic animation_image/2.
73		:- dynamic animation_image_click_transition/6, animation_image_right_click_transition/3.
74		:- dynamic animation_image_right_click_transition/4.
75		:- dynamic heuristic_function_active/0.
76		:- dynamic heuristic_function_result/2.
77		:- dynamic prob_pragma_string/2, prob_game_info/3.
78		:- dynamic xtl_search_scope/1, xtl_main_file_name/1.
79		:- dynamic disprover_po/6.
80
81
82		% the following imports are required so that XTL .P files can make use of these functions:
83		:- use_module(library(lists)).
84		:- use_module(library(between)).
85		:- use_module(library(ordsets)).
86		:- use_module(library(samsort)).
87		:- use_module(library(random)).
88		:- use_module(library(avl)).
89		:- use_module(library(heaps)).
90		:- use_module(tools_portability, [exists_source/1]).
91		:- if(exists_source(library(logarr))).
92		:- use_module(library(logarr)). % not yet available in SWI Prolog
93		:- endif.
94
95		% ProB utilities (which can also be used by XTL code)
96		:- use_module(error_manager).
97		:- use_module(preferences,[get_preference/2]).
98		:- use_module(debug).
99		:- use_module(tools).
100
101		:- if(\+ current_prolog_flag(dialect, sicstus)).
102		abolish_all([]).
103		abolish_all([Pred|Preds]) :-
104		abolish(Pred),
105		abolish_all(Preds).
106		:- else.
107		abolish_all(Preds) :-
108		abolish(Preds, [force(true),tree(true)]).
109		:- endif.
110
111		open_xtl_file(File) :-
112		abolish_all([prop/2, trans/3, trans/4, trans_prop/2, symb_trans/3, symb_trans_enabled/2, start/1, start/2, nr_state_properties/1]),
113		abolish_all([animation_image/2,animation_function_result/2,
114		animation_image_click_transition/6,animation_image_right_click_transition/3,
115		animation_image_right_click_transition/4,
116		heuristic_function_active/0,
117		prob_pragma_string/2,
118		prob_game_info/3]),
119		abolish_all([xtl_search_scope/1, xtl_main_file_name/1]),
120		abolish_all([disprover_po/6]),
121		assertz((prop(_,_) :- fail)),
122		assertz((trans(_,_,_) :- fail)),
123		assertz((trans(_,_,_,_) :- fail)),
124		assertz((trans_prop(_,_) :- fail)),
125		assertz((symb_trans(_,_,_) :- fail)),
126		assertz((symb_trans_enabled(_,_) :- fail)),
127		assertz((start(_) :- fail)),
128		assertz((start(_,_) :- fail)),
129		assertz((nr_state_properties(_) :- fail)),
130		assertz((heuristic_function_active :- fail)),
131		assertz((animation_image(_,_) :- fail)),
132		assertz((animation_function_result(_,_) :- fail)),
133		assertz((animation_image_click_transition(_,_,_,_,_,_) :- fail)),
134		assertz((animation_image_right_click_transition(_,_,_) :- fail)),
135		assertz((animation_image_right_click_transition(_,_,_,_) :- fail)),
136		assertz((prob_pragma_string(_,_) :- fail)),
137		assertz((prob_game_info(_,_,_) :- fail)),
138		assertz((xtl_search_scope(_) :- fail)),
139		assertz(xtl_main_file_name(File)),
140		assertz((disprover_po(_,_,_,_,_,_) :- fail)), % to detect sequent_prover mode
141
142		debug_println(9,tcltk_open_xtl_file(File)),
143		consult_without_redefine_warning(File),
144		check_is_po_file(File),
145		debug_println(9,new_xtl_file(File)),
146		(xtl_get_definition_string('SCOPE',ScopePredStr) -> xtl_set_search_scope(ScopePredStr) ; true).
147
148		xtl_transition(State,Operation,NewState) :-
149	?	xtl_transition(State,Operation,NewState,_).
150		xtl_transition(State,Operation,NewState,Infos) :-
151		(get_preference(xtl_safe_mode, true)
152		-> xtl_transition_safe(State,Operation,NewState,Infos)
153	?	; xtl_transition_unsafe(State,Operation,NewState,Infos)).
154	?	xtl_transition_unsafe(root,start_xtl_system,NewState,Infos) :- get_start(NewState,Infos).
155		xtl_transition_unsafe(State,Operation,NewState,Infos) :-
156	?	State \= root, get_trans(Operation,State,NewState,Infos).
157		xtl_transition_safe(State,Operation,NewState,Infos) :-
158		(ground(State) -> true ; add_error(xtl,'Non-ground XTL state:',State),fail),
159		(State=root
160		-> Operation=start_xtl_system, get_start(NewState,Infos)
161		; get_trans(Operation,State,NewState,Infos),
162		((atom(Operation) ; compound(Operation)) -> true ; add_error(xtl,'Illegal XTL operation:',Operation),fail),
163		(ground(Operation) -> true ; add_error(xtl,'Non-ground XTL operation:',Operation),fail)
164		),
165		(ground(NewState) -> true ; add_error(xtl,'Non-ground XTL destination state:',NewState), fail).
166
167		xtl_transition_with_symbolic(State,Operation,NewState) :-
168		ground(Operation),
169		symb_trans(Operation,State,NewState), !,
170		check_trans_params(Operation).
171		xtl_transition_with_symbolic(State,Operation,NewState) :-
172	?	xtl_transition(State,Operation,NewState).
173
174	?	get_start(State,[]) :- start(State).
175	?	get_start(State,Infos) :- start(State,Infos),
176		(is_list(Infos) -> true ; add_error(xtl,'Transition info is not a list:',Infos), fail).
177	?	get_start(_,_) :- \+ start(_), \+start(_,_), add_error(xtl,'No XTL start state defined'), fail.
178
179	?	get_trans(Operation,State,NewState,[]) :- trans(Operation,State,NewState), check_trans_params(Operation).
180	?	get_trans(Operation,State,NewState,Infos) :- trans(Operation,State,NewState,Infos),
181		(is_list(Infos) -> true ; add_error(xtl,'Transition info is not a list:',Infos), fail),
182		check_trans_params(Operation).
183
184		% check that number of specified parameters matches the arity of the transition term and
185		% that only one declaration of parameter names per name is provided
186	?	check_trans_params(_) :- \+ trans_prop(_,param_names(_)), !.
187		check_trans_params(OpTerm) :-
188		functor(OpTerm,Name,Ar),
189		(xtl_transition_parameters(Name,Paras)
190		-> length(Paras,NrP),
191		(Ar =:= NrP -> true ; add_error(xtl,'Number of specified parameter names does not match the arity of transition:',Name),fail)
192		; true). % no params
193
194		xtl_transition_parameters(TransName,ParaNames) :-
195		trans_prop(TransName,param_names(ParaNames)),
196		(trans_prop(TransName,param_names(P2)), P2\=ParaNames
197		-> add_error(xtl,'Multiple parameter declarations for transition name:',TransName), fail
198		; true).
199
200		get_xtl_paras_as_identifiers(OpName,ParaIds) :-
201		xtl_transition_parameters(OpName,ParaNames), !,
202		findall(b(identifier(Name),string,[]), member(Name,ParaNames), ParaIds).
203		get_xtl_paras_as_identifiers(_,[]).
204
205		xtl_symbolic_transition_potentially_enabled(TransName,State) :-
206		symb_trans_enabled(TransName,State).
207
208		xtl_property(State,Property) :-
209	?	(get_preference(xtl_safe_mode, true) -> xtl_property_safe(State,Property) ; xtl_property_unsafe(State,Property)).
210		xtl_property_unsafe(State,Property) :-
211	?	State \= root, get_prop(State,Property).
212		xtl_property_safe(State,Property) :-
213		State \= root,
214		get_prop(State,Property),
215		(ground(Property)-> true ; add_error(xtl,'Non-ground XTL property:',Property), fail).
216
217	?	get_prop(State,Property) :- if(prop(State,Property), true, Property='No XTL properties defined').
218
219		% special Property is unsafe; see is_xtl_error_state in model_checker.pl
220		% Note for XTL we do not use not_invariant_checked/1 facts
221		xtl_invariant_violated(State) :- xtl_property(State,unsafe).
222		xtl_goal_found(State) :- xtl_property(State,goal).
223
224		xtl_nr_state_properties(Nr) :- nr_state_properties(Nr).
225
226		xtl_animation_function_result(State,AnimationMatrix) :- State \= root,
227		animation_function_result(State,AnimationMatrix).
228
229		xtl_animation_image(Nr,PathToGif) :-
230		%on_exception(error(existence_error(_,_),_),
231		animation_image(Nr,PathToGif).
232
233		% return a transition template to execute for simple clicks (From=To) or drags
234		% OperationTemplate can either be the template of an operation to match or a list of such templates
235		% (the operations will then be executed in order)
236		xtl_animation_image_click_transition(FromX,FromY,ToX,ToY,OperationTemplate,Image) :-
237		animation_image_click_transition(FromX,FromY,ToX,ToY,OperationTemplate,Image).
238
239		xtl_animation_image_right_click_transition(X,Y,OperationTemplate,State) :-
240		animation_image_right_click_transition(X,Y,OperationTemplate,State).
241		xtl_animation_image_right_click_transition(X,Y,OperationTemplate,_) :-
242		animation_image_right_click_transition(X,Y,OperationTemplate).
243
244		xtl_heuristic_function_active :-
245		heuristic_function_active.
246		xtl_heuristic_function_result(State,int(IntegerVal)) :- State \= root,
247		heuristic_function_result(State,Res),
248		(Res=int(R) -> IntegerVal=R
249		; number(Res) -> IntegerVal=Res
250		; add_error(xtl_heuristic_function_result,'heuristic_function_result must be integer: ',Res),fail
251		).
252
253		xtl_game_info(Key,State,Value) :- prob_game_info(Key,State,Value).
254		%xtl_game_over(State) :- prob_game_info('GAME_OVER',State,true).
255		%xtl_game_value(State,Value) :- prob_game_info('GAME_VALUE',State,Value).
256		%xtl_game_player(State,Player) :- prob_game_info('GAME_PLAYER',State,Player).
257
258
259		% way to mimic DEFINITION Strings in XTL mode, such as ASSERT_LTL
260		xtl_get_definition_string(Def_Name,DefString) :-
261	?	prob_pragma_string(N,S),
262		get_atom_string(N,Def_Name),
263		get_atom_string(S,DefString).
264
265		:- use_module(tools,[safe_atom_codes/2]).
266		get_atom_string(Atom,Res) :- atom(Atom),!,Res=Atom.
267		get_atom_string([H|T],Res) :- safe_atom_codes(Atom,[H|T]), !, Res=Atom. % transform "abc" into 'abc'
268		get_atom_string(R,R).
269
270		% set search_scope, restricting model checking to states which satisfy the SCOPE DEFINITION predicate
271		xtl_set_search_scope(Goal) :-
272		(predicate_property(xtl_search_scope(_),dynamic) % can be static if it is defined by the XTL spec
273		-> bmachine:b_parse_machine_predicate(Goal,[prob_ids(visible),variables,external_library(all_available_libraries)],TypedPred),
274		retractall(xtl_search_scope(_)),
275		assertz(xtl_search_scope(TypedPred))
276		; add_warning(xtl_set_search_scope,'Failed to set XTL search scope (xtl_search_scope is already defined): ',Goal)).
277
278		consult_without_redefine_warning(File) :-
279		get_set_optional_prolog_flag(redefine_warnings, Old, off),
280		get_set_optional_prolog_flag(single_var_warnings, Old2, off),
281		(catch(my_compile(File),
282		error(existence_error(_,_),_),
283		add_error_fail(xtl,'XTL File does not exist:',File))
284		-> OK=true ; OK=false),
285		get_set_optional_prolog_flag(redefine_warnings, _, Old),
286		get_set_optional_prolog_flag(single_var_warnings, _, Old2),
287		OK=true.
288
289		my_compile(F) :- %get_preference(user_is_an_expert_with_accessto_source_distribution,true),
290		!, % it seems it is ok to call compile also in probcli binary; it may do consult though
291		compile(F).
292		my_compile(F) :- consult(F).
293
294		:- use_module(seqproversrc(sequent_prover),[initialise_for_po_file/1]).
295		check_is_po_file(File) :-
296	?	disprover_po(_,_,_,_,_,_), !, % proof obligation facts generated by the ProB disprover: disprover_po/6
297		specfile:set_animation_minor_mode(sequent_prover),
298		initialise_for_po_file(File).
299		check_is_po_file(_).
300
301		% see disprover_test_runner [load_po_file/1,get_disprover_po/6]
302		get_disprover_po(FName,Context,Goal,All,Sel,Status) :-
303	?	xtl_interface:disprover_po(Name,Context,Goal,All,Sel,Status),
304		fix_rodin_name(Name,FName).
305		linefeed(10).
306		linefeed(13).
307		% sometimes Rodin POs have a newline before the slash; we remove this (see e.g., test 2023)
308		fix_rodin_name(POName,FixedName) :- atom_codes(POName,Cs),
309		exclude(linefeed,Cs,NewCs),
310		atom_codes(FixedName,NewCs).
311
312		/* --------------- Promela ----------------- */
313
314		%:- use_module('promela/h_int').
315
316		/* --------------- SMV ----------------- */
317
318		% :- use_module('smv/smv_trans').
319
320
321		/* --------------- CSP-M ----------------- */
322
323		:- use_module(probcspsrc(haskell_csp),[parse_and_load_cspm_file/1,
324		cspm_trans_enum/3,
325		animatable_process/1, animatable_process_without_arguments/1,
326		get_symbol_span/2,force_evaluate_argument/2,normalise_cspm_state/2]).
327		:- use_module(probcspsrc(haskell_csp_analyzer),[cspPrintCompiled/2]).
328		:- use_module(probsrc(translate),[translate_cspm_state/2]).
329
330		:- dynamic last_opened_cspm_file/1. % useful for csp_and_b mode
331
332		open_cspm_file(File) :-
333		retractall(last_opened_cspm_file(_)),
334		debug_println(15,open_cspm_file(File)), flush_output(user_output),
335		parse_and_load_cspm_file(File),
336		assertz(last_opened_cspm_file(File)).
337
338		:- dynamic cspm_main_process/1.
339		cspm_main_process('MAIN').
340		set_cspm_main_process(M) :-
341		retractall(cspm_main_process(_)),
342		assertz(cspm_main_process(M)).
343
344		reset_xtl_interface :- retractall(last_opened_cspm_file(_)),
345		reset_cspm_main_process.
346		reset_cspm_main_process :- set_cspm_main_process('MAIN').
347
348		:- use_module(eventhandling,[register_event_listener/3]).
349		:- register_event_listener(clear_specification,reset_xtl_interface,
350		'Reset XTL Interface.').
351
352		cspm_transition(root,start_cspm_MAIN,NormalisedNewState) :-
353		cspm_main_process(MAIN),
354	?	animatable_process_without_arguments(MAIN),
355		get_start_expr(MAIN,NewState),
356	?	normalise_cspm_state(NewState,NormalisedNewState).
357		cspm_transition(root,start_cspm(X),NormalisedNewState) :- cspm_main_process(MAIN),
358		(get_preference(cspm_animate_all_processes_without_arguments,true)
359	?	; \+ animatable_process_without_arguments(MAIN)),
360	?	animatable_process_without_arguments(X),
361		X\=MAIN,
362		get_start_expr(X,NewState),
363	?	normalise_cspm_state(NewState,NormalisedNewState).
364		cspm_transition(root,start_cspm(X),NormalisedNewState) :- cspm_main_process(MAIN),
365		get_preference(cspm_animate_all_processes,true),
366		animatable_process(X),
367		X\=MAIN,
368		get_start_expr(X,NewState),
369		normalise_cspm_state(NewState,NormalisedNewState).
370		cspm_transition(root,io([V1],print,no_loc_info_available),root) :-
371	?	cspPrintCompiled(Expr,CompiledExpr), debug_println(9,cspPrintCompiled(Expr,CompiledExpr)),
372		nl, translate:print_csp_value(Expr),
373		print(' == '), nl, print(' '),
374	?	force_evaluate_argument(CompiledExpr,V1),
375		translate:print_csp_value(V1),nl.
376		cspm_transition(root,no_process_to_animate,root) :-
377		( get_preference(cspm_animate_all_processes,true) ->
378		\+ animatable_process(_)
379	?	; \+ animatable_process_without_arguments(_)).
380		cspm_transition(State,Action,NormalisedNewState) :- State \= root,
381		%print(comp),nl,
382	?	cspm_trans_enum(State,Action,NewState),
383	?	normalise_cspm_state(NewState,NormalisedNewState).
384		%(ActionS = io(V,Ch,_Span) -> Action = io(V,Ch) ; Action=ActionS).
385		%print(new(NewState)),nl. /* TO DO: Normalise */
386
387		cspm_property(State,Property) :-
388		translate_cspm_state(State,Property).
389
390		/* --------------- CSP ----------------- */
391
392
393		get_start_expr(Proc,val_of(Proc,Span)) :- get_symbol_span(Proc,Span).
394
395
396
397		csp_initialisation_for_b(NewState) :- cspm_main_process(MAIN),
398	?	(animatable_process_without_arguments(MAIN) -> get_start_expr(MAIN,NewState);
399		(animatable_process_without_arguments(X)
400		-> add_error(csp_transition_for_b,'No MAIN process in the CSP file! I am animating:',X),
401		NewState = val_of(X)
402		; add_error(csp_transition_for_b,'No animatable process in the CSP file!'), NewState = stop)
403		).
404
405		csp_transition_for_b(State,Ch,Args,Action,NewState) :- State \= root,
406		% print(cspm_trans_enum(State,Action,NewState)),nl,
407	?	cspm_trans_enum(State,Action,NewState), %% TO DO: delay enumeration until B operation has been setup ?
408		% print(cspm_trans_enum(Action,NewState)),nl,
409		decompose_event(Action,Ch,Args).
410		% print(b(Ch,BArgs)),nl.
411
412
413		/* needed: an any operation: map any operation<------------- */
414
415		decompose_event(io(V,Ch,_Src),Ch,V).
416		decompose_event(tau(S),tau(S),[]).
417		%% decompose_event(i(S),i(S),[]). %% deprecated
418		decompose_event(tick(S),tick(S),[]).
419
420		generate_b_operationargs_from_csp(V,BArgs) :- l_copy_args_to_b(V,BArgs).
421
422
423		l_copy_args_to_b(tail_in(X),[Y]) :- translate_and_normalise_arg_to_b(X,Y).
424		l_copy_args_to_b([],[]).
425		l_copy_args_to_b([HCSP|T],[HB|TB]) :-
426		copy_args_to_b(HCSP,HB),
427		l_copy_args_to_b(T,TB).
428
429		copy_args_to_b(dot(X),Y) :- !,translate_and_normalise_arg_to_b(X,Y). /* is this still required with the new eval ?? */
430		copy_args_to_b(in(X),Y) :- !,translate_and_normalise_arg_to_b(X,Y).
431		copy_args_to_b(out(X),Y) :- !,translate_and_normalise_arg_to_b(X,Y).
432		copy_args_to_b(X,Y) :- translate_and_normalise_arg_to_b(X,Y).
433
434		:- use_module(store,[normalise_value_for_var/4]).
435
436		translate_and_normalise_arg_to_b(CSP,BN) :- translate_arg_to_b(CSP,B), normalise_value_for_var(csp,true,B,BN).
437
438		:- use_module(tools,[print_message/1, convert_list_into_pairs/2]).
439		:- use_module(custom_explicit_sets,[construct_avl_from_lists/2]).
440
441		%translate_arg_to_b(X,Y) :- print(translate_arg_to_b(X,Y)),nl,fail.
442		translate_arg_to_b(X,X) :- var(X),!.
443		translate_arg_to_b(X,int(X)) :- number(X),!,print_message(converted_int(X)).
444		translate_arg_to_b(fd(N,S),fd(N,S)) :- !. /* copy B SET element across */
445		translate_arg_to_b(string(S),string(S)) :- !. /* copy B STRING element across */
446		translate_arg_to_b(int(N),int(N)) :- !.
447		translate_arg_to_b(true,pred_true /* bool_true */) :- !.
448		translate_arg_to_b(false,pred_false /* bool_false */) :- !.
449		translate_arg_to_b(global_set(N),global_set(N)) :- !.
450		translate_arg_to_b(freetype(N),freetype(N)) :- !.
451		translate_arg_to_b(avl_set(N),avl_set(N)) :- !.
452		translate_arg_to_b(closure(A,B,C),closure(A,B,C)) :- !.
453		translate_arg_to_b(closure(A,B,C,E),closure(A,B,C,E)) :- !.
454		translate_arg_to_b(setValue(S),R) :- !, translate_arg_to_b(S,R1),
455		construct_avl_from_lists(R1,R).
456		%sort(R1,R). % IS SORTING NECESSARY?; we could translate to AVL
457		translate_arg_to_b(list(L),R) :- !, translate_list_to_b(L,1,R1),
458		custom_explicit_sets:construct_avl_from_lists(R1,R).
459		translate_arg_to_b([],[]) :- !.
460		translate_arg_to_b([H|T],[TH|TT]) :- !,translate_arg_to_b(H,TH), translate_arg_to_b(T,TT).
461		translate_arg_to_b((H,T),(TH,TT)) :- !,translate_arg_to_b(H,TH), translate_arg_to_b(T,TT).
462		translate_arg_to_b(na_tuple(L),Res) :- !,l_translate_arg_to_b(L,TL),
463		convert_list_into_pairs(TL,Res).
464		translate_arg_to_b(Constant,BRep) :- translate_b_constant(Constant,BRep),!. /* clause necessary?? */
465		translate_arg_to_b(term(Constant),BRep) :- translate_b_constant(Constant,BRep),!.
466		% TO DO: treat floats/reals
467		translate_arg_to_b(term(N),term(N)) :- !.
468		translate_arg_to_b(DeferredSetEl,FD) :-
469		is_deferred_set_element_name(DeferredSetEl,FD),!.
470		translate_arg_to_b(X,string(X)) :- atomic(X),!. % if the identfier X is not known: translate it to a string
471		% TO DO: some static checking: if no operation has a STRING parameter type, then we can skip this clause and generate an error message straightaway
472		translate_arg_to_b(X,term(X)) :- add_error(translate_arg_to_b,'Unknown CSP datatype, cannot convert to B:',X).
473		/* extend for other types */
474
475		translate_list_to_b([],_,[]).
476		translate_list_to_b([H|T],Nr,[(int(Nr),TH)|TT]) :- translate_arg_to_b(H,TH),
477		N1 is Nr+1, translate_list_to_b(T,N1,TT).
478
479		l_translate_arg_to_b([],[]).
480		l_translate_arg_to_b([H|T],[TH|TT]) :- translate_arg_to_b(H,TH),
481		l_translate_arg_to_b(T,TT).
482
483		:- use_module(tools,[safe_atom_codes/2]).
484		:- use_module(self_check).
485		:- assert_must_succeed( (xtl_interface:is_deferred_set_element_name('Code1',R),R=fd(1,'Code')) ).
486		:- assert_must_fail( xtl_interface:is_deferred_set_element_name('CodeXX',_R) ).
487		is_deferred_set_element_name(DeferredSetEl,fd(Nr,Set)) :- atomic(DeferredSetEl),
488	?	b_global_sets:b_global_deferred_set(Set), atom_codes(Set,SetCodes),
489		append(SetCodes,NrCodes,DC),
490		safe_atom_codes(DeferredSetEl,DC),
491		catch(number_codes(Nr,NrCodes),_,fail).
492
493		:- use_module(b_global_sets,[b_global_set/1, all_elements_of_type/2]).
494
495		translate_b_constant(GS,BRep) :- nonvar(GS),b_global_set(GS),all_elements_of_type(GS,BRep),!.
496		translate_b_constant(Constant,BRep) :- nonvar(Constant),b_global_sets:lookup_global_constant(Constant,BRep),!.