/***************************************************************************** * visualSTATE Validator Test Sequence File, Format 2.2 * Generated by visualSTATE Validator 5.4.0.1273 * Trace: No * Additional modules: visualSTATE VSLFx 5.4.0.1273 * Time: 2007-11-19 11:45:22 * visualSTATE Project File: * visualSTATE Signature Generator: "50" * Project Signature: "e153 19db af6c 4b8c 321e 1a73" *****************************************************************************/ PROJECT INFORMATION Project Name: cesar_cp Explanation: "" ****************************************************************************** # SEQUENCE INFORMATION # Sequence Name: "Sequence 0" # Explanation: "" # Created : 2007-11-16 10:07:27 # Modified : 2007-11-19 11:45:03 # STEPS # Send Event # System: main_fsm # Event: SE_RESET() # HierarchicalStateVector: Station.Station.INIT_SYSTEM, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: init_system(); # Signals: # Variables: # Send Event # System: sta_connection[0] # Event: SE_RESET() # HierarchicalStateVector: Topstate1.UNCONNECTED; # Actions: # Signals: # Variables: # Send Event # System: main_fsm # Event: RECEIVE_DRV_MAC_START_REQ(0) # HierarchicalStateVector: Station.Station.ON.POND_OR_USTA.POND, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: process_drv_start_mac_req(0), launch_ustt_timer(), launch_bbt_timer(), trace_pond(); # Signals: # Variables: # Send Event # System: main_fsm # Event: TO_CCO() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(1), trace_cco(), cp_station_set_assoc_status(1); # Signals: # Variables: # Send Event # System: main_fsm # Event: TO_HANDOVER() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.HANDOVER, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: # Signals: # Variables: # Send Event # System: main_fsm # Event: HANDOVER_DONE() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.ASSOCIATED_STA.AUTHENTICATED, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(0), trace_sta(), cp_station_set_auth_status(1); # Signals: # Variables: # Send Event # System: main_fsm # Event: TO_HANDOVER() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.ASSOCIATED_STA.AUTHENTICATED, Station.Small_FSMs.SMALL_FSM.Handover_Region.HANDOVER, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: # Signals: # Variables: # Send Event # System: main_fsm # Event: HANDOVER_DONE() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_auth_status(0), cp_station_set_cco_status(1), trace_cco(); # Signals: # Variables: # Send Event # System: main_fsm # Event: JOIN_WAIT_TIMER_EXPIRES() # HierarchicalStateVector: Station.Station.ON.UCCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(0), cp_station_set_assoc_status(0), trace_ucco(), send_discover_beacon_as_ucco(); # Signals: # Variables: # Send Event # System: main_fsm # Event: RECEIVE_CC_ASSOC_REQ(0) # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.NO_AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: process_cc_assoc_req(0), cp_station_set_cco_status(1), trace_cco(), cp_station_set_assoc_status(1); # Signals: # Variables: # Send Event # System: main_fsm # Event: BEACON_DETECTED(0) # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: launch_beacon_timer(); # Signals: # Variables: # Send Event # System: main_fsm # Event: JOIN_WAIT_TIMER_EXPIRES() # HierarchicalStateVector: Station.Station.ON.POND_OR_USTA.USTA, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(0), cp_station_set_assoc_status(0), launch_ustt_timer(), trace_usta(); # Signals: # Variables: # Send Event # System: main_fsm # Event: TO_CCO() # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(1), trace_cco(), cp_station_set_assoc_status(1); # Signals: # Variables: # Send Event # System: main_fsm # Event: RECEIVE_CC_ASSOC_REQ(0) # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(0), process_cc_assoc_req(0); # Signals: # Variables: # Send Event # System: main_fsm # Event: RECEIVE_CC_SET_TEI_MAP_REQ(0) # HierarchicalStateVector: Station.Station.ON.STA_OR_CCO.CCO, Station.Small_FSMs.SMALL_FSM.Handover_Region.NORMAL, Station.Small_FSMs.SMALL_FSM.AVLN_Tracking.AVLN_TO_TRACK, Station.Small_FSMs.SMALL_FSM.Proxy_CCO.NOT_PCCO, Station.Small_FSMs.SMALL_FSM.BackupCCO.NOT_BACKUP, Station.Small_FSMs.SMALL_FSM.SC_Level.SC_NONE; # Actions: cp_station_set_cco_status(0), process_cc_set_tei_map_req(0); # Signals: # Variables: ******************************************************************************