DocName Project Version FullName ShortDescription
EnvTrack RailwayCrossing V6
A track may still have only one type of train at one time. It consists of two sensors, trainSens1 corresponds to the sensor that signals the approach of a train, and trainSens2 signals the leaving of the gate.
ModelName Number Type
tS 2 EnvTrainSens
sig 1 EnvSignal
trains n EnvTrain
ModelName Description Strategy StrategyType RealizedRequirement
EnvTrackTask1 Creation of Trains Depending on typeOfTrack, create on request (creNewTrain) or periodically (every perToCreTrain) a new train. Increment noOfTrains. After creating, send initTrain to the new train with the appropiate parameters.  f
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
EnvTrackTask8 receiving a new signal state Change signalState  by receiving newSignalState. 
EnvTrackTask4 changing type of track By receiving setTypeOfTrack, the type of new trains changes from regular to fast or vice versa, depending on the given parameter. Change the value of typeOfTrack stop creating new trains, until the track is empty. Set the period to the smallest acceptable value and, in case of creationMode = period, create new trains (EnvTrackTask1).  f
EnvTrackTask5 setting type of creation Mode Receive setTypeOfCreMode and set the creationMode to the given value. f
EnvTrackTask6 train receives signal The receiving of sigReach implies, that a train has stop at (signalState is stop) or has passed (signalState is go) sig1. f
EnvTrackTask10 train receives ts1 The receiving of trainArrived implies, that a train has arrived ts1. Send newTrain to ts1.
EnvTrackTask7 train leaves gate Receiving trainPassed signals that a train has left the gate. Decrement noOfTrains. Send newTrain to ts2. f
EnvTrackTask9 initialization after creation of a track, wait for the signal initTrack. Set typeOfTrack, creationMode, and perToCreTrain to the given values. Send getSignalState, wait for the reply (newSignalState) and store the value in sigState.
ModelName FullName Type Value Tasks Usage Description
typeOfTrack TrackType := Enum (regular, fast) regular
noOfTrains Integer 0
perToCreTrain Duration ???
sigState SignalStateType := Enum (go, stop) stop
creationMode CreationModeType := Enum (period, event) period
ModelName FullName Parameters Tasks Usage Description
newTrain EnvTrackTask6, EnvTrackTask7 p
sigReached EnvTrackTask6 c
trainPassed EnvTrackTask7 c
trainArrived EnvTrackTask10
setTypeOfCreMode CreationModeType EnvTrackTask5 c
setTypeOfTrack TrackType EnvTrackTask4 c
newSignalState SignalStateType EnvTrackTask3 p/c
EnvTrackTask8, EnvTrackTask9 c
getSignalState EnvTrackTask9
setPerToCreTrain Duration EnvTrackTask2 c
creNewTrain EnvTrackTask1 c
initTrain CharString, Duration, Duration, Duration, SignalStateType EnvTrackTask1 p instanceName, ts1Dur, ts1Sig1Dur, Sig1ts2Dur, sigState
initTrack TrackType, CreationModeType, Duration EnvTrackTask9 c