ObjectType
Document
| DocName |
Project |
Version |
FullName |
ShortDescription |
| EnvTrack |
RailwayCrossing |
V7 |
|
|
|
Description
| 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. |
|
Components
| ModelName |
Number |
Type |
| ts |
2 |
EnvTrainSens |
| sig |
1 |
EnvSignal |
| trains |
n |
EnvTrain |
|
Tasks
| 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 |
|
|
Attributes
| 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 |
|
|
Signals
| 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:
Sender |
|
| newTrain |
|
CharString |
EnvTrackTask7, EnvTrackTask8 |
p |
Parameters:
Receiver |
|
| initTrack |
|
xxx |
EnvTrackTask9 |
c |
xxx |
|
|