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