eliminates the issues of train length, and introduces no upper limit of trains. This allows the model checker to spawn unlimited trains, that the explicit modelling approach cannot. It can be arguable how many trains are needed to verify the case of Stenstrup station, but having a larger station would require more trains making the following approach more elegant.
6.2 Model of Trains
Recall the definition of trains from section 2.2. A train is rolling stock that performs a train movement, i.e. travels from one station to another.
Some of the following rules may apply for shunting movements as well, while others will not.
The following properties are true about trains:
• Occupies a minimum of one track section, with no upper limit.
• Track sections occupied must form a path, i.e. a sequence of track sections, where each track section is neighbour with the next track section in the sequence.
Instead of the limitations of modelling train movement discussed in section 6.1 we will present a model to eliminate this.
A counter variable will be introduced to indicate how many trains currently occupies a given track section, thus allowing an arbitrary number of trains. A connection variable will be introduced, allowing a train to have a length with no upper bound, and a direction variable to indicate the travelling movement.
Using solely the state of the track circuit relays, one is able to tell on which track sections trains are located2. One cannot tell how many trains are on each section, which direction they are heading or if several adjacent track sections are occupied, whether it is by a single long train or several smaller.
The variables rely on the name of the track sections. Considering Stenstrup station on figure6.1, it can be of reference point when constructing the variable names.
2assuming only trains short the track circuits, which is reasonable when model checking
90 Behavioural Model of Train Movements
A12 01 02 03 B12
04
Figure 6.1: Track Layout of Stenstrup station.
6.2.1 Counter
A counter for each track section is introduced, which counts how many trains are located on the associated track section. Shown on figure6.2each variable is prefixed withcnt followed by the name of the track section to denote a counter variable.
When a train enters a section, the counter is incremented and when a train leaves the section, the counter is decremented.
cnt_A12 : Nat
cnt_04 : Nat
cnt_B12 : Nat cnt_03 : Nat
cnt_02 : Nat cnt_01 : Nat
Figure 6.2: Relation between the track sections and the counter variables.
The initial state of Stenstrup has no trains located on the station, hence all counters are assigned with zero.
cnt A12 : Nat:= 0, cnt 01 : Nat := 0, cnt 02 : Nat := 0, cnt 04 : Nat := 0, cnt 03 : Nat := 0, cnt B12 : Nat := 0,
Example Let us consider a subset of Stenstrup station using track sections A12, 01, 02 and 04. Train A and B each occupy track section A12 and 01, and 01 and 02, respectively. Hence the counters of A12 and 02 are both one. Having both A and B occupy track section 02 the counter is two. Track section 04 is unoccupied leaving the counter to zero.
6.2 Model of Trains 91
Train B
cnt_01 = 2 cnt_02 = 1
Train A cnt_A12 = 1
cnt_04 = 0
Occupied Track Unoccupied Track
Figure 6.3: An example of trains A and B occupying track sections A12, 01 and 02 showing the counter variables.
6.2.2 Connection
A connection variable is introduced to distinguish different trains. Without a connection variable it would be hard to tell whether two occupied tracks are by two separate trains or a single train, that occupy both track sections.
This time a boolean variable is introduced for each border between track sections shown on figure 6.4. The variables are true when the same train is located on both the adjacent track sections.
Recall the neighbour relation from section4.2.4. The variables are constructed such that each pair of neighbours, excluding the line, are prefixed with con followed by a track section, followed by an underscore and the neighbouring track section.
con A12 01 : Bool:=false, con 01 02 : Bool:=false, con 01 04 : Bool:=false, con 02 03 : Bool:=false, con 03 04 : Bool:=false, con 03 B12 : Bool:=false,
con_A12_01 : Bool con_01_02 : Bool con_02_03 : Bool con_03_B12 : Bool con_01_04 : Bool con_04_03 : Bool
Figure 6.4: The connection variables are true if a single train occupy both neighbouring track sections.
92 Behavioural Model of Train Movements
Example Let us consider the same scenario on Stenstrup station in the example in section 6.2.1. Figure 6.5 shows that train A occupies section A12 and 01, hence con A12 01 is true. While train B occupies 01 and 02 hence con 01 02 is true. There is no connection between 01 and 04 leaving con 01 04 false.
Using the connection variable in conjunction with the counter variable it can be derived that there are two trains, since the counter for track section 01 is two.
Thus, one train connected with A12 and 01 and another connected with 01 and 02.
Train A
con_A12_01 = true con_01_02 = true
con_01_04 = false
Occupied Track Unoccupied Track Train B
Figure 6.5: An example of train A and B occupying track sections A12, 01 and 02 showing the connection variables.
6.2.3 Direction
The direction variable denotes the travelling movement of trains. Each track section has two direction variables prefixed with fwd andbwd followed by a track name, where fwd is short for forward and bwd is short for backward. Figure 6.6shows the complete set of direction variables for Stenstrup station.
Whenever one of the variables is true then a train on the associated track section is heading in one direction, while the other is true when a train on the same track section is heading the other way. They are false if there is no train on the section or if no train on the section is heading in the given direction.
Moving from Odense to Svendborg denotes a travelling direction of forward and moving from Svendborg to Odense is backward.
fwd A12 : Bool:=false, bwd A12 : Bool:=false