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