DocName Project Version FullName ShortDescription
EnvTrain RailwayCrossing V2 Environment train
ModelName Number Type Version
ModelName Description Strategy StrategyType RealizedRequirement
EnvTrainTask1 Creation of a train After creation a train, it switchs to the mode idle (curMode). Set the time for approaching the signal (appTime) to the given value and send getSignalState to the signal. Get the minimum delay time (getMinDelayDur, setMinDelayDur) and set minDelayDur. After receiving newSignalState, switch to appGo or appStop, depending on the current state of the signal (signalState). f
EnvTrainTask2 Approaching the signal If curMode changes to appGo, restart counting down the appTime.  If curMode changes to appStop, stop counting down the appTime. f
EnvTrainTask3 Reaching the signal If appTime becomes zero, switch curMode to sigStop or sigPass, depending an signalState. Set passTime to the given value. Notify the track of the reaching via sending newSignalReached f
EnvTrainTask4 Receiving new signal state If curMode is appGo and newSignalState (stop) is received, count down the appTime to the next availabale, predefined point (computed using minDelayDur) and after raching this point, switch to appStop. 
In newSignalState (go) is received, switch to appGo or stop counting down appTime to the next predefined value.
EnvTrainTask5 Passing the gate While passing the gate, count down passTime. If it becomes zero, send trainPassed to the track and terminate. f
ModelName FullName Type Value Tasks Usage Description
minDelayDur Duration 0 EnvTrainTask1, EnvTrainTask4 r/w minimum time difference between two trains
appTime approach time Duration 0 EnvTrainTask1, EnvTrainTask2, EnvTrainTask3 w time to approach to signal
curMode current mode Enum (idle, appGo, appStop, sigPass, sigStop) idle EnvTrainTask1, EnvTrainTask2, EnvTrainTask3, EnvTrainTask4 w
passTime passing time Duration 0 EnvTrainTask3, EnvTrainTask5 time to pass from the signal to the leaving sensor
ModelName FullName Parameters Tasks Usage Description SignalPaths
newSignalReached EnvTrainTask1, EnvTrainTask3 p (EnvTrainTask[1,3]:*:EnvTrain)=$1
> $1
setMinDelayDur Duration EnvTrainTask1 c
getMinDelayDur EnvTrainTask1 p (EnvTrainTask1:*:EnvTrain)=$1
> $1
getSignalState EnvTrainTask1 p (EnvTrainTask1:*:EnvTrain)=$1
> $1
newSignalState SignalStateType EnvTrainTask1, EnvTrainTask4 c
trainPassed EnvTrainTask5 p (EnvTrainTask5:*:EnvTrain)=$1
> $1