The notion of paths in diagrams

Most of the focus will be on the circuits of the relay diagrams. Rules will be introduced for drawing and dropping relays, but general rules for how the external world behaves (e.g. when buttons can be pushed and track relays can be occupied) will not be introduced in this chapter. Only the problems related to interactions with buttons and track sections will be discussed. Patterns for external behaviour are described in chapter 7.

The following main sections are included in this chapter:

• Section 6.1 will explain how paths can be used to decide whether a relay can be dropped or drawn.

• Section 6.2 will discuss two different approaches for making a transition system that models the behaviour of an interlocking system. It will be decided to generate specific transition systems based on specific StaticIn-terlockingSystemsinstead of making a general transition system that could be used for everyStaticInterlockingSystem.

• Section 6.3 will deduce formal conditions for when a single relay can be dropped or drawn.

• Section 6.4 will give an informal discussion of problems related to the chosen model in section 6.2. Confidence conditions will be introduced for proving that the problems do not exist for a specific transition system.

• Section 6.5 will give an informal discussion of problems related to mod-elling interactions between interlocking systems and the external world.

Further confidence conditions will be introduced.

• Section 6.6 will, based on the discussions in sections 6.2, 6.3, 6.4, and 6.5, give a formal description of how a transition system that describes the behaviour of aStaticInterlockingSystem can be generated.

• Section 6.7 will, based on the discussions in sections 6.4 and 6.5, give a formal description of how to generate the confidence conditions that must be verified in order to know if the generated transition system is sound.

6.1 The notion of paths in diagrams

Diagrams are, as previously mentioned in section 2.6, snapshots of interlocking systems in the normal state. When modelling the behaviour of an interlocking system, the model is no longer static and will be able to enter different states.

6.1 The notion of paths in diagrams 64

This section will informally describe how to decide when a relay of a diagram is allowed to change its state based on the current state of the interlocking system.

In order to decide whether a given relay can be dropped or drawn, it is necessary to introduce a way to decide whether there is current through a given part of the circuit. As explained in section 5.1, it is assumed that the modelled diagrams do not use resistance for shunting down relays. With that assumption in mind, it is possible to use the concept of a path to decide whether there is current through a relay.

In this context, apath can be considered as a list ofIdsrepresenting components contained by a givenDiagram such that:

• its first element is the positive pole of theDiagram.

• its last element is the negative pole of theDiagram.

• path(1) is neighbour with path(2), path(2) is neighbour with path(3),..., path(n-1) is neighbour with path(n), where n is the length of the path.

In principle, there can be an unlimited number of paths in aDiagram. Therefore, it is decided only to consider simple paths, i.e. paths without repetition of elements in a Diagram. From now on, when referring to a path, we mean a simple path without repetition of elements.

Figure 6.1: A diagram with two simple paths from plus to minus. The paths are indicated by the dotted lines.

6.1 The notion of paths in diagrams 65

6.1.1 The notion of conductive paths

Having a path containing a given regular relay is not enough to know whether the relay should be drawn or dropped. To know that, one needs to know if there is current propagating through the path.

Current will propagate through all the components of a path if and only if all the contacts inside the path are closed and all the buttons inside the path are pushed. From now on, we will refer to a path as beingconductive if and only if current propagates through the path.

If there is a regular relay inside a conductive path, the relay can be drawn in the next state. On the contrary, if no conductive path goes through a regular relay, it can be dropped in the next state.

Whether a path is conductive or not will depend on the state of the interlocking system. Therefore, for each state of the interlocking system, one should consider every path through a given regular relay in order to decide whether it can be dropped or drawn in the next state of the system. For instance, in the diagram shown in figure 6.1, no path is conductive because the contact ruled by relayA1 is closed and buttonB1 is released. However, ifA1 is drawn orB1 is pushed at some point, there is a conductive path through relayRR1 and it can be drawn.

6.1.2 Paths containing steel core relays

Recall section 5.2.2.3 that explains how extra observer functions have been added to the abstract model for providing information on steel core relays.

As explained in the same section, even though a steel core relay has three neighbours, current cannot pass through it to all its neighbours. Current can pass through a steel core relay from the neighbour given by the upRelation observer function to the neighbour given by minusRelation. Also, current can pass through a steel core relay from the neighbour given by downRelation to the neighbour given byminusRelation. However, current cannot pass through a steel core relay between the neighbours given byupRelation anddownRelation.

This implies that some of the paths through a steel core relay cannot be conduc-tive by definition. From now on, such paths will be considered as being illegal.

Figure 6.2 shows a part of an impossible path through a steel core relay from uptodown. Current cannot go this way and the paths containing this sequence of components should never be considered.

6.2 Different approaches to a behavioural semantics of relay diagrams 66

Figure 6.2: A part of an illegal path through a steel core relay that is indicated by the dotted line.

Figure 6.3 shows two parts of legal paths through a steel core relay. A steel core relay can then be drawn in the next state if there is a conductive path through it that contains both its neighbour given byupRelation andminusRelation. In the same way, a steel core relay can be dropped in the next state if there is a conductive path through it that contains its neighbours given by downRelation andminusRelation. If there is no conductive path through a steel core relay, the steel core relay should keep its current state in the next state of the interlocking system.

Figure 6.3: Two parts of legal paths through a steel core relay. The paths are indicated by the dotted lines.

6.2 Different approaches to a behavioural