The external behaviour

Now that the internal behaviour of the interlocking system of Stentrup Station is described by a transition system, external behaviour has to be added, following the patterns introduced in section 7.1. There are three categories of external behaviour that need to be added: one for track relays, one for buttons, and one for points. This will be described in further details in the following sections.

The resulting transition systems can be found on the attached CD (see appendix C.4.2).

8.2.2.1 The track relays

As mentioned in section 7.1.1 there are two ways of modelling track relay be-haviour: random track relay behaviour and ordered track relay behaviour. The following will explain how these are formulated for Stenstrup Station:

Random track relay behaviour The behaviour will be formulated by in-stantiating the patterns given in section 7.1.1.1, page 109.

At Stenstrup, there are 6 track sections: A12, B12,01, 02, 03, and04. When using a random track relay behaviour, each relay linked to these track sections will be ruled by one transition rule that can be taken each time the system is idle.

8.2 The behaviour of Stenstrup station 143

From Odense From Svendborg Both directions

a12 fwd b12 back t02 fwd back

a12 t01 fwd b12 t03 back t04 fwd back

t01 fwd t03 back

t01 t02 fwd t03 t02 back t01 t04 fwd t03 t04 back t02 t03 fwd t02 t01 back t04 t03 fwd t04 t01 back

t03 fwd t01 back

t03 b12 fwd t01 a12 back

b12 fwd a12 back

Table 8.3: Position variables for Stenstrup

For example, as track sectionA12 is linked to relaya12, the transition rule for changing the state of the relay is:

[ randomA12 ] ∼idle→idle⁰=false, a12⁰ =∼a12

Ordered track relay behaviour The behaviour will be formulated by in-stantiating the patterns given in section 7.1.1.2, page 110.

Position variables are needed to represent the trains on the track. As previously explained, we assume that a train can at most occupy two track sections at a time. Due to this assumption, a train position will define a direction and the occupation of either a single track or two neighbour tracks.

The only exception is train positions for track sections02 and04. When trains occupy these, they are allowed to change direction. E.g. they can arrive from Odense, move to track section 02, stop, and leave the station towards Odense.

Therefore, there is no need to have a direction for trains when they are on these track sections.

All the position variables necessary to describe an ordered track relay behaviour for Stenstrup can be found in table 8.3. All these variables are initialized to false because there is no train at the station in thenormal state of the interlocking system. In order to allow trains to enter and to exit the station, transition rules are added. Examples of the formulated transition rules for train movements are:

• For a train to enter the station:

8.2 The behaviour of Stenstrup station 144

When entering from Odense, the train has to wait for signalAto become green. When it is green, track sectionA12 becomes occupied (i.e. track relaya12 is dropped) and the position variablea12 fwd is set to true.

[ insertTrainA ] idle∧aGreen→

idle⁰ =false, a12 fwd⁰=true, a12⁰=false

There is a similar rule for entering the station from Svendborg.

• For a train to occupy the next track section:

When a train is on A12 and coming from Odense, the next step is to move to track section 01. After the transition is taken, track section 01 will become occupied,a12 fwdwill be set to false anda12 t01 fwd to true.

[ a12Fwd ]

• For a train to leave a track section:

When a train is on A12 and 01 and coming from Odense, the next step is to leave track sectionA12. After this transition, track sectionA12 will become free,a12 t01fwd will be set to false andt01 fwdwill be set to true.

[ a12t01Fwd ]

Stenstrup is using the old point convention described in section 2.2.1.2.

When a train is on a point, the next track section that will be occupied by the train will depend on the position of the point. If a train is on track section01 coming from Odense (t01 fwd = true), there are two possible transition rules:

– if point01 is in the plus position

8.2 The behaviour of Stenstrup station 145

– if point01 is in the minus position [ t01minusFwd ]

This section will instantiate the patterns for point behaviour given in section 7.1.2, page 118.

As previously mentioned, Stenstrup has two points, 01 and 02. As seen in section 7.1.2, each point has three positions: plus, intermediate and minus.

Two relays are linked to each point. The position of a point is detected by these relays. For example, point01 is linked to relayplus01 that is only drawn when the point is in the plus position and to relayminus01 that is only drawn when the point is in the minus position. So point01 is in:

• the plus position ifplus01 is up andminus01 is dropped,

• the minus position ifplus01 is down andminus01 is drawn,

• the intermediate position if bothplus01 andminus01 are dropped.

A point can only be changed when no train route containing it is locked and when it is free (see section 7.1.2). For point01, three couples of train routes use it. Whether they are locked is shown by the state of three steel core relays ia, ib andua. The occupation of the point is shown by relayt01. The interlocking system has to be in an idle state when changing a point. The transition rules for point01 will be on the following form:

idle∧ia∧ib ∧ua∧t01∧... →...

8.2 The behaviour of Stenstrup station 146

For each point there are four transition rules for switching it from intermediate to plus, intermediate to minus, plus to intermediate, and minus to intermediate.

The state of the point is part of the transition guard and, when the transition is taken, all the point relays are updated to their new value. The following is an example of the transition rule for switching point 01 from its intermediate position to its plus position:

[ intermediateToPlus1 ]

idle∧ia∧ib ∧ua∧t01∧ ∼plus01∧ ∼minus01 → idle⁰=false, plus01⁰=true

8.2.2.3 The buttons

This section will instantiate the patterns for button behaviour given in section 7.1.2, page 118.

At Stenstrup, there are 4 buttons that initiate the locking of train routes. As decided in section 7.1.3, only one button can be pushed at a time, and once all the internal consequences of pushing a button have occurred, the button is released. Then, when all the consequences of this release are finished, the system is idle.

The following has to be added to the transition system in order to include the proper button behaviour:

• one transition rule for each button to push it. Here is the transition rule for the buttonb00406:

[ pushButton b00406 ]

idle→idle⁰=false, b00406⁰=true

• theidle transition rule is changed to:

[ setIdle ] gIdle→

idle⁰ =∼(b00406 ∨b00606∨b03106∨b03306), b00406⁰=false,

b00606⁰=false, b03106⁰=false, b03306⁰=false