| 1 | % (c) 2009-2014 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 | ||
| 6 | :- module(fdr_csp_generator, [tcltk_print_states_for_fdr/1,tcltk_print_states_for_spin/1]). | |
| 7 | ||
| 8 | :- use_module(module_information,[module_info/2]). | |
| 9 | :- module_info(group,tools). | |
| 10 | :- module_info(description,'Tools for exporting state space in CSP or Promela format.'). | |
| 11 | ||
| 12 | :- use_module(gensym). | |
| 13 | :- use_module(library(lists)). | |
| 14 | ||
| 15 | :- dynamic channel/4. | |
| 16 | :- dynamic selectsymbol/0. | |
| 17 | :- dynamic commasymbol/0. | |
| 18 | :- dynamic written_channel/1. | |
| 19 | ||
| 20 | ||
| 21 | ||
| 22 | :- use_module(specfile,[animation_mode/1, currently_opened_file/1,csp_with_bz_mode/0]). | |
| 23 | ||
| 24 | :- use_module(state_space). | |
| 25 | :- use_module(translate). | |
| 26 | :- use_module(debug,[time/1]). | |
| 27 | :- use_module(tools,[print_message/1, ajoin/2]). | |
| 28 | ||
| 29 | ||
| 30 | tcltk_print_states_for_fdr(F) :- | |
| 31 | time(fdr_csp_generator:tcltk_print_states_for_fdr2(F)). | |
| 32 | tcltk_print_states_for_fdr2(F) :- | |
| 33 | print_message('Saving State Space to FDR/CSP File: '), print_message(F), | |
| 34 | tell(F),(convert_b_2_csp -> true ; true),told, | |
| 35 | print_message('Finished'). | |
| 36 | tcltk_print_states_for_spin(F) :- | |
| 37 | print_message('Saving State Space to SPIN/Promela File: '), print_message(F), | |
| 38 | tell(F),(convert_b_2_promela -> true ; true),told, | |
| 39 | print_message('Finished'). | |
| 40 | ||
| 41 | ||
| 42 | ||
| 43 | /* ------------- */ | |
| 44 | ||
| 45 | transition_for_fdr(FromID,Trans,ToID) :- transition(FromID,Trans,ToID), | |
| 46 | \+ to_be_ignored(Trans). | |
| 47 | ||
| 48 | to_be_ignored(io([_V1],print,_)). % comes from cspPrint | |
| 49 | ||
| 50 | /* ------------- */ | |
| 51 | ||
| 52 | convert_b_2_csp :- | |
| 53 | retractall(current_mode(_)), assert(current_mode(fdr)), | |
| 54 | convert. | |
| 55 | convert_b_2_promela :- | |
| 56 | retractall(current_mode(_)), assert(current_mode(spin)), | |
| 57 | convert. | |
| 58 | ||
| 59 | convert :- | |
| 60 | print_overall_header, | |
| 61 | (current_mode(fdr) -> true /* no need to print channels */ ; print_channels), | |
| 62 | gen_process. | |
| 63 | ||
| 64 | gen_tran:- | |
| 65 | transition_for_fdr(StateID,TransAsTerm,TID), | |
| 66 | (channel(TransAsTerm,_,StateID,_) -> fail | |
| 67 | ; (translate_event(TransAsTerm,Trans), | |
| 68 | generate_transition_id(TransAsTerm,Trans,FDRTransID), | |
| 69 | assert(channel(TransAsTerm,FDRTransID,StateID,TID)) | |
| 70 | ) | |
| 71 | ),fail. | |
| 72 | gen_tran. | |
| 73 | ||
| 74 | generate_transition_id(TransAsTerm,_,TransID) :- | |
| 75 | var(TransAsTerm),!,TransID = error_trans_is_var. | |
| 76 | generate_transition_id(TransAsTerm,_,TransID) :- atomic(TransAsTerm),!,TransID = TransAsTerm. | |
| 77 | generate_transition_id(TransAsTerm,Transs,TransID) :- | |
| 78 | functor(TransAsTerm,Func,_), | |
| 79 | (Func = ('-->') | |
| 80 | -> arg(1,TransAsTerm,Arg), generate_transition_id(Arg,Transs,TransID) | |
| 81 | ; ((Func = '$initialise_machine' ; Func = '$setup_constants') | |
| 82 | -> TransID = Func | |
| 83 | ; Transs = TransID %char_translate(Transs,TransID) | |
| 84 | ) | |
| 85 | ). | |
| 86 | ||
| 87 | ||
| 88 | %char_translate(Sf,ResultS) :- | |
| 89 | % name(Sf, Sflist), | |
| 90 | % mysubstitute(123,Sflist,40,SflistR), /* { -> ( */ | |
| 91 | % mysubstitute(125,SflistR,41,SflistRR), /* } -> ) */ | |
| 92 | % %mysubstitute(40,SflistRR,95,SflistRRR), | |
| 93 | % %mysubstitute(41,SflistRRR,95,SflistRRRR), | |
| 94 | % %%mysubstitute(44,SflistRR,95,SflistRRRRR), | |
| 95 | % name(ResultS,SflistRR). | |
| 96 | % | |
| 97 | % | |
| 98 | %mysubstitute(X,L,Y,Res) :- sub(L,X,Y,Res). /* for Sicstus 4 */ | |
| 99 | %sub([],_,_,[]). | |
| 100 | %sub([H|T],X,Y,[SH|ST]) :- | |
| 101 | % (H=X -> SH=Y ; SH=H), | |
| 102 | % sub(T,X,Y,ST). | |
| 103 | ||
| 104 | ||
| 105 | write_tran:- | |
| 106 | (animation_mode(cspm) -> print('-- ') ; true), /* Comment out if in CSP mode as original CSP will already define channels */ | |
| 107 | print_channel_keyword, | |
| 108 | channel(_,ID,_,_), | |
| 109 | (written_channel(ID) -> true ; ( | |
| 110 | assert(written_channel(ID)), | |
| 111 | print_comma, | |
| 112 | print(ID))), | |
| 113 | fail. | |
| 114 | write_tran:- print_end_of_construct,nl. | |
| 115 | ||
| 116 | print_comma:- | |
| 117 | (commasymbol -> print(',') ; assert(commasymbol)). | |
| 118 | ||
| 119 | ||
| 120 | print_channels :- | |
| 121 | %time(fdr_csp_generator:gen_tran), | |
| 122 | gen_tran, | |
| 123 | retractall(commasymbol), | |
| 124 | retractall(written_channel(_)), | |
| 125 | write_tran,nl. | |
| 126 | ||
| 127 | gen_process :- print_transition_header,fail. | |
| 128 | gen_process :- | |
| 129 | visited_expression_id(NodeIDs), | |
| 130 | print_process_declaration_header(NodeIDs), | |
| 131 | retractall(selectsymbol), | |
| 132 | (transition_for_fdr(NodeIDs,_,_) -> process_detail(NodeIDs) | |
| 133 | ; (not_all_transitions_added(NodeIDs) | |
| 134 | -> print_open_detail(NodeIDs) ; print_stop_detail(NodeIDs)) | |
| 135 | ), | |
| 136 | print_process_declaration_footer(NodeIDs), fail. | |
| 137 | gen_process:- print_transition_footer. | |
| 138 | ||
| 139 | :- dynamic tau_found/0, non_tau_found/0. | |
| 140 | assert_tau_found_fail :- \+ tau_found, assert(tau_found), fail. | |
| 141 | %assert_non_tau_found :- non_tau_found -> true ; assert(non_tau_found). | |
| 142 | ||
| 143 | process_detail(Node1) :- | |
| 144 | retractall(tau_found), retractall(non_tau_found), | |
| 145 | %non_tau_transition_exists(Node1),!, | |
| 146 | process_non_tau_detail(Node1),!, | |
| 147 | (tau_found % tau_transition(Node1,_,_) | |
| 148 | -> ( print(' [> '), process_tau_instructions(Node1)) | |
| 149 | ; true), | |
| 150 | nl. | |
| 151 | process_detail(Node1) :- \+ non_tau_found, | |
| 152 | (tau_found % tau_transition(Node1,_,_) | |
| 153 | -> ( process_tau_instructions(Node1)) | |
| 154 | ; print(' STOP ') | |
| 155 | ), | |
| 156 | nl. | |
| 157 | ||
| 158 | process_non_tau_detail(Node1) :- | |
| 159 | transition_for_fdr(Node1,TransAsTerm,Node2), | |
| 160 | (is_tau(TransAsTerm) -> assert_tau_found_fail | |
| 161 | ; (non_tau_found -> true ; (print(' ( '),assert(non_tau_found) ))), | |
| 162 | print_detail(TransAsTerm,Node1,Node2),nl,fail. | |
| 163 | process_non_tau_detail(_) :- non_tau_found, | |
| 164 | (selectsymbol -> (print(' ) '),retract(selectsymbol)) ; print(' STOP ) ') ). | |
| 165 | ||
| 166 | %non_tau_transition_exists(Node1) :- | |
| 167 | % transition_for_fdr(Node1,TransAsTerm,_Node2),\+ is_tau(TransAsTerm). | |
| 168 | ||
| 169 | tau_transition(Node1,TransAsTerm,Node2) :- | |
| 170 | transition_for_fdr(Node1,TransAsTerm,Node2),is_tau(TransAsTerm). | |
| 171 | ||
| 172 | is_tau(tau(_)). | |
| 173 | is_tau(start_cspm_MAIN). | |
| 174 | ||
| 175 | process_tau_instructions(Node1) :- print(' ( '), | |
| 176 | tau_transition(Node1,Trans,Node2), | |
| 177 | print_tau_detail(Trans,Node2),nl,fail. | |
| 178 | process_tau_instructions(_) :- print(' ) '). | |
| 179 | ||
| 180 | ||
| 181 | print_detail(TransAsTerm,_Node1,Node2):- | |
| 182 | fdr_translate_event(TransAsTerm,TransAsString), | |
| 183 | (selectsymbol -> print(' [] '); (current_mode(fdr) -> assert(selectsymbol) ; true)), | |
| 184 | print_single_transition(TransAsString,Node2). | |
| 185 | ||
| 186 | print_tau_detail(Trans,Node2):- | |
| 187 | (selectsymbol -> print(' |~| '); (current_mode(fdr) -> assert(selectsymbol) ; true)), | |
| 188 | print_single_tau_transition(Trans,Node2). | |
| 189 | ||
| 190 | fdr_translate_event(Transition,String) :- | |
| 191 | csp_with_bz_mode,!, | |
| 192 | fdr_translate_event2(Transition,String). | |
| 193 | fdr_translate_event(Transition,String) :- | |
| 194 | translate_event(Transition,String). | |
| 195 | ||
| 196 | fdr_translate_event2(io(Values,Channel,_Span),String) :- !, | |
| 197 | translate_event(io(Values,Channel),String). % omit "CSP: ..." | |
| 198 | fdr_translate_event2('-->'(Operation,OutputValues),String) :- !, | |
| 199 | Operation =.. [Channel|InputValues], | |
| 200 | append(InputValues,OutputValues,Values), | |
| 201 | fdr_translate_operation(Channel,Values,String). | |
| 202 | fdr_translate_event2(Event,String) :- | |
| 203 | is_csp_event(Event),!,translate_event(Event,String). | |
| 204 | fdr_translate_event2(Operation,String) :- | |
| 205 | Operation =.. [Channel|Values], | |
| 206 | fdr_translate_operation(Channel,Values,String). | |
| 207 | ||
| 208 | fdr_translate_operation(Name,Values,String) :- | |
| 209 | maplist(translate_bvalue,Values,ValueStrings), | |
| 210 | inject_dots([Name|ValueStrings],Strings), | |
| 211 | ajoin(Strings,String). | |
| 212 | ||
| 213 | inject_dots([],[]). | |
| 214 | inject_dots([E],[E]) :- !. | |
| 215 | inject_dots([H|T],[H,'.'|NT]) :- | |
| 216 | inject_dots(T,NT). | |
| 217 | ||
| 218 | ||
| 219 | ||
| 220 | is_csp_event(start_cspm(_)). | |
| 221 | is_csp_event(tick(_)). | |
| 222 | is_csp_event(tau(_)). | |
| 223 | is_csp_event(io(_,_,_)). | |
| 224 | is_csp_event(io(_,_)). | |
| 225 | ||
| 226 | ||
| 227 | ||
| 228 | /* Language dependent stuff */ | |
| 229 | :- dynamic current_mode/1. | |
| 230 | ||
| 231 | current_mode(fdr). | |
| 232 | ||
| 233 | print_overall_header :- retractall(prob__open__node_generated), | |
| 234 | current_mode(fdr),!, | |
| 235 | print('-- ProB State Space Encoded for FDR in CSP'),nl, | |
| 236 | currently_opened_file(F), | |
| 237 | (animation_mode(cspm) -> (nl, print('include "'), | |
| 238 | print(F),print('"'),nl,nl, | |
| 239 | print('assert MAIN [FD= Nroot'),nl, | |
| 240 | print('assert Nroot [FD= MAIN'),nl,nl) | |
| 241 | ; (print('-- Original file: '), print(F)) | |
| 242 | ), | |
| 243 | print('--'),nl. | |
| 244 | print_overall_header :- print('/* ProB State Space Encoded for Spin in Promela */'),nl, | |
| 245 | currently_opened_file(F), | |
| 246 | print('/* Original file: '), print(F), print(' */'),nl. | |
| 247 | ||
| 248 | print_channel_keyword :- current_mode(fdr),!, | |
| 249 | print('channel '). | |
| 250 | print_channel_keyword :- print('chan '). | |
| 251 | ||
| 252 | print_end_of_construct :- current_mode(fdr),!,nl. | |
| 253 | print_end_of_construct :- print(';'),nl. | |
| 254 | ||
| 255 | print_transition_header :- current_mode(fdr),!,nl. | |
| 256 | print_transition_header :- nl, print('active proctype root()'),nl,print('{'),nl. | |
| 257 | ||
| 258 | :- dynamic prob__open__node_generated/0. | |
| 259 | print_transition_footer :- current_mode(fdr),!, | |
| 260 | (prob__open__node_generated | |
| 261 | -> (print_channel_keyword, print('prob__open__node'),print_end_of_construct | |
| 262 | ) | |
| 263 | ; true | |
| 264 | ), | |
| 265 | print('-- end of ProB Encoding'),nl. | |
| 266 | print_transition_footer :- print('}'),nl, print('/* end of ProB Encoding */'),nl. | |
| 267 | ||
| 268 | print_process_declaration_header(ID) :- current_mode(fdr),!, | |
| 269 | print('N'),print(ID), print(' = '). | |
| 270 | print_process_declaration_header(ID) :- | |
| 271 | print('N'),print(ID), print(':'),nl, | |
| 272 | print(' if'),nl. | |
| 273 | ||
| 274 | print_process_declaration_footer(_) :- current_mode(fdr),!,nl. | |
| 275 | print_process_declaration_footer(_) :- print(' fi;'),nl. | |
| 276 | ||
| 277 | ||
| 278 | print_single_transition(TransName,ToNodeID) :- current_mode(fdr),!, | |
| 279 | ((TransName = tick(_) ; TransName=tick) | |
| 280 | -> (print('SKIP {- N'),print(ToNodeID),print(' ( == STOP) -}')) | |
| 281 | ; ((TransName = i(_) ; TransName=i) | |
| 282 | -> (print('(STOP /\\ N'),print(ToNodeID), print(')') ) | |
| 283 | ; (print(TransName),print('->'),print('N'),print(ToNodeID)) | |
| 284 | ) | |
| 285 | ). | |
| 286 | print_single_transition(TransName,ToNodeID) :- !,print(' :: printf("'), | |
| 287 | print(TransName),print('\\n") -> goto '), print('N'),print(ToNodeID). | |
| 288 | print_single_transition(TransName,ToNodeID) :- print(' :: '), | |
| 289 | print(TransName),print('-> goto '), print('N'),print(ToNodeID). | |
| 290 | ||
| 291 | ||
| 292 | ||
| 293 | print_single_tau_transition(TransName,ToNodeID) :- current_mode(fdr),!, | |
| 294 | print(' {- '),print(TransName),print('->'), print(' -} N'),print(ToNodeID). | |
| 295 | print_single_tau_transition(TransName,ToNodeID) :- !,print(' :: printf("'), | |
| 296 | print(TransName),print('\\n") -> goto '), print('N'),print(ToNodeID). | |
| 297 | print_single_tau_transition(TransName,ToNodeID) :- print(' :: '), | |
| 298 | print(TransName),print('-> goto '), print('N'),print(ToNodeID). | |
| 299 | ||
| 300 | ||
| 301 | print_stop_detail(_) :- current_mode(fdr),!,print('STOP'),nl. | |
| 302 | print_stop_detail(NodeIDs) :- print_single_transition(prob__deadlock,NodeIDs). | |
| 303 | ||
| 304 | print_open_detail(_NodeIDs) :- current_mode(fdr),!,print('prob__open__node -> STOP'),nl, | |
| 305 | assert(prob__open__node_generated). | |
| 306 | print_open_detail(NodeIDs) :- print_single_transition(prob__open__node,NodeIDs). | |
| 307 | ||
| 308 | /* --------------------------- */ | |
| 309 |