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