DocName Project Version FullName ShortDescription
TrackCtrl RailwayCrossing V2
ModelName Number Type
ts 2 TrainSensCtrl
sig 1 SignalCtrl
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.
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 a new signal state After sending setSignalState to sig1, propagate the new signal state (newSignalState). Change curMode to the appropiate value. f
TrackCtrlTask4 Initialziation After creation, switch curMode to init and ask for current signalState (getSignalState). After receiving newSignalState, switch curMode to the given value. f
ModelName FullName Type Value Tasks Usage Description
curTrainNo Integer 0 TrackCtrlTask1 r
TrackCtrlTask2 w
curMode Enum (init, go, halt) init TrackCtrlTask3, TrackCtrlTask4 w
ModelName FullName Parameters Tasks Usage Description SignalPaths
setSignalState CharString, SignalStateType TrackCtrlTask1 p/c
newSignalState CharString, SignalStateType TrackCtrlTask3 p
TrackCtrlTask4 c SignalCtrlTask2:sig1:SignalCtrl/
*=$1 > $2/$1
getSignalState CharString, SignalStateType TrackCtrlTask4 p (TrackCtrlTask4:*:TrackCtrl)=$2/
*=$1 > 
newTrain CharString TrackCtrlTask2 c TrainSensCtrlTask1:ts[1,2]:TrainSensCtrl/
*=$1 > $2/$1