Abstract model of relay diagrams
5.2 Modelling diagrams
5.2 Modelling diagrams
This section will introduce an abstract RSL model of relay diagrams. Only the most important details of the model will be explained here. The whole model can be seen in appendix A together with the introduced schemes in chapter 6.
The abstractRSLmodel consists of the following schemes:
• Types. The purpose of this scheme is to represent the common types and the common auxiliary functions. The complete scheme can be found in appendix A.1, page 209.
• Diagrams. The purpose of this scheme is to describe what diagrams look like using an abstract type for a diagram and observer, auxiliary, and well-formed functions. The complete scheme can be found in appendix A.2, page 210.
• StaticInterlockingSystem. The purpose of this scheme is to describe what an interlocking system looks like using abstract types for diagrams and interlocking systems, and observer, auxiliary, and well-formed func-tions. The complete scheme can be found in appendix A.3, page 216.
In order to enable references between the schemes, the following global objects are introduced:
• T, an instance ofTypes.
• D, an instance ofDiagrams.
• SIS, an instance ofStaticInterlockingSystems.
The following sections will give a more detailed description of the mentioned RSLschemes.
5.2.1 Types
This section will explain parts of theTypes scheme that includes common ele-ments of the abstractRSLmodel. The purpose of the abstract model is not to give concrete types for the components in a diagram. Instead, an identifier for a component in aDiagramor aStaticInterlockingSystemis introduced as a sort type:
5.2 Modelling diagrams 53
type Id
For representing the state of a relay, a variant type is introduced. As seen in the following declaration, a relay can either be up or down (i.e. drawn or dropped):
type
State == up| down
Further types and functions are included in the Types scheme, but these are only relevant when extracting the behaviour of an interlocking system from a StaticInterlockingSystem. Therefore, the explanation of these functions will not be given until chapter 6.
5.2.2 Diagrams
This section will explain the Diagrams scheme that models diagrams, but not a collection of diagrams. For representing a diagram, the following sort type is introduced:
type Diagram
5.2.2.1 Identifying components
The components of a diagram are represented by values in the Id type from theTypesscheme. Observer functions are introduced in order to identify which type of component an identifier represents. Examples of such observer functions are:
value
isPlus : T.Id×Diagram→Bool, isMinus : T.Id×Diagram→Bool
5.2 Modelling diagrams 54
isPlus indicates whether a given Id is a positive pole in a given Diagram and isMinus indicates whether a given id is a negative pole in a given Diagram.
Similar observer functions of the same type are introduced in order to test whether anIdis representing a regular relay, a steel relay, a contact, a button, or a junction in a given diagram. The names of these functions areisRegularRelay, isSteelRelay,isContact,isButton, andisJunction respectively.
Junctions are not components of the real diagram circuits. However, diagrams have a general way of introducing branches. Branches in a circuit represented by a diagram are either introduced by steel core relays or by letting three wires meet. When three wires meet in a diagram, we will from now refer to this as a junction. Twojunctions can be seen in figure 5.3.
Figure 5.3: Two junctions marked by circles.
Junctions will be used in the model of the diagrams for introducing branches.
This will allow for setting up rules about the number of neighbours. For instance, one can make rules for allowing regular relays to be connected to exactly two other components in the model of a diagram. If a given relay is connected to several components inside the real diagram, one can connect this relay to a junction and then connect the junction to the other components.
A junction is only supposed to introduce one branch in a network. If one wishes to introduce several branches at the same time, several junctions can be connected in series.
As one might have noticed, there is no function for detecting whether a com-ponent is a lamp, a fuse, a resistor, or a power source that were introduced in section 2.6.1. Concerning the lamps, each of them is monitored by a relay.
Therefore, they are not needed as part of the model. If one wants to know the state of a given lamp, one can consider the relay that monitors the lamp. As
5.2 Modelling diagrams 55
we do not model electrical phenomenons like resistance, resistors, fuses, and the power sources are not included in the model.
5.2.2.2 Connecting components
As previously explained in section 2.6.1, the components in a diagram have pins that can be considered as sockets. Components are connected from pin to pin by wires. If one wants to make a model that includes all the information of the diagrams, it is necessary to model the pins.
If pins were included in the model, the components represented by Ids would be related to their pins and two components would be connected if two of their pins were connected. Such information would be needed if the components were asymmetric, e.g. if the direction of the current going through the component were important. However, most of the components of the diagrams are sym-metrical. For instance, a regular relay can be drawn if there is current through it, but where the current is coming from does not matter. The only asymmetric component is the steel core relay. Further information on it is presented in the next section.
As most components are symmetric, there is no need to include pin information in each component. It would introduce extra information to the model that is not required to extract the behaviour of interlocking systems.
Therefore, it is chosen not to include the information about pins in the definition of components. Instead, it is chosen to introduce a neighbour relation between two identifiers representing two components in a diagram:
value
areNeighbours : T.Id×T.Id×Diagram →Bool
The function tests whether the two components represented by the twoIdsare neighbours in the Diagram. If two components are neighbours, it corresponds to having a wire between them inside theDiagram. For instance, the function is supposed to return true when being applied to the identifiers of the two contacts shown in figure 5.4 and theDiagramthat contains them. The contacts in figure 5.3 are not considered as being neighbours, but they are neighbours to the junctions.
5.2 Modelling diagrams 56
Figure 5.4: Two contacts that are neighbours.
5.2.2.3 Extra steel core relay information
Most components conduct current from one neighbour to another neighbour when all the conditions for having current through the component are fulfilled (e.g if the component is a button, it has to be pushed, if it is a contact, it has to be closed, if it is a regular relay or a junction, it is always conductive).
However, as previously mentioned in section 2.5.1.2, a steel core relay cannot conduct current between all its neighbours. For instance, the steel core relay in figure 5.5 is only capable of conducting current from up to minus and down to minus, but not from up to down.
If current is conducted from up to minus, the relay will be drawn and if current is conducted from down to minus, the relay will be dropped. When no current is applied to the steel core relay, it will maintain its state.
Figure 5.5: A steel core relay with named neighbours
Therefore, the areNeighbours function is not enough for specifying how steel relays are connected to other components in a Diagram. In order to add the needed extra information, it is decided to add the following observer functions to the model:
value
upRelation : T.Id×Diagram→∼ T.Id,
5.2 Modelling diagrams 57
downRelation : T.Id×Diagram→∼ T.Id, minusRelation : T.Id×Diagram →∼ T.Id
These functions are only supposed to be applied to Ids representing steel core relays in the given Diagram. When applied to theId of a steel core relay, the functions are supposed to return an Id of a neighbour to the steel core relay in a Diagram. The functions will, respectively, give the neighbour connected to the up part, the neighbour connected to the down part, and the neighbour connected to the minus part of the steel core relay.
5.2.2.4 Representing a relay state
The state of a relay in the normal state of an interlocking system is represented in relay diagrams. Therefore, the following observer function is introduced for observing the state of a relay identified by anId in a givenDiagram:
value
relayState : T.Id×Diagram→∼ T.State
5.2.2.5 Representing contact information
As previously mentioned, diagrams contain the following information about con-tacts:
• The id of the relay that rules the contact, i.e. opens or closes it when changing state.
• The state of this relay in the normal state of the interlocking system.
• The state of the contact, i.e. open or closed in the normal state of the interlocking system.
As the state of the relay that rules the contact is already represented by the relayState function, it would be redundant to add that information. The follow-ing observer functions are enough for addfollow-ing the necessary information about contacts:
5.2 Modelling diagrams 58
value
relayIdForContact : T.Id×Diagram→∼ T.Id, relayStateForContact : T.Id×Diagram→∼ T.State
relayIdForContact will return the Id of the relay that rules the contact and relayStateForContact will return the state of the relay required for the contact to be closed. Whether the contact is open or closed can then be extracted from the model by considering the state of the relay that rules the contact.
5.2.2.6 State of buttons
As buttons are released in the normal state of an interlocking system, the state of a button is not given by any observer function. The normal state of a button is implicitlyreleased.
5.2.2.7 Well-formed diagrams
For now, diagrams have been considered, but no constraints have been intro-duced on the observer functions. From now on, we will refer to diagrams that follow the conventions used by Banedanmark as well-formed Diagrams.
The following axiomatic function is introduced for testing whether a Diagram is well-formed:
value
isWfDiagram : Diagram→Bool axiom
∀d : Diagram•isWfDiagram(d)⇒
okNeighbourRelation(d)∧okNumberOfNeighbours(d)∧ twoPoles(d)∧noIdOverlaps(d)∧
okSteelRelayRelations(d)
The axiom underspecifies the function in the sense that the defined constraints must hold for every well-formed Diagram. However, further constraints can be added when refining the specification.
okNeighbourRelation checks that:
5.2 Modelling diagrams 59
• AnId cannot be neighbour to itself.
• TheareNeighbours function is symmetric.
okNumberOfNeighbours checks that:
• A plus and a minus in aDiagramboth have at least one neighbour.
• Contacts, regular relays, and buttons have exactly 2 neighbours.
• Steel core relays and junctions have exactly 3 neighbours.
twoPoles checks that:
• There are exactly one plus and one minus in aDiagram.
Note: Real diagram can contain several positive and negative poles. This is reflected in the model by allowing an unlimited number of neighbours for a plus and a minus. Instead of adding more than one positive pole or negative pole, one can add extra neighbours to an already existing pole.
noIdOverlaps checks that:
• At most one of the observer functions isPlus, isMinus, isRegularRelay, isSteelRelay, isContact, isButton, and isJunction can be true for a given Id in a givenDiagram.
okSteelRelayRelations checks that:
• For everyId that is a steel core relay in a givenDiagram, the set of the returnedIds from upRelation, downRelation, and minusRelation applied to theId of the steel core relay is equal to the set of all the neighbours of the givenId in the given Diagram.
5.2.3 StaticInterlockingSystem
SchemeStaticInterlockingSystem is responsible for handling a collection of Di-agrams that represents a snapshot of a given interlocking system in its normal state. For representing the whole interlocking system, the following sort type is introduced:
5.2 Modelling diagrams 60
type
StaticInterlockingSystem
For getting the Diagrams of aStaticInterlockingSystem, the following observer function is introduced:
value
diagrams : StaticInterlockingSystem→D.Diagram-set
The diagrams contain relays that are part of the circuits of the interlocking system. However, some relays are not ruled by the circuits of the diagrams.
Theseexternal relays are ruled by the external world and will be used as input to the interlocking system. For instance, a track relay will be dropped when a train occupies its associated track circuit and drawn when the associated track circuit is free. In general, if a relay rules at least one contact in a diagram of an interlocking system, but does not occur in one of the diagrams of the interlocking system, it is anexternal relay.
As contacts of the external relays appear in the diagrams, it is necessary to have information about the external relays of the interlocking system. For getting the Ids of the external relays in aStaticInterlockingSystem, the following observer function is introduced:
value
externalRelayIds : StaticInterlockingSystem→T.Id-set
Because external relays can have different states in the normal state of the system, the initial state of each external relay must be specified. It is therefore decided to introduce the following observer function for determining the state of an external relay:
value
externalRelayState : T.Id×StaticInterlockingSystem→∼ T.State
5.2.3.1 Well-formed StaticInterlockingSystem
As forDiagrams, it is necessary to assume that aStaticInterlockingSystemfulfils the conventions used by Banedanmark. For checking that, an axiomatic well-formed function forStaticInterlockingSystems is introduced:
5.2 Modelling diagrams 61
value
isWfStaticInterlockingSystem : StaticInterlockingSystem→Bool axiom
∀sis : StaticInterlockingSystem• isWfStaticInterlockingSystem(sis)⇒
(∀d : D.Diagram•
d∈diagrams(sis)⇒D.isWfDiagram(d))∧ uniqueIds(sis)∧contactsHaveRelays(sis)
The axiom underspecifies the function in the sense that the defined constraints must hold for every well-formed StaticInterlockingSystem. However, further constraints can be added when refining the specification.
The quantified expression checks that:
• All theDiagrams of theStaticInterlockingSystem are well-formed.
uniqueIds checks that:
• An Id is never used more than once in the sense that two elements in the interlocking system (either in the diagrams or in the external relays) cannot have the sameId.
contactsHaveRelays checks that:
• Each contact is ruled by a relay that exists in some part of the StaticIn-terlockingSystem.
5.2.3.2 The normal state properties
As previously mentioned in section 2.6, an interlocking system has a normal state in which some specific properties are fulfilled. Checking that an interlocking system is in the normal state is closely related to modelling the behaviour of an interlocking system. Therefore, checking that the diagrams represent an interlocking system in its normal state will be treated in section 6.5.4.1.