Figure 11.2: Structure of the implementation.
text string to name the transition system. Each sub-generator is then invoked to create the transition system.
value
generate : Text×ObjectRelayAssociations× InterlockingPlan×Text-set→TransitionSystem generate(name, ora, ip, buttonIds)≡
letsld = sld(ip),
tma = genTrainMovementAssociations(sld) inmk TransitionSystem(
name,
generateStateSpace(ip, tma),
generateTransitionSystem(ora, ip, tma, buttonIds), generateAssertions(ora, ip, tma))
end
preisWfInterlockingPlan(ip)∧
isWfObjectRelayAssociations(ora, ip)
11.2 State Generator
According to our model of train movement, thecounter,connection, anddirection variables are to be generated.
All of this is stored in aTrainMovementAssociation value and is created by
plan nor can they be derived.
148 Generator
functions defined in StateGenerator.rsl, which can be found in appendix sectionE.3.3andE.2.4, respectively.
type
TrainMovementAssociations ::
connectionVars : (TrackId×TrackId) →m VarId counterVars : TrackId →m VarId
directionFwdVars : TrackId →m VarId directionBwdVars : TrackId →m VarId
directions : (TrackId ×TrackId) →m Direction
where direction is type
Direction == fwd |bwd
The generated TrainMovementAssociations are then used as input to the state generator to generate all the variables by calling the function generateStateSpace.
The preconditions requires that the interlocking plan and the train movement associations are well-formed.
value
generateStateSpace : InterlockingPlan× TrainMovementAssociations→Var-set generateStateSpace(ip, tma) ≡
genBoolVars(rngconnectionVars(tma))∪ genNatVars(rngcounterVars(tma))∪ genBoolVars(rngdirectionFwdVars(tma))∪ genBoolVars(rngdirectionBwdVars(tma)) preisWfInterlockingPlan(ip)∧
isWfTrainMovementAssociations(sld(ip), tma)
In the following sections the three types of variables will be introduced.
11.2.1 Counter Variables
Every track section has a counter which keeps track of how many trains currently occupy the section. Therefore the state generator recursively goes through every
11.2 State Generator 149
track section (except for line) and creates a name of the counter variable for it.
The name is created by prefixing “cnt ” to the name of the track section.
value
genCntVars : TrackId-set×Diagram →TrackId →m VarId genCntVars(ids, d) ≡
ifids ={}then[ ]else
letid =hdids, ids0 = ids\ {id}
in if isLine(id, d)then[ ] elsegenCntVar(id) end∪genCntVars(ids0, d) end
end,
genCntVar : TrackId→TrackId →m VarId genCntVar(id) ≡[ id7→00cnt_00 bid ]
It is then stored in a map, where the id of the track section is used as key.
value
counterVars : TrackId →m VarId
This creates anassociation between a track section and the variable.
11.2.2 Connection Variables
Every track section has a connection variable for each of its neighbours. Therefore, the generator uses the neighbour relation, introduced in section4.2.4, as it only contains one entry for each pair of neighbours. As with the counter variables theline section is disregard. The name is generated by prefixing “con ” to the identifiers of the neighbouring track section, which have been concatenated with an underscore in between.
value
genConVars : (TrackId ×TrackId)-set×Diagram → (TrackId ×TrackId) →m VarId genConVars(nbs, d) ≡
ifnbs ={}then[ ]else
150 Generator
let(nb1,nb2) =hdnbs, nbs0= nbs\ {(nb1,nb2)}
in if isLine(nb1, d)∨isLine(nb2, d) thengenConVars(nbs0, d)
elsegenConVar(nb1, nb2)∪genConVars(nbs0, d) end
end end,
genConVar : TrackId×TrackId→
(TrackId×TrackId) →m VarId genConVar(id1, id2)≡[ (id1,id2)7→00con_00b id1b
00_00b id2 ],
The ids of the connection variables are stored in a map that use the neighbouring pair of track sections as key.
value
connectionVars : (TrackId ×TrackId) →m VarId
11.2.3 Direction Variables
Recall section6.2.3, that each track section has one forward and one backward variable. They are created in a similar fashion to the counters and therefore the code will not be shown here.
The state generator creates these variables by using the principle of source and sink. Travelling away from the source (towards the sinks) are considered forward, whereas the opposite is considered backward. The source and sinks are the station borders, where trains can enter and exit the station, i.e. theline. One of these are chosen as the source while the rest are considered sinks (fig. 11.3).
A12 01 02
04
03 B12
Source Sink
Figure 11.3: Stenstrup in graph form.
11.2 State Generator 151
It is noteworthy that the model of the station only has a singleline section (fig.
11.4). Therefore it is necessary to consider it a special case. Otherwise it would act only as source and never as sink.
A12 01 02
04
03 B12
Line
Figure 11.4: Stenstrup in graph form.
The algorithm assigns the directions in the following manner. First all the neighbours of line are collected. Lets call them nb1, . . . , nbn where n is the number of neighbours toline andn≥1. Then the edge fromline tonb1is given the direction forward and the edge fromnb1to lineis marked as backward.
For the remainder, the backward direction will always be the opposite direction of the forward and will therefore not be mentioned again. For the remaining neighbours ofline, the direction from the neighbour toline is forward. In this way a single source with possible multiple sinks have been created (fig. 11.5).
A12 01 02
04
03 B12
forward Line backward
forward backward
nb1 nb2
Figure 11.5: Stenstrup in graph form.
The rest of the network is then traversed from the neighbours of the source.
Visited notes are marked so that they are not visited again. In this manner directions are given to the edges of the entire network, except for sources and sinks, which have already been visited in the first step. See figure 11.6 for a step-by-step run-though of the algorithm.
152 Generator
A12 01 02
04
03 B12
Source Sink
A12 01 02
04
03 B12
Source Sink
A12 01 02
04
03 B12
Source Sink
A12 01 02
04
03 B12
Source Sink
A12 01 02
04
03 B12
Source Sink
Step 1
Step 2
Step 3
Step 4
Step 5
Figure 11.6: Step by step demonstration of the direction generating algorithm.
11.2 State Generator 153
The result is a mapping from a neighbour pair to a direction, which can be used in creating the rules of train movement.
value
directions : (TrackId×TrackId) →m Direction
This algorithm has a weakness in that it recognises the station borders as a single line node. Consider a station that has the following station layout on figure11.7
nb2 nb1
nb4 nb3
Line Line
Figure 11.7: Station layout
The algorithm, like before, finds all neighbours to the line. In this case the line has four neighbours, nb1, nb2, nb3 and nb4.
The edge from line to nb1 gets the forward direction, and from nb1 to line gets backward. As stated earlier the algorithm then assigns all the remaining neighbours such that going from the neighbour to line is forward. Figure 11.8 shows the algorithms representation of the station.
Notice that the dotted arrows from line to nb2 and from nb2 to line. This creates inconsistency for the notion of direction, since going from line to nb2 should be forward. Figure11.9shows the forward directions and how the dotted forward direction from nb2 to line creates this inconsistency. The backward direction is ignored since it always is the opposite of forward.
As the example shows, the algorithm currently will not work when the line has more than two neighbours. However, one way of solving this is by naming the station borders uniquely. In case of Stenstrup, this could be Odense and Svendborg.
154 Generator
nb2
nb1 nb3
nb4 Line
backward
forward forward backward forward
backward forward
backward
Figure 11.8: The algorithms representation of the station layout
nb2 nb1
nb4 nb3
Line Line
forward forward
forward forward
forward forward
Figure 11.9: Station layout with directions