DocName Project Version FullName ShortDescription
EnvTrack RailwayCrossing V1
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
EnvTrackTask2 setting period to create new trains Receive the new new period (perToCreTrain). Set creationMode to period. 
EnvTrackTask3 propagation the change of newSignalState to all trains If signalState changes by receiving newSignalState from sig1, propagate the new value by sending newSignalState with the new state. 
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). 
EnvTrackTask5 setting type of creation Mode Receive setTypeOfCreMode and set the creationMode to the given value. 
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. In case of passing, set trainLoc to gate, else to signal. 
EnvTrackTask7 train leaves gate Receiving trainPassed signals that a train has left the gate. Set trainLoc to none and decrement noOfTrains
ModelName FullName Type Value Tasks Usage Description
typeOfTrack Enum (regular, fast) regular
noOfTrains Integer 0
perToCreTrain Duration ???
signalState Enum (go, stop) stop
creationMode Enum (period, event) period
trainLoc train location Enum (gate, signal, none) none
ModelName FullName Parameters Tasks Usage Description
RequestNo Type Method Tester Description Transferred Corrector Corrected