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