16.5 Dynamics
16.5.3 Updating the physical system
The physical system(theDynamics module) periodically receives a notification to update its state. We say that the physical system is ticked. This is done by calling the tick function stating how much time has passed since last up-date. Using this tick value the physical system calculates the new state of points, crossings and trains according to the algorithm and some physical laws concerning movement of the train. The specification of the tick function looks like:
value
tick : T.Tick×S.Configuration×State→∼ State tick(tick,con,s)≡
let
s = tickPoints(tick,con,s), s = tickCrossings(tick,con,s), s = tickTrains(tick,con,s) in
s end
16.5 Dynamics 125
The tick function just ticks every point, crossing and train after each other.
Below these three functions are described.
Ticking points
ThetickPointsfinds all the point IDs (SB IDs for point SBs) and then calls the pointProcess function with the set of the point IDs as parameter.
value
tickPoints : T.Tick×S.Configuration×State→∼ State tickPoints(tick,con,s)≡
let
points ={p|p : T.SBID•S.getSBType(p,con) = T.POINTSB} in
pointProcess(points,tick,con,s) end
The pointProcess method handles one point at the time. It takes a point ID from the set of point IDs and uses this as argument to theupdatePointfunction.
After updatePoint has been executed pointProcess calls itself recursively after removing the mentioned point ID from the set of point IDs. The function terminates when all point IDs have been processed, i.e. when the set of point IDs is empty.
updatePoint finds the new position of the point. If the point is moving either up or down respectively the point either remains the same or switches up or down respectively. This simulates that it takes some amount of time to switch a point. When the model is made concrete point ticks are introduced which specifies how many seconds it takes to switch the point.
The states of a point are modelled as a state machine in figure 9.4 in section 9.5.
value
pointProcess : T.SBID-set×T.Tick×S.Configuration×State→∼ State pointProcess(points,tick,con,s)≡
if(points ={}) then
s else let
p : T.SBID•p∈points, points = points\ {p}, s = updatePoint(p,tick,con,s) in
pointProcess(points,tick,con,s) end
end
preS.sbsArePoints(points,con),
126 Initial Model
updatePoint : T.SBID×T.Tick×S.Configuration×State→∼ State updatePoint(p,tick,con,s)≡
let
pp = getPointPosition(p,s,con) in
caseppof
T.MOVINGDOWN→sdesetPointPosition(p,T.DOWN,s,con), T.MOVINGUP→sdesetPointPosition(p,T.UP,s,con),
→s end end
preS.getSBType(p,con) = T.POINTSB
Ticking crossings
ThetickCrossings finds all the crossing IDs (SB IDs for crossing SBs) and then calls thecrossingProcessfunction with the set of the crossing IDs as parameter.
value
tickCrossings : T.Tick×S.Configuration×State→∼ State tickCrossings(tick,con,s)≡
let
crossings ={c|c : T.SBID•S.getSBType(c,con) = T.CROSSINGSB} in
crossingProcess(crossings,tick,con,s) end
ThecrossingProcess function handles one crossing at the time. It takes a cross-ing ID from the set of crosscross-ing IDs and uses this as argument to the updateCross-ing function. After updateCrossing has been executed crossingProcesses calls itself recursively after removing the mentioned crossing ID from the set of cross-ing IDs. The function terminates when all crosscross-ing IDs have been processed, i.e. when the set of crossing IDs is empty.
TheupdateCrossing function handles the change in the state of a crossing that has just begun to close og to open. If the crossing is open (barriers is up and signals is off) or if the crossing is closed (barriers is down and signals is off) thenupdateCrossing does not change the state of the crossing.
The first step in opening or closing the crossing is always performed by the SB controlling the crossing when it prepares the segment the train has requested a reservation for and when the train has passed the crossing.
The first step in closing the crossing is to turn on the signals. Then after an amount of time updateCrossing sets the barriers to be moving down. This is modelled by having an internal choice between doing nothing and setting the barriers to be moving down. It simulates that the signals are turned on a while before the barriers start to move down. Likewise, if the barriers are moving
16.5 Dynamics 127
down, then after an amount of time updateCrossing sets the barriers to be down and the signals to be off. The crossing is now closed.
The first step in opening the crossing is to set the barriers to be moving up.
Then after an amount of time updateCrossing sets the barriers to be up. Now the crossing is open.
When the model is made concretecrossing ticksandsignal ticks are introduced.
They specify how many seconds it takes to close or open the barriers and how many seconds the signals are turned on before the barriers start to move down.
The states of a crossing are modelled as a state machine in figure 9.3 in section 9.4.
value
crossingProcess : T.SBID-set×T.Tick×S.Configuration×State→∼ State crossingProcess(crossings,tick,con,s)≡
if(crossings ={}) then
s else let
c : T.SBID•c∈crossings, crossings = crossings\ {c}, s = updateCrossing(c,tick,con,s) in
crossingProcess(crossings,tick,con,s) end
end
preS.sbsAreCrossings(crossings,con),
updateCrossing : T.SBID×T.Tick×S.Configuration×State→∼ State updateCrossing(cr,tick,con,s)≡
let
bp = getBarrierPosition(cr,s,con), ss = getSignalStatus(cr,s,con) in
casebpof T.UP→ (
if(ss = T.ON) then
sde
setBarrierPosition(cr,T.MOVINGDOWN,s,con) else
s end ),
T.MOVINGDOWN→ (
sde (
let
bp = setBarrierPosition(cr,T.DOWN,s,con) in
setSignalStatus(cr,T.OFF,s,con)
128 Initial Model
end ) ),
T.DOWN→s,
T.MOVINGUP→sdesetBarrierPosition(cr,T.UP,s,con) end
end
preS.getSBType(cr,con) = T.CROSSINGSB
Ticking trains
ThetickTrains finds all the train IDs and then calls thetrainProcess function with the set of the train IDs as parameter.
value
tickTrains : T.Tick×S.Configuration×State→∼ State tickTrains(tick,con,s)≡
let
trains ={t|t : T.TrainID}
in
trainProcess(trains,tick,con,s) end
ThetrainProcessmethod handles one train at the time. It takes a train ID from the set of train IDs and uses this as argument to the unspecified updateTrain function. updateTrain calculates the new position of the train from the current position, speed and acceleration.
value
trainProcess : T.TrainID-set×T.Tick×S.Configuration×State→∼ State trainProcess(trains,tick,con,s)≡
if(trains ={}) then
s else let
t : T.TrainID•t∈trains, trains = trains\ {t}, s = updateTrain(t,tick,con,s) in
trainProcess(trains,tick,con,s) end
end,
updateTrain : T.TrainID×T.Tick×S.Configuration×State→∼ State
16.5 Dynamics 129