DocName Project Version FullName ShortDescription
EnvTrack RailwayCrossing V3
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.
Constraints: (1) While a train is passing the gate, that means the train is between the signal and trainSens2, no other train is reaching trainsSens1. The time between the creation of the trains has to be set accordingly. 
ModelName Number Type
trainSens 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 the current signalState via the new train via newSignalState 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. Send newTrain to trainSens1. f
EnvTrackTask7 train leaves gate Receiving trainPassed signals that a train has left the gate. Decrement noOfTrains. Send newTrain to trainSens2. f
ModelName FullName Type Value Tasks Usage Description
typeOfTrack TrackType := Enum (regular, fast) regular
noOfTrains Integer 0
perToCreTrain Duration ???
signalState 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
setTypeOfCreMode CreationModeType EnvTrackTask5 c
setTypeOfTrack TrackType EnvTrackTask4 c
newSignalState SignalStateType EnvTrackTask3 p/c
EnvTrackTask1 p
EnvTrackTask8 c
setPerToCreTrain Duration EnvTrackTask2 c
creNewTrain EnvTrackTask1 c
RequestNo Type Method Tester Description Transferred Corrector Corrected