DocName Project Version FullName ShortDescription
EnvTrack RailwayCrossing V7
A track may still have only one type of train at one time. It consists of two sensors, ts1 corresponds to the sensor that signals the approach of a train, and ts2 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 a new train. Increment noOfTrains. After creating, send initTrain to the new train with the appropiate parameters. Notify the last train on track with the new train by sending 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 creation of a track switch curState to init1 and wait for the signal initTrack. Set typeOfTrack, and perToCreTrain to the given values. 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. f
ModelName FullName Type Value Tasks Usage Description
typeOfTrack TrackType := Enum (regular, fast) regular EnvTrackTask1 r
EnvTrackTask9 w
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 EnvTrackTask1 p xxx
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 xxx EnvTrackTask9 c xxx