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),!. |