DocName Project Version FullName ShortDescription
EnvTrain RailwayCrossing V1 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. 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 gets zero, switch curMode to sigStop or pass, depending an signalState. Set passTime to the given value. Send the reaching to the track via newSignalReached f
EnvTrainTask4 Changing the signal If curMode is appGo and newSignalState (red) is received, switch to appStop and vice versa. f
EnvTrainTask5 Passing the gate While passing the gate, count down passTime. If it gets zero, send trainPassed to the track and terminate. f
ModelName FullName Type Value Tasks Usage Description
signalState Enum (red, green) red EnvTrainTask1, EnvTrainTask3 r/w
appTime approach time Duration 0 EnvTrainTask1, EnvTrainTask2, EnvTrainTask3 w time to approach to signal
curMode current mode Enum (idle, appGo, appStop) 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
getSignalState EnvTrainTask1 p (EnvTrainTask1:*:EnvTrain)=$1
> $1
newSignalState SignalStateType EnvTrainTask1, EnvTrainTask4 c
trainPassed EnvTrainTask5 p (EnvTrainTask5:*:EnvTrain)=$1
> $1