Points are operated by pressing the + or−button next to the points section of the operators panel, as described in section2.5.1.3. The interlocking system will
7.2 Points Behaviour 111
register the button press and switch the point if it is safe to do so. This logic is implemented in the circuitry of the interlocking system and is documented by circuit diagrams.
This means that the correct way to implement the behaviour is to always allow the operator to press the buttons and then let the interlocking system sort out whether to move the points or not. Kjær and Le Bliguet [2, p. 119] chose to introduce a model abstraction from the real point control, since the hardware implementation of the point control was too complex to implement in the internal system. Instead they supplied some hand made rules to simulate the logic for Stenstrup station. The provided rules for points behaviour allows the model checker to switch the points without simulating button presses on the operators panel.
Recall the point states described in section 2.1.1.1, points can be in a minus position, a plus position or an intermediate position. The intermediate position is a state when the points are in the act of changing from plus to minus or vice versa.
Thus there are four rules for each points section. Consider the point machineP the general form is the following.
[ plusToIntermediateP ]
where Q is a boolean expression that requires no train routes that involvesP are locked and that the points section associated withP is free. The internal system ensures that if Q is false the point cannot change i.e. if any of the locking relays are dropped which involves P or the associated point section is occupied, then
112 Behavioural Model of Buttons and Points
the point is not allowed to change position. Figure7.1shows the transition rules for the point machine behaviour of P.
Intermediate
Figure 7.1: Transition system of point P.
Example Let us consider the point machine 01 on Stenstrup station. Using the pattern for rules of point behaviour shown above we will start by requiring that the system needs to be idle, since this is an external event. Recall that Q requires that the points section associated withP must be free, which is part of the no derailing safety rule, dictating that the points must not be operated while occupied. Therefore it is required that the section is vacant, i.e. the track relay variablet01 is true. Notice that the name isoperatePoint01, since the rule by now is general enough to be any of the four rules.
[ operatePoint01 ] idle∧t01∧. . .−→
idle0 =false, . . .
Additionally Q requires that no route involving P is locked, which means the switch must not be operated while a route that covers it is locked, i.e. route locking relays ia, ib and ua must not be locked. If a route is locked, then the corresponding route locking relay will be dropped.
[ operatePoint01 ]
idle∧t01∧ia∧ib ∧ua∧. . .−→
idle0 =false, . . .
By now the rule is generic for any of the four cases of the point behaviour, hence the name is stilloperatePoint01. The key difference between these rules are which position the point currently are in and which position to switch to. Let us consider point 01 locked in plus position changing to intermediate. Switching from a locked position, the points relay must drop, hence plus01 is set to false.
7.2 Points Behaviour 113
[ plusToIntermediateP ]
idle∧t01∧ia∧ib∧ua ∧plus01−→
idle0=false, plus010 =false
The other case is when switching from the intermediate position to a locked position, both points relays must first be dropped before one of them are drawn, i.e. locked into a position. This case the point position is intermediate locking into plus.
[ intermediateToPlusP ]
idle∧t01∧ia∧ib∧ua ∧ ∼plus01∧ ∼minus01−→
idle0=false, plus010 =true
To account for the behaviour of point P, rules must exist for the minus position as well. Below are all the rules that constitutes for point 01 for Stenstrup station.
The rules for point machine 02 will not be shown, since they are made in a similar fashion.
114 Behavioural Model of Buttons and Points
C h a p t e r 8
Associations
This chapter will introduce two structures, both of which relates entities in the station documentation to variables in the model. A human may guess that the boolean variable plus01 is the point detection relay for the plus position of a points section, but it is a difficult task for a computer program.
It would be desirable to have a direct mapping between the physical elements of the station and the relays that observe them in terms of naming conventions.
Unfortunately, this is not the case. In many cases one could derive the name of the relays from the name of the element, but this is not generally true. For example, the point machine 02 is not located on track section02 (happens to a linear), but is located on points section 03.
Section 8.1 introduces the object relay association, which is a collection of associations between physical objects (and train routes) and the variables that models relays in the internal system.
Section 8.2 introduces train movement association, which is a collection of associations between the track sections and the variables introduced by the model of train movements.
116 Associations
8.1 Object Relay Associations
Object relation associations are associations between physical objects (and train routes) and relay variable that models them, e.g. for Stenstrup, the track relay of track section 01 is modelled by the boolean variable t01.
type
ObjectRelayAssociations ::
routeRelayAssoc : TrainRouteId →m VarId trackRelayAssoc : TrackId →m VarId
pointRelayAssoc : PointMachineId×Branch →m VarId signalRelayAssoc : SignalId×Lamp →m VarId
where we consider only the green and red lamp.
type
Lamp == gr| re
8.1.1 Well-formedness of Object Relay Associations
The object relay association is formed if each of its components are well-formed and no relay variable is shared between the associations, e.g. the same relay cannot be used both as a train route locking relay and as a point detection relay.
value
isWfObjectRelayAssociations : Diagram×TrainRouteTable× ObjectRelayAssociations→Bool
isWfObjectRelayAssociations(d, trt, ora) ≡ noRelayVariableOverlap(ora) ∧
isWfRouteAssoc(trt, ora)∧ isWfTrackAssoc(d, ora) ∧ isWfPointAssoc(d, ora) ∧ isWfSignalAssoc(d, ora)
No relay variable is pointed to in more than one of the association maps.
8.1 Object Relay Associations 117
value
noRelayVariableOverlap : ObjectRelayAssociations→Bool noRelayVariableOverlap(ora)≡
letrouteVars =rngrouteRelayAssoc(ora), trackVars =rngtrackRelayAssoc(ora), pointVars =rngpointRelayAssoc(ora), signalVars =rng signalRelayAssoc(ora) inrouteVars∩trackVars ={} ∧
routeVars∩pointVars ={} ∧ routeVars∩signalVars = {} ∧ trackVars ∩pointVars ={} ∧ trackVars ∩signalVars ={} ∧ pointVars∩signalVars = {}
end
8.1.1.1 Well-formedness of Route Associations
The train route association map is well-formed if the map has the same domain has the train route table, i.e. all the train routes.
value
isWfRouteAssoc : TrainRouteTable× ObjectRelayAssociations→Bool isWfRouteAssoc(trt, ora)≡
domrouteRelayAssoc(ora) = domtrt
8.1.1.2 Well-formedness of Track Associations
The track section association map is well-formed if the map has exactly all of the track sections of the station in its domain.
value
isWfTrackAssoc : Diagram×ObjectRelayAssociations→Bool isWfTrackAssoc(d, ora)≡
letallTrackSections = allLinears(d)∪allPoints(d) in domtrackRelayAssoc(ora) = allTrackSections end
118 Associations
8.1.1.3 Well-formedness of Point Machine Associations
The point machine association map is well-formed if:
1. Every point machine on the station is part of the association and every point machine in the association exists on the station.
2. The same relay may not appear in the association twice.
value
isWfPointAssoc : Diagram×ObjectRelayAssociations→Bool isWfPointAssoc(d, ora) ≡
existingPointMachines(d, ora)∧ differentPointRelays(ora)
1. Existing Point Machines The point machines in the association must exist on the station and vice versa.
value
existingPointMachines : Diagram× ObjectRelayAssociations→Bool existingPointMachines(d, ora)≡
(∀ (pmId, b) : PointMachineId×Branch• (pmId, b)∈dom pointRelayAssoc(ora)⇒
pmId ∈dompointMachineTrack(d) )∧
(∀ pmId : PointMachineId•
pmId∈dom pointMachineTrack(d)⇒
(∃(pmId0, b) : PointMachineId×Branch• (pmId0, b)∈dom pointRelayAssoc(ora)∧ pmId = pmId0)
)
2. Each relay in the association, must only appear once The same relay may not be used to lock different points or the same point in different positions.
8.1 Object Relay Associations 119
value
differentPointRelays : ObjectRelayAssociations→Bool differentPointRelays(ora)≡
(∀(pmId, b) : PointMachineId×Branch• (pmId, b)∈dompointRelayAssoc(ora)⇒
∼(∃(pmId0, b0) : PointMachineId×Branch• (pmId0, b0)∈dom pointRelayAssoc(ora)∧ (pmId, b)6= (pmId0, b0)∧
pointRelayAssoc(ora)(pmId, b) = pointRelayAssoc(ora)(pmId0, b0) )
)
8.1.1.4 Well-formedness of Signal Associations
The signal association map is well-formed if:
1. Every signal on the station is part of the association and every signal in the association exists on the station.
2. The same relay may not appear in the association twice.
value
isWfSignalAssoc : Diagram×ObjectRelayAssociations→Bool isWfSignalAssoc(d, ora)≡
existingSignals(d, ora)∧ differentLampRelays(ora)
1. Existing signals The signals in the association must exist on the station and vice versa.
value
existingSignals : Diagram×
ObjectRelayAssociations→Bool existingSignals(d, ora)≡
(∀(sId, l) : SignalId×Lamp•
(sId, l) ∈domsignalRelayAssoc(ora)⇒
120 Associations
sId∈allSignals(d) )∧
(∀ sId : SignalId• sId∈allSignals(d) ⇒
(∃(sId0, l) : SignalId ×Lamp•
(sId0, l)∈dom signalRelayAssoc(ora)∧ sId = sId0)
)
2. Each relay in the association, must only appear once The same relay may not be used to control different lamps.
value
differentLampRelays : ObjectRelayAssociations→Bool differentLampRelays(ora)≡
(∀ (sId, l) : SignalId×Lamp•
(sId, l)∈dom signalRelayAssoc(ora)⇒
∼(∃(sId0, l0) : SignalId×Lamp•
(sId0, l0)∈domsignalRelayAssoc(ora)∧ (sId, l)6= (sId0, l0)∧
signalRelayAssoc(ora)(sId, l) = signalRelayAssoc(ora)(sId0, l0) )
)