ObjectType
Document
DocName Project Version FullName ShortDescription
TrackCtrl RailwayCrossing V1
 
Description
 
Components
ModelName Number Type
ts 2 TrainSensCtrl
sig 1 SignalCtrl
 
Tasks
ModelName Description Strategy StrategyType Tasks Usage RealizedRequirement
TrackCtrlTask1 set signal to given value asap If setSignalState (go) is received, and curTrainNo is not 0, set the signal to go (setSignalState (go) to sig1).
If setSignalState (halt) is received, set the signal to halt (setSignalState (halt) to sig1), iff curTrainNo is 0.
f
TrackCtrlTask2 count no of trains If newTrain from ts1 is received, increment curTrainNo by 1, if it is received from ts2, decrement curTrainNo. f
TrackCtrlTask3 propagate newSignalState If newSignalState is received, propagate it and change curSigState to the appropiate value. f
 
Attributes
ModelName FullName Type Value Description
curTrainNo Integer 0
curSigState SignalStateType = Enum (go, halt) halt
 
Signals
ModelName FullName Parameters Tasks Usage Description SignalPaths
setSignalState SignalStateType
newSignalState SignalStateType
newTrain CharString