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