ObjectType
Document
| DocName |
Project |
Version |
FullName |
ShortDescription |
| EnvTrack |
RailwayCrossing |
V4 |
|
|
|
Description
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. |
|
Components
| ModelName |
Number |
Type |
| trainSens |
2 |
EnvTrainSens |
| sig |
1 |
EnvSignal |
| trains |
n |
EnvTrain |
|
Tasks
| 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 apporpiate
signals. |
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 |
|
|
Attributes
| 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 |
|
|
|
|
Signals
| 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 |
|
|
|
|
EnvTrackTask8 |
c |
|
| setPerToCreTrain |
|
Duration |
EnvTrackTask2 |
c |
|
| creNewTrain |
|
|
EnvTrackTask1 |
c |
|
| initTrain |
|
CharString, Duration, Duration, SignalStateType |
EnvTrackTask1 |
p |
|
|
ChangeRequests
| RequestNo |
Type |
Method |
Tester |
Description |
Transferred |
Corrector |
Corrected |
|
|
|
|
|
|
|
|
|