Railway 2014
Page tree

Versions Compared

Old Version 9

changes.mady.by.user Unknown User (sna)

Saved on

compared with

New Version 10

changes.mady.by.user Unknown User (sna)

Saved on

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

input int *_perm;
output bool *_req[11];
input int trainNum;
input int depTrack;
input int destTrack;
input bool cleanup;
input bool debug;
output int arrTrack;
int i_arrOnTrack;
 
initial state *_ST {
    entry debug / 'println([trainNum][ST-ST] ... )';
 
    initial state waitForPerm {
        entry / *_ST_4_req[trainNum] = true;
        entry / *_LN_0_req[trainNum] = true;
    }
    --> gotPerm with (*_ST_4_perm == trainNum) & (*_LN_0_perm == trainNum)
    --> backOff with (*_ST_4_perm == trainNum) | (*_LN_0_perm == trainNum);
 
    state backOff
    --> backOff1;
 
    state backOff1 {
entry / *_ST_4_req[trainNum] = false;
entry / *_LN_0_req[trainNum] = false;
    }
    --> waitForPerm;
 
final state gotPerm;
}
>-> Dep_*_ST;
 
state Dep_IC_ST {
    entry / 'railPoint(*,STRAIGHT)';
    entry / 'railSignal(*_LN_0, FWD, RED)';
    entry / 'railTrack(*_LN_0,FWD,trainNum,NORMAL)';
    entry / 'railTrack(*_ST_4,FWD,trainNum,NORMAL)';
    entry depTrack == 1 / 'railSignal(*_ST_1, FWD, GREEN)';
    entry depTrack == 2 / 'railSignal(*_ST_2, FWD, GREEN)';
    entry depTrack == 3 / 'railSignal(*_ST_3, FWD, GREEN)';
    ..........
  } --> *_LN_0 with 'railContact(*_LN_0,0)';
 
  state *_LN_0 {
    entry / 'println("[trainNum][ST-ST] Entering *_LN_0")';
    entry debug / 'println("[trainNum][ST-ST] Requesting permission for *_LN_1")';
    entry depTrack == 1 / 'railSignal(*_ST_1, FWD, RED)';
    entry depTrack == 2 / 'railSignal(*_ST_2, FWD, RED)';
    entry depTrack == 3 / 'railSignal(*_ST_3, FWD, RED)';
    entry / *_LN_1_req[trainNum] = true;
 
    region Travel:
      initial state Entry
      --> Continue with 'railContact(*_LN_0,0)' & (*_LN_1_perm == trainNum)
      --> Slowdown with 'railContact(*_LN_0,0)';
 
      state Slowdown {
        entry debug / 'println("[trainNum][ST-ST] Slowing down on *_LN_0")';
        entry / 'railTrack(*_LN_0,FWD,trainNum,CAUTION)';
      }
      --> Waiting with 'railContact(*_LN_0,1)'
      --> Continue with *_LN_1_perm == trainNum;
 
      state Waiting {
        entry debug / 'println("[trainNum][ST-ST] Stopping on *_LN_0")';
        entry / 'railTrackBrake(*_LN_0)';
      }
      --> Continue with *_LN_1_perm == trainNum;
 
      final state Continue {
        entry debug / 'println("[trainNum][ST-ST] Continuing on *_LN_0")';
        entry / 'railSignal(*_LN_0,FWD,GREEN)';
        entry / 'railTrack(*_LN_0,FWD,trainNum,NORMAL)';
        entry / 'railTrack(*_LN_1,FWD,trainNum,NORMAL)';
        entry / 'railSignal(*_LN_1, FWD, RED)';
      };
 
    region Cleanup:
      initial state Entry
      --> cleanup with 'railContact(*_LN_0,0)';
 
      final state cleanup {
      entry debug / 'println("[trainNum][ST-ST] Entered *_LN_0 completely")';
      entry / 'railTrackOff(*_ST_4)';
      entry / *_ST_4_req[trainNum] = false;
      };
  }>-> *_LN_0_*_LN_1;
 
  state IC_LN_0_IC_LN_1
  --> IC_LN_1 with 'railContact(IC_LN_1,0)';
 
// ...................
// Set of track segment controlling states such as before
// ...................
 
state *_LN_5 {
    int perm_all_next_segments = false;
    entry / 'println("[trainNum][ST-ST] Entering *_LN_5")';
    entry / 'railSignal(*_LN_4, FWD, RED)';
 
    region Travel:
      initial state Entry
      --> Continue with 'railContact(*_LN_5,0)' & perm_all_next_segments
      --> Slowdown with 'railContact(*_LN_5,0)';
 
      state Slowdown {
        entry debug / 'println("[trainNum][ST-ST] Slowing down on *_LN_5")';
        entry / 'railTrack(*_LN_5,FWD,trainNum,CAUTION)';
      }
      --> Waiting with 'railContact(*_LN_5,1)'
      --> Continue with perm_all_next_segments;
 
      state Waiting {
        entry debug / 'println("[trainNum][ST-ST] Stopping on *_LN_5")';
        entry / 'railTrackBrake(*_LN_5)';
      }
      --> Continue with perm_all_next_segments;
 
      final state Continue {
        entry debug / 'println("[trainNum][ST-ST] Continuing on *_LN_5")';        
        entry i_arrOnTrack == 1 / 'railTrack(*_ST_1,FWD,trainNum,NORMAL)';
        entry i_arrOnTrack == 2 / 'railTrack(*_ST_2,FWD,trainNum,NORMAL)';
        entry i_arrOnTrack == 3 / 'railTrack(*_ST_3,FWD,trainNum,NORMAL)';
        ----------
        entry / arrTrack = i_arrOnTrack;
      };
 
    region Cleanup:
      initial state Entry
      --> cleanup with 'railContact(*_LN_5,0)';
 
      final state cleanup {
        entry debug / 'println("[trainNum][ST-ST] Entered *_LN_5 completely")';
        entry / 'railTrackOff(*_LN_4)';
        entry / *_LN_4_req[trainNum] = false;
      };
 
    region Permissions:
      initial state checking {
        entry / *_ST_0_req[trainNum] = true;
        entry destTrack == 1 | !cleanup / *_ST_1_req[trainNum] = true;
        entry destTrack == 2 | !cleanup / *_ST_2_req[trainNum] = true;
        entry destTrack == 3 | !cleanup / *_ST_3_req[trainNum] = true;
      }
      --> success with destTrack == 1 & *_ST_0_perm == trainNum & *_ST_1_perm == trainNum / i_arrOnTrack = 1      --> success with destTrack == 2 & *_ST_0_perm == trainNum
                                      & *_ST_21_perm == trainNum / i_arrOnTrack = 21
      --> success with destTrack == 32 & *_ST_0_perm == trainNum & *_ST_3_perm == trainNum / i_arrOnTrack = 3      --> success with *_ST_0_perm == trainNum
                                      & *_ST_12_perm == trainNum / i_arrOnTrack = 12
      --> success with *_ST_0_permdestTrack == trainNum3 & *_ST_20_perm == trainNum /
  i_arrOnTrack = 2      --                                  & *_ST_3_perm == trainNum / i_arrOnTrack = 3
      --> success with *_ST_0_perm == trainNum & *_ST_31_perm == trainNum / i_arrOnTrack = 31
      --> resolvingsuccess with *_ST_0_perm == trainNum |& *_ST_32_perm == trainNum |/ *_i_arrOnTrack = 2
      --> success with *_ST_0_perm == trainNum & *_ST_3_perm == trainNum / i_arrOnTrack = 3
      --> resolving with *_ST_0_perm == trainNum | *_ST_3_perm == trainNum 
                                                 | *_ST_2_perm == trainNum 
                                                 | *_ST_1_perm == trainNum;
 
      state resolving
      --> resolving1;
 
      state resolving1 {
        entry / *_ST_0_req[trainNum] = false;
        entry / *_ST_1_req[trainNum] = false;
        entry / *_ST_2_req[trainNum] = false;
        entry / *_ST_3_req[trainNum] = false;
      }
      --> checking;
 
      state success
      --> success1;
 
      final state success1 {
        entry !(i_arrOnTrack == 1) / *_ST_1_req[trainNum] = false;      
        entry !(i_arrOnTrack == 2) / *_ST_2_req[trainNum] = false;
        entry !(i_arrOnTrack == 3) / *_ST_3_req[trainNum] = false;
        entry / perm_all_next_segments = true;
      };
  }>-> *_LN_5_*_ST;
 
  state *_LN_5_*_ST
  --> Arr_*_ST with i_arrOnTrack == 1 & 'railContact(*_ST_1,0)'
  --> Arr_*_ST with i_arrOnTrack == 2 & 'railContact(*_ST_2,0)'
  --> Arr_*_ST with i_arrOnTrack == 3 & 'railContact(*_ST_3,0)';
 
  state Arr_*_ST {
    entry / 'railSignal(*_LN_5, FWD, RED)';
    entry / 'railTrackOff(*C_LN_5)';
    entry / 'railTrack(*_ST_0,FWD,trainNum,SLOW)';
    entry i_arrOnTrack == 1 / 'railTrack(*_ST_1,FWD,trainNum,SLOW)';
    entry i_arrOnTrack == 2 / 'railTrack(*_ST_2,FWD,trainNum,SLOW)';
    entry i_arrOnTrack == 3 / 'railTrack(*_ST_3,FWD,trainNum,SLOW)';
    entry / *_LN_5_req[trainNum] = false;
 
    initial state SlowEntry
    --> Slow with i_arrOnTrack == 1 & 'railContact(*_ST_1,0)'
    --> Slow with i_arrOnTrack == 2 & 'railContact(*_ST_2,0)'
    --> Slow with i_arrOnTrack == 3 & 'railContact(*_ST_3,0)';
 
    state Slow {
      entry / 'railTrackOff(*_ST_0)';
      entry / *_ST_0_req[trainNum] = false;
    }
    --> Halt with i_arrOnTrack == 1 & 'railContact(*_ST_1,1)'
    --> Halt with i_arrOnTrack == 2 & 'railContact(*_ST_2,1)'
    --> Halt with i_arrOnTrack == 3 & 'railContact(*_ST_3,1)';
 
    final state Halt {
      entry i_arrOnTrack == 1 / 'railTrackBrake(*_ST_1)';
      entry i_arrOnTrack == 2 / 'railTrackBrake(*_ST_2)';
      entry i_arrOnTrack == 3 / 'railTrackBrake(*_ST_3)';
      entry i_arrOnTrack == 1 / 'railArrival(trainNum, *_ST_1)';
      entry i_arrOnTrack == 2 / 'railArrival(trainNum, *_ST_2)';
      entry i_arrOnTrack == 3 / 'railArrival(trainNum, *_ST_3)';
    };
  }
  >-> done;
 
  state done
  --> reallyDone with 'railDeparture(trainNum)';
 
  final state reallyDone;

// All permissiions variables

// All request variables

// Train number

// Departure track number

// Destination track number

// Cleanup flag for selecting the track of destination

// Debug flag for additional output

// Arrival track

// Variable (arrival track) for selecting correct station elements

 

// Handles departing from a station

// Additional output for debugging

 

// State, which set requests for needed tracks

 

 

 

// Transition for received all needed permissions

// Tranisition for received some needed permissions

 

// State for waiting an additional Tick

 

 

// State, which releases the requests for needed tracks

 

 

 

// Transition to trying the requesting again

 

 

 

// Transition to the departure state

 

// State, which handles the train departure

// Set of entry-Actions to set tracks, points and signals according to depTrack

 


 

 

 

 

 

// Transition to next track segment, if contact is readed

 

// State for handling the train on track *_LN_0

// Outputs for debugging

 

// Entry-Actions to set the previous signals to RED

 

 

// Requesting the next segment

 

// Region for handling train driving

 

// Transition to continuing state, if permitted

// Transition to slowing down else

 

// State for slowing down

// Addtitional output for debugging

// Entry-Action for slowing down the train

 

// Transition to waiting state

// Transition to continuing state, if permitted

 

// Waiting state

// Addtitional output for debugging

// Entry-Action for stopping the train

 

// Tranisition to continuing state

 

// State to continuing driving on the track

// Addtitional output for debugging

// Entry-Actions to set tracks and signals for driving

 

 

 

 

 

// Region for handling cleanup-functionalities

 

// Transition to cleanup state

 

// Cleanup state

// Addtitional output for debugging

// Entry-Action to switching off the previous track

// Entry-Action to release the previous track

 

// Transition to transitional state

 

// Transitional state

// Transition to next track segment, if contact is readed

 

 

 

 

 

// State for entering a station

// Variable for checking all needed permissions

// Output

// Setting signal to RED

 

// Region for handling train driving

 

// Transition to continuing state, if permitted

// Transition to slowing down else

 

// State for slowing down

// Addtitional output for debugging

// Entry-Action for slowing down the train

 

// Transition to waiting state

// Transition to continuing state, if permitted

 

// Waiting state

// Addtitional output for debugging

// Entry-Action for stopping the train

 

// Tranisition to continuing state

 

// State to continuing driving on the track

// Addtitional output for debugging

// Set of entry-Actions for setting tracks, points and signals according to i_arrOnTrack

 

 

 

// Setting the arrival track (output)

 

 

// Region for handling cleanup-functionalities

 

// Transition to cleanup state

 

// Cleanup state

// Addtitional output for debugging

// Entry-Action to switching off the previous tracks

// Entry-Action to release the previous tracks

 

 

// Region for handling permissions of all needed tracks

// State for requesting all needed tracks according to destination track and cleanup-Flag

 

 

 

 

 

// Transitions for permitted tracks match wished tracks

 

 

// Transitions for permitted tracks don't match wished tracks

 

 

// Transition for not all tracks permitted

 

// State for waiting an additional tick

 

 

// State for releasing track requests

 

 

 

 

 

// Transition for trying the requesting again

 

// State for waiting an additional tick

 

 

// State for releasing not used track requests and

 

 

 

// Settting perm_all_next_segments to true

 

// Transition to station entry states

 

// State waiting for station entry

 

 

 

 

// State for setting tracks, points and signals according to i_arrOnTrack

// and releasing previous track request

 

 

 

 

 

 

 

// State for slowing down, if train completely on track

 

 

 

 

// State for switching off previous track and releasing the request

 

 

 

// Transitions to halt states, if train at second contact of a track

 

 

 

 

// Entry-Actions for braking the train on correct track

 

 

// Entry-Actions for waiting for timer on correct track

 

 

 

 

 

 

 

// Transition to final state, if timer is ready