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