/* translation */ system wand; type Character = range 1..256; Charstring = abstract implementation "geode predefined type" end; return_type = enum success,failed; susp_type = enum later,immediately; tip_type = enum start_tip,end_tip; ho_type = enum forward_ho,backward_ho; mac_ad_type = range 5 .. 5; ap_mac_addrtype = range 5 .. 5; channel_id_type = range 5 .. 5; mt_mac_addrtype = range 0 .. 5; signal measure_rlq_req_mtc(pid); measure_rlq_cnf_mtc(pid); init_mss(pid); close_mss(pid); get_target_ap(pid, ho_type); target_ap_found(pid, ap_mac_addrtype); suspend_mhi(pid); resume_mhi(pid); synchro_with(pid, ap_mac_addrtype); association_completed(pid); synchro_with_ack(pid, return_type); acquire_new_ap(pid, channel_id_type); acquire_new_ap_ok(pid); acquire_new_ap_ko(pid); neigh_ap_load_info_req(pid); neigh_ap_load_info_cnf(pid); resume_msc(pid); resume_msc_ok(pid); suspend_msc(pid, susp_type); suspend_msc_ok(pid); ap_lost(pid); mpdu_tip(pid, mac_ad_type, tip_type); mpdu_tip_ack(pid, mac_ad_type); mpdu_beacon(pid, ap_mac_addrtype); init_ho_seek_info(pid); stop_ho_seek_info(pid); init_ho_seek_info_ok(pid); init_ho_seek_info_ko(pid); init_mba(pid); close_mba(pid); init_mti(pid); close_mti(pid); init_mtc(pid); close_mtc(pid); send_neigh_ap_info(pid); buffer env : queue :toenv of *; q_msg_0 : queue of close_mss, init_mss; q_mba_0 : queue of mpdu_beacon, close_mba, init_mba; q_mti_0 : queue of mpdu_tip_ack, stop_ho_seek_info, init_ho_seek_info, close_mti, init_mti; q_mtc_0 : queue of neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, close_mtc, init_mtc; process msg_0 :buffer q_msg_0; var sender : pid; parent : pid; offspring : pid; state start :init; open_close; stop discard close_mss, init_mss in q_msg_0; end; transition from start :eager /* start */ to open_close; from open_close :eager input init_mss(sender) from q_msg_0 do output init_mba(msg_0) to q_mba_0 ,output init_mti(msg_0) to q_mti_0 ,output init_mtc(msg_0) to q_mtc_0 to open_close; from open_close :eager input close_mss(sender) from q_msg_0 do output close_mba(msg_0) to q_mba_0 ,output close_mti(msg_0) to q_mti_0 ,output close_mtc(msg_0) to q_mtc_0 /* stop */ to stop; process mba_0 :buffer q_mba_0; var sender : pid; parent : pid; offspring : pid; ap_mac_addr: ap_mac_addrtype; state start :init; wait_init discard mpdu_beacon, close_mba in q_mba_0; end; wait_network_info discard init_mba in q_mba_0; end; stop discard mpdu_beacon, close_mba, init_mba in q_mba_0; end; transition from start :eager /* start */ to wait_init; from wait_init :eager input init_mba(sender) from q_mba_0 to wait_network_info; from wait_network_info :eager input mpdu_beacon(sender, ap_mac_addr) from q_mba_0 /* Extract infos from the Beacon */ do output send_neigh_ap_info(mba_0) to q_mtc_0 to wait_network_info; from wait_network_info :eager input close_mba(sender) from q_mba_0 /* stop */ to stop; process mti_0 :buffer q_mti_0; var sender : pid; parent : pid; offspring : pid; t_tip_wait_ack : timer; retries: int; mt_mac_addr: mt_mac_addrtype; state start :init; wait_init discard mpdu_tip_ack, stop_ho_seek_info, init_ho_seek_info, close_mti in q_mti_0; end; mti_active discard mpdu_tip_ack, init_mti in q_mti_0; end; stop discard mpdu_tip_ack, stop_ho_seek_info, init_ho_seek_info, close_mti, init_mti in q_mti_0; end; wait_ap_answer discard stop_ho_seek_info, init_ho_seek_info, init_mti in q_mti_0; end; q14 :nostable; transition from start :eager /* start */ to wait_init; from wait_init :eager input init_mti(sender) from q_mti_0 to mti_active; from mti_active :eager input close_mti(sender) from q_mti_0 /* stop */ to stop; from mti_active :eager input init_ho_seek_info(sender) from q_mti_0 do retries := 1 ,output mpdu_tip(mti_0,mt_mac_addr, start_tip) to env ,set t_tip_wait_ack := (0 + 10) to wait_ap_answer; from wait_ap_answer :eager input mpdu_tip_ack(sender, any) from q_mti_0 do reset t_tip_wait_ack ,output init_ho_seek_info_ok(mti_0) to q_mtc_0 to mti_active; from wait_ap_answer :eager if (t_tip_wait_ack = 0) /* expire t_tip_wait_ack */ do reset t_tip_wait_ack to q14; from q14 :eager if (retries <= 5) = false do output init_ho_seek_info_ko(mti_0) to q_mtc_0 to mti_active; from q14 :eager if (retries <= 5) = true do output mpdu_tip(mti_0,mt_mac_addr, start_tip) to env ,set t_tip_wait_ack := (0 + 10) ,retries := (retries + 1) to wait_ap_answer; from wait_ap_answer :eager input close_mti(sender) from q_mti_0 /* stop */ to stop; from mti_active :eager input stop_ho_seek_info(sender) from q_mti_0 do output mpdu_tip(mti_0,mt_mac_addr, end_tip) to env to mti_active; process mtc_0 :buffer q_mtc_0; var sender : pid; parent : pid; offspring : pid; t_neigh_search : timer; tip_flag: bool; beacon_received: bool; i: int; j: int; the_channel: channel_id_type; old_channel: channel_id_type; ap_mac_addr: ap_mac_addrtype; urgency: susp_type; ho: ho_type; state start :init; wait_init discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info in q_mtc_0; end; stop discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, close_mtc, init_mtc in q_mtc_0; end; non_associated discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; wait_synchro discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; associated discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, init_mtc in q_mtc_0; end; q33 :nostable; wait_ap_acquisition_due_to_ho discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; q43 :nostable; q46 :nostable; wait_resume_msc discard neigh_ap_load_info_cnf, suspend_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; q54 :nostable; return_to_old_ap discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; q60 :nostable; wait_data discard suspend_msc_ok, resume_msc_ok, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; test_j80 :nostable; q82 :nostable; q83 :nostable; q85 :nostable; back_ho88 :nostable; q95 :nostable; wait_ap_acquisition_due_to_tip discard neigh_ap_load_info_cnf, suspend_msc_ok, resume_msc_ok, measure_rlq_cnf_mtc, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; q105 :nostable; q108 :nostable; susp_msc123 :nostable; wait_ack_suspended discard neigh_ap_load_info_cnf, resume_msc_ok, measure_rlq_cnf_mtc, acquire_new_ap_ko, acquire_new_ap_ok, association_completed, synchro_with, get_target_ap, init_ho_seek_info_ko, init_ho_seek_info_ok, send_neigh_ap_info, init_mtc in q_mtc_0; end; q133 :nostable; q28 :nostable; transition from start :eager /* start */ to wait_init; from wait_init :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from wait_init :eager input init_mtc(sender) from q_mtc_0 do beacon_received := false to non_associated; from non_associated :eager input synchro_with(sender, ap_mac_addr) from q_mtc_0 /* find frequency for given AP_MAC_Addr and return it in the_channel */ do the_channel := ap_mac_addr ,output acquire_new_ap(mtc_0,the_channel) to env to wait_synchro; from wait_synchro :eager input acquire_new_ap_ko(sender) from q_mtc_0 do output synchro_with_ack(mtc_0,failed) to env ,beacon_received := false to non_associated; from wait_synchro :eager input acquire_new_ap_ok(sender) from q_mtc_0 do output synchro_with_ack(mtc_0,success) to env ,beacon_received := false to non_associated; from wait_synchro :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from non_associated :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from non_associated :eager input association_completed(sender) from q_mtc_0 do set t_neigh_search := (0 + 10) to associated; from associated :eager input get_target_ap(sender, ho) from q_mtc_0 do reset t_neigh_search ,tip_flag := false ,i := 1 to q33; from q33 :eager if ho = forward_ho /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_ho; from wait_ap_acquisition_due_to_ho :eager input acquire_new_ap_ko(sender) from q_mtc_0 do i := (i + 1) to q43; from q43 :eager if (i <= 5) = false do i := 1 to q46; from q46 :eager if tip_flag = false /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_ho; from q46 :eager if tip_flag = true do output resume_msc(mtc_0) to env to wait_resume_msc; from wait_resume_msc :eager input resume_msc_ok(sender) from q_mtc_0 to q54; from q54 :eager if tip_flag = false do output acquire_new_ap(mtc_0,old_channel) to env to return_to_old_ap; from return_to_old_ap :eager input acquire_new_ap_ok(sender) from q_mtc_0 to q60; from q60 :eager if tip_flag = true do tip_flag := false ,output stop_ho_seek_info(mtc_0) to q_mti_0 ,set t_neigh_search := (0 + 10) to associated; from q60 :eager if tip_flag = false do ap_mac_addr := old_channel ,the_channel := old_channel ,output target_ap_found(mtc_0,ap_mac_addr) to env to associated; from return_to_old_ap :eager input acquire_new_ap_ko(sender) from q_mtc_0 do output ap_lost(mtc_0) to env ,beacon_received := false to non_associated; from return_to_old_ap :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from q54 :eager if tip_flag = true do output resume_mhi(mtc_0) to env ,output acquire_new_ap(mtc_0,old_channel) to env to return_to_old_ap; from wait_resume_msc :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from q43 :eager if (i <= 5) = true /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_ho; from wait_ap_acquisition_due_to_ho :eager input acquire_new_ap_ok(sender) from q_mtc_0 do j := 1 ,output measure_rlq_req_mtc(mtc_0) to env to wait_data; from wait_data :eager input measure_rlq_cnf_mtc(sender) from q_mtc_0 /* join */ to test_j80; from test_j80 :eager /* test_j: */ to q82; from q82 :eager if (j = 2) = false to q83; from q83 :eager if tip_flag = false to q85; from q85 :eager if ho = forward_ho /* find frequency for current index i and return it in the_channel */ do ap_mac_addr := i ,output target_ap_found(mtc_0,ap_mac_addr) to env ,beacon_received := false to non_associated; from q85 :eager if ho = backward_ho to back_ho88; from back_ho88 :eager /* back_ho: */ do output resume_msc(mtc_0) to env to wait_resume_msc; from q83 :eager if tip_flag = true do i := (i + 1) to q95; from q95 :eager if (i <= 5) = false /* join */ to back_ho88; from q95 :eager if (i <= 5) = true /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_tip; from wait_ap_acquisition_due_to_tip :eager input acquire_new_ap_ko(sender) from q_mtc_0 do i := (i + 1) to q105; from q105 :eager if (i <= 5) = false do i := 1 to q108; from q108 :eager if tip_flag = false /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_ho; from q108 :eager if tip_flag = true do output resume_msc(mtc_0) to env to wait_resume_msc; from q105 :eager if (i <= 5) = true /* find frequency for current index i and return it in the_channel */ do the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to wait_ap_acquisition_due_to_tip; from wait_ap_acquisition_due_to_tip :eager input acquire_new_ap_ok(sender) from q_mtc_0 do j := 2 ,output measure_rlq_req_mtc(mtc_0) to env ,output neigh_ap_load_info_req(mtc_0) to env to wait_data; from wait_ap_acquisition_due_to_tip :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from q82 :eager if (j = 2) = true do j := 1 to wait_data; from wait_data :eager input neigh_ap_load_info_cnf(sender) from q_mtc_0 to test_j80; from wait_data :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from wait_ap_acquisition_due_to_ho :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from q33 :eager if ho = backward_ho do urgency := later /* join */ to susp_msc123; from susp_msc123 :eager /* susp_msc: */ do output suspend_msc(mtc_0,urgency) to env to wait_ack_suspended; from wait_ack_suspended :eager input suspend_msc_ok(sender) from q_mtc_0 do i := 1 ,old_channel := the_channel /* find frequency for current index i and return it in the_channel */ ,the_channel := i ,output acquire_new_ap(mtc_0,the_channel) to env to q133; from q133 :eager if tip_flag = true to wait_ap_acquisition_due_to_tip; from q133 :eager if tip_flag = false to wait_ap_acquisition_due_to_ho; from wait_ack_suspended :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; from associated :eager input init_ho_seek_info_ok(sender) from q_mtc_0 do tip_flag := true ,output suspend_mhi(mtc_0) to env ,urgency := immediately to susp_msc123; from associated :eager input init_ho_seek_info_ko(sender) from q_mtc_0 do set t_neigh_search := (0 + 10) to associated; from associated :eager input send_neigh_ap_info(sender) from q_mtc_0 do beacon_received := true /* Store neigh AP infos */ to associated; from associated :eager if (t_neigh_search = 0) /* expire t_neigh_search */ do reset t_neigh_search to q28; from q28 :eager if beacon_received = true do output init_ho_seek_info(mtc_0) to q_mti_0 to associated; from q28 :eager if beacon_received = false do set t_neigh_search := (0 + 10) to associated; from associated :eager input synchro_with(sender, ap_mac_addr) from q_mtc_0 /* find frequency for given AP_MAC_Addr and return it in the_channel */ do the_channel := ap_mac_addr ,output acquire_new_ap(mtc_0,the_channel) to env to wait_synchro; from associated :eager input close_mtc(sender) from q_mtc_0 /* stop */ to stop; /* translation - 736 lines */