DocName Project Version FullName ShortDescription
EnvTrack RailwayCrossing V7
All trains on a track must be of the same type (regular or fast) at any given time. A track consists of two sensors. Sensor ts1 corresponds to the sensor that signals the approach of a train, and ts2 signals the leaving of the gate. Further, each track has a signal.
ModelName Number Type
ts 2 EnvTrainSens
sig 1 EnvSignal
trains n EnvTrain
ModelName Description Strategy StrategyType RealizedRequirement
EnvTrackTask1 Creation of Trains Dynamically create a new train. Then, increment the noOfTrains

After creation, send initTrain to the new train with the appropriate parameters (ts1Dur, ts1SigDur, sigTs2Dur, breakDur, minDistDur). 

Finally, notify the last train on the track of the new train by sending the signal newSeqTrain.

f EnvTrackTask4, EnvTrackTask5
EnvTrackTask2 setting period to create new trains Receive the new new period (perToCreTrain) via setPerToCreTrain. Set creationMode to period.  f
EnvTrackTask3 propagation the change of newSignalState to all trains If newSignalState receives, propagate the new value by sending newSignalState with the new state to all trains. p
EnvTrackTask4 creating train on request After receiving creNewTrain, set curMode to event and create a new train. f
EnvTrackTask5 creating trains periodically If curMode is period, create every perToCreTrain a new train. f
EnvTrackTask6 receiving a new signal state Change sigState by receiving newSignalState.  f
EnvTrackTask7 train leaves gate Receiving trainPassed signals that a train has left the gate. Decrement noOfTrains. Send newTrain to ts2. f
EnvTrackTask8 train receives ts1 The receiving of trainArrived implies, that a train has arrived ts1. Send newTrain to ts1. f
EnvTrackTask9 initialization After the creation of a track switch curState to init1 and wait for the signal initTrack

Set ts1Dur, ts1SigDur, sigTs2Dur, breakDur, minDistDur, and perToCreTrain to the values provided by initTrack

Send getSignalState, switch curState to init2 and wait for the reply (newSignalState). Store the given value in sigState and switch curState to the given value.

ModelName FullName Type Value Tasks Usage Description
ts1Dur approach duration Duration 0 EnvTrackTask9 w duration to reach the ts1
EnvTrackTask1 r
ts1SigDur signal duration Duration 0 EnvTrackTask9 w duration from ts1 to signal
EnvTrackTask1 r
sigTs2Dur passing duration Duration 0 EnvTrackTask9 w duration from the signal to ts2
EnvTrackTask1 r
breakDur breaking duration Duration 0 EnvTrackTask9 w duration that is needed to break
EnvTrackTask1 r
minDistDur minimum distance duration Duration 0 EnvTrackTask9 w minimum time difference between two trains
EnvTrackTask1 r
noOfTrains Integer 0 EnvTrackTask1, EnvTrackTask7 w
perToCreTrain Duration 0 EnvTrackTask2, EnvTrackTask9 w
EnvTrackTask5 r
curMode CreationMode:= Enum (init1, init2, period, event) period EnvTrackTask2, EnvTrackTask4, EnvTrackTask9 w
EnvTrackTask5 r
sigState SignalStateType := Enum (go, halt) halt EnvTrackTask6, EnvTrackTask9 w
EnvTrackTask1, EnvTrackTask3 r
ModelName FullName Parameters Tasks Usage Description SignalPaths
newSeqTrain CharString, CharString EnvTrackTask1 p Parameters:
Receiver, seqTrain
initTrain CharString, Duration, Duration, Duration, Duration, Duration, SignalStateType EnvTrackTask1 p Parameters: 
Instancename, ts1Dur, ts1SigDur, sigTs2Dur, 
minDistDur, sigState
setPerToCreTrain CharString, Duration EnvTrackTask2 c Parameters:
Receiver, Period
newSignalState SignalStateType:= Enum (go, halt) EnvTrackTask3 p/c Parameters:
Receiver, signal state
EnvTrackTask6 c
creNewTrain EnvTrackTask4 c
trainPassed EnvTrackTask7 c
trainArrived CharString EnvTrackTask8 c Parameters:
newTrain CharString EnvTrackTask7, EnvTrackTask8 p Parameters:
initTrack CharString, Duration, Duration, Duration, Duration, Duration, Duration EnvTrackTask9 c Parameters: 
Instancename, ts1Dur, ts1SigDur, sigTs2Dur, 
minDistDur, perToCreateTrains