Skip to Content

Wiki source code of Basic design

Version 17.1 by sna on 2014/08/13 02:54
Show last authors
1
2
3 {{toc/}}
4
5 We compose our railway controller from several train controllers, combined with controllers for mutual exclusion.
6
7 == Mutual Exclusion ==
8
9 === Normal segments ===
10
11 **For each block** we generate one mutex controller, similar to the following pattern.
12
13 [[image:attach:Mutex.png]]
14
15 **For each controlled train** one state and the corresponding transitions are added.
16
17 A train **must** signal the wish to enter a segment by setting the variable **bool <segment>_req[trainNum] **to true.
18 The right to enter a segement is given to the train by setting the variable **int <segment>_perm** to the train number.
19 After leaving a segment the train **must** remove its request by setting <segment>_req[trainNum] to false again.
20
21 For a free track the *_perm variable is set to -1 and all tracks, apart from starting positions, are initialized with -1. For the starting positions the *_perm variables are set to the corresponding train number and the *_req variable for the train is set to true.
22
23 **A train must not enter a segment or alter the settings of a segment without holding the lock for the segment. No exceptions from this rule are allowed.**
24
25 === Kicking Horse Pass ===
26
27 To prevent collisions on the track, a special controller manages the rights to enter or leave the Kicking Horse Pass.
28
29 [[image:attach:Mutex_KH.png]]
30
31 The controller splits the pass into two parts, //left// and //right//, corresponding to the track layout chart. [[(Simplified track layout)>>url:http://www.informatik.uni-kiel.de/~~railway/Downloads/kscheme.pdf||shape="rect"]]
32
33 Each part has two operational modes, //in// and //out//, being active when trains are allowed to either enter or leave the pass. When entering the pass the controller counts the entering trains and only lets two trains enter (one after the other). When leaving the pass the trains are removed from the counter, freeing space for the next train.
34
35 == Train controller ==
36
37 Each train controller is set in a separate region with a referenced state. This state has the following interface:
38
39
40 \\\\\\\\
41
42 {{{    input int *_perm;         # All permission variables (Tracks) input bool *_perm # KH permission variables   input int trainNum;    input bool cleanup; input bool debug; output bool *_req[]; # All request variables}}}
43
44 The train controller is composed of several //Station-2-Station// controllers. These are combined to form a complete schedule. Additionally, the cleanup signal has to be watched to abort the schedule and return back to the initial position.
45
46 === Structure ===
47
48 {{code linenumbers="true" language="sct"}}
49 scchart Test2b "Test of IC_JCT" {
50 bool IC_JCT_0_req[11], IC_LN_0_req[11], IC_LN_1_req[11], IC_LN_2_req[11];
51 bool IC_LN_3_req[11], IC_LN_4_req[11], IC_LN_5_req[11], IC_ST_0_req[11];
52 bool IC_ST_1_req[11], IC_ST_2_req[11], IC_ST_3_req[11], IC_ST_4_req[11];
53 bool IO_LN_0_req[11], IO_LN_1_req[11], IO_LN_2_req[11], KH_LN_0_req[11];
54 bool KH_LN_1_req[11], KH_LN_2_req[11], KH_LN_3_req[11], KH_LN_4_req[11];
55 bool KH_LN_5_req[11], KH_LN_6_req[11], KH_LN_7_req[11], KH_LN_8_req[11];
56 bool KH_ST_0_req[11], KH_ST_1_req[11], KH_ST_2_req[11], KH_ST_3_req[11];
57 bool KH_ST_4_req[11], KH_ST_5_req[11], KH_ST_6_req[11], KIO_LN_0_req[11];
58 bool KIO_LN_1_req[11], OC_JCT_0_req[11], OC_LN_0_req[11], OC_LN_1_req[11];
59 bool OC_LN_2_req[11], OC_LN_3_req[11], OC_LN_4_req[11], OC_LN_5_req[11];
60 bool OC_ST_0_req[11], OC_ST_1_req[11], OC_ST_2_req[11], OC_ST_3_req[11];
61 bool OC_ST_4_req[11], OI_LN_0_req[11], OI_LN_1_req[11], OI_LN_2_req[11];
62 bool req_in_R, req_out_R, req_in_L, req_out_L, perm_in_R, perm_out_R, perm_in_L, perm_out_L;
63 int IC_JCT_0_perm, IC_LN_0_perm, IC_LN_1_perm, IC_LN_2_perm;
64 int IC_LN_3_perm, IC_LN_4_perm, IC_LN_5_perm, IC_ST_0_perm;
65 int IC_ST_1_perm, IC_ST_2_perm, IC_ST_3_perm, IC_ST_4_perm;
66 int IO_LN_0_perm, IO_LN_1_perm, IO_LN_2_perm, KH_LN_0_perm;
67 int KH_LN_1_perm, KH_LN_2_perm, KH_LN_3_perm, KH_LN_4_perm;
68 int KH_LN_5_perm, KH_LN_6_perm, KH_LN_7_perm, KH_LN_8_perm;
69 int KH_ST_0_perm, KH_ST_1_perm, KH_ST_2_perm, KH_ST_3_perm;
70 int KH_ST_4_perm, KH_ST_5_perm, KH_ST_6_perm, KIO_LN_0_perm;
71 int KIO_LN_1_perm, OC_JCT_0_perm, OC_LN_0_perm, OC_LN_1_perm;
72 int OC_LN_2_perm, OC_LN_3_perm, OC_LN_4_perm, OC_LN_5_perm;
73 int OC_ST_0_perm, OC_ST_1_perm, OC_ST_2_perm, OC_ST_3_perm;
74 int OC_ST_4_perm, OI_LN_0_perm, OI_LN_1_perm, OI_LN_2_perm;
75
76 bool debug = false;
77 bool cleanup = false;
78 int trainCount;
79
80 const int c_EINS = 1;
81 const int c_ZWEI = 2;
82 const int c_DREI = 3;
83 const int c_VIER = 4;
84 const int c_FUENF = 5;
85
86 initial state init references initRailway11Trains
87 --> run;
88
89 state run {
90 region Mutexes:
91 initial state Mutexes references mutexRailway11Trains;
92
93 region KH_Mutexes:
94 initial state KH_Mutexes references kh_mutex;
95
96 region Train4 :
97 initial state train4 {
98
99 @alterHostcode
100 const int trainNum = 4;
101 int arrivalTrack = 3;
102
103 initial state Round references ICIC
104 bind depTrack to arrivalTrack,
105 destTrack to c_DREI,
106 arrTrack to arrivalTrack
107 >-> Choice;
108
109 state Choice
110 --> Round with !cleanup | !(arrivalTrack == 3)
111 --> Done;
112
113 final state Done;
114
115 };
116 region Train5 :
117 initial state train5 {
118
119 @alterHostcode
120 const int trainNum = 5;
121 int arrivalTrack = 2;
122
123 initial state Round references ICIC
124 bind depTrack to arrivalTrack,
125 destTrack to c_ZWEI,
126 arrTrack to arrivalTrack
127 >-> Choice;
128
129 state Choice
130 --> Round with !cleanup | !(arrivalTrack == 2)
131 --> Done;
132
133 final state Done;
134
135 };
136
137 region Train9 :
138 initial state train9 {
139
140 @alterHostcode
141 const int trainNum = 9;
142 int arrivalTrack = 1;
143
144 initial state Round references ICIC
145 bind depTrack to arrivalTrack,
146 destTrack to c_EINS,
147 arrTrack to arrivalTrack
148 >-> Choice;
149
150 state Choice
151 --> Round with !cleanup | !(arrivalTrack == 1)
152 --> Done;
153
154 final state Done;
155 };
156
157 region Train7 :
158 initial state train7 {
159
160 @alterHostcode
161 const int trainNum = 7;
162 int arrivalTrack = 1;
163
164 initial state OCtoIC references OCIC
165 bind depTrack to arrivalTrack,
166 destTrack to c_ZWEI,
167 arrTrack to arrivalTrack
168 >-> ICtoOC;
169
170 state ICtoOC references ICOC
171 bind depTrack to arrivalTrack,
172 destTrack to c_EINS,
173 arrTrack to arrivalTrack
174 >-> Choice;
175
176 state Choice
177 --> OCtoIC with !cleanup | !(arrivalTrack == 1)
178 --> Done;
179
180 final state Done;
181 };
182 };
183 }
184 {{/code}}
185
186
187
188 == Station-2-Station controller ==
189
190 Each Station-2-Station controller realizes the movement from one of the stations (IC,OC,KH) to another station. All controllers using IC or OC parts have to respect the traveling directions. For the Kicking Horse Pass two separate controllers, forwards and backwards, are used.
191
192 The controllers starting from Kicking Horse Pass Station make an assumption of the direction of the train. These are dependent on the directions of the inner or outer circle, e.g. the KHIC controller starts backwards because this is the only valid direction to travel this path. To drive a train from the Kicking Horse Station (facing forward) to the Inner Circle we have to combine the KHOC and OCIC controllers.
193
194 [[image:attach:ICIC.png]]
195
196 When arriving on a station the train controller **must** first call the function //void railArrival(int train, int station)//. This starts the waiting timer for the train.
197 Next the train **must** wait for// int railDeparture(int train)// to return 1.
198 After the waiting has finished the controller can reach a final state and pass the control back to the train controller.
199
200 === Structure  ===
201
202 {{code linenumbers="true" language="sct"}}
203 //
204 // Structure of a Station-2-Station controller from Station * to Station *
205 //
206 scchart STST " * to * Controller " {
207
208 // Set of permission variables for required tracks
209 input int *_perm;
210
211 // Set of request variables for required tracks for 11 trains
212 output bool *_req[11];
213
214 // Train number
215 input int trainNum;
216
217 // Number of the departure track in a station
218 input int depTrack;
219
220 // Number of the destination track in a station
221 input int destTrack;
222
223 // Cleanup flag for selecting the destination track
224 input bool cleanup;
225
226 // Debug flag for additional output
227 input bool debug;
228
229 // Arrival track
230 output int arrTrack;
231
232 // Variable with value for arrTrack for selecting correct station elements
233 int i_arrOnTrack;
234
235 // Handles departing from a station *
236 initial state *_ST {
237 // hostcode call for additional output when debug
238 entry debug / 'println([trainNum][ST-ST] ... )';
239
240 // State, which sets requests for needed tracks
241 initial state waitForPerm {
242 entry / *_ST_4_req[trainNum] = true;
243 entry / *_LN_0_req[trainNum] = true;
244 }
245 // Transition is taken, if all permissions are received
246 --> gotPerm with (*_ST_4_perm == trainNum) & (*_LN_0_perm == trainNum)
247 // Transition is taken, if some (not all) permissions are received
248 --> backOff with (*_ST_4_perm == trainNum) | (*_LN_0_perm == trainNum);
249
250 // State for waiting an additional tick when not all permissions are received
251 state backOff
252 --> backOff1;
253
254 // State, which releases the requests for needed tracks
255 state backOff1 {
256 entry / *_ST_4_req[trainNum] = false;
257 entry / *_LN_0_req[trainNum] = false;
258 }
259 // Transition to repeat requesting permissions procedure
260 --> waitForPerm;
261
262 final state gotPerm;
263 }
264 // Transition to the departure state
265 >-> Dep_*_ST;
266
267 // State, which handles the departure of a train
268 state Dep_*_ST {
269 // Set of entry-Actions with hostcode calls to set tracks, points and signals according to depTrack
270 entry / 'railPoint(*,STRAIGHT)';
271 entry / 'railSignal(*_LN_0, FWD, RED)';
272 entry / 'railTrack(*_LN_0,FWD,trainNum,NORMAL)';
273 entry / 'railTrack(*_ST_4,FWD,trainNum,NORMAL)';
274 entry depTrack == 1 / 'railSignal(*_ST_1, FWD, GREEN)';
275 entry depTrack == 2 / 'railSignal(*_ST_2, FWD, GREEN)';
276 entry depTrack == 3 / 'railSignal(*_ST_3, FWD, GREEN)';
277 //...
278 // Transition to next track segment, if contact is triggered
279 } --> *_LN_0 with 'railContact(*_LN_0,0)';
280
281
282
283 // .....................................................................................
284 // Set of track segment controlling states such as follows
285 // .....................................................................................
286
287 // Transition to next track segment, if contact is triggered
288 state *_LN_0 {
289 // Hostcode calls for outputs
290 entry / 'println("[trainNum][ST-ST] Entering *_LN_0")';
291 entry debug / 'println("[trainNum][ST-ST] Requesting permission for *_LN_1")';
292 // Entry-Actions with hostcode calls to set previous signal according to depTrack to RED
293 entry depTrack == 1 / 'railSignal(*_ST_1, FWD, RED)';
294 entry depTrack == 2 / 'railSignal(*_ST_2, FWD, RED)';
295 entry depTrack == 3 / 'railSignal(*_ST_3, FWD, RED)';
296 // Requesting the next track segment
297 entry / *_LN_1_req[trainNum] = true;
298
299 // Region for handling train driving
300 region Travel:
301 initial state Entry
302 // Transition to continuing state, if permitted
303 --> Continue with 'railContact(*_LN_0,0)' & (*_LN_1_perm == trainNum)
304 // Transition to slowing down else
305 --> Slowdown with 'railContact(*_LN_0,0)';
306
307 // State for slowing down the train
308 state Slowdown {
309 entry debug / 'println("[trainNum][ST-ST] Slowing down on *_LN_0")';
310 // Entry-Action with hostcode calls for slowing down the train
311 entry / 'railTrack(*_LN_0,FWD,trainNum,CAUTION)';
312 }
313 // Transition to waiting state
314 --> Waiting with 'railContact(*_LN_0,1)'
315 // Transition to continuing state, if permitted
316 --> Continue with *_LN_1_perm == trainNum;
317
318 // State for train waiting on permission
319 state Waiting {
320 entry debug / 'println("[trainNum][ST-ST] Stopping on *_LN_0")';
321 // Entry-Action with hostcode call for stopping the train
322 entry / 'railTrackBrake(*_LN_0)';
323 }
324 --> Continue with *_LN_1_perm == trainNum;
325
326 // State to continuing driving on the track
327 final state Continue {
328 entry debug / 'println("[trainNum][ST-ST] Continuing on *_LN_0")';
329 // Entry-Actions with hostcode calls to set tracks and signals for driving
330 entry / 'railSignal(*_LN_0,FWD,GREEN)';
331 entry / 'railTrack(*_LN_0,FWD,trainNum,NORMAL)';
332 entry / 'railTrack(*_LN_1,FWD,trainNum,NORMAL)';
333 entry / 'railSignal(*_LN_1, FWD, RED)';
334 };
335
336 // Region for handling cleanup functionalities
337 region Cleanup:
338 initial state Entry
339 // Transition to cleanup state
340 --> cleanup with 'railContact(*_LN_0,0)';
341
342 // State for cleaning up the previous track segments
343 final state cleanup {
344 entry debug / 'println("[trainNum][ST-ST] Entered *_LN_0 completely")';
345 // Entry-Action with hostcode call to switching off the previous track
346 entry / 'railTrackOff(*_ST_4)';
347 // Entry-Action to release the previous track
348 entry / *_ST_4_req[trainNum] = false;
349 };
350 // Transition to transitional state
351 }>-> *_LN_0_*_LN_1;
352
353 state *_LN_0_*_LN_1
354 // Transition to next track segment, if contact is triggered
355 --> *_LN_1 with 'railContact(*_LN_1,0)';
356
357 // ..................................................................................
358
359
360
361 // State for entering a station
362 state *_LN_5 {
363 // Variable for checking all needed permissions
364 int perm_all_next_segments = false;
365 entry / 'println("[trainNum][ST-ST] Entering *_LN_5")';
366 entry / 'railSignal(*_LN_4, FWD, RED)';
367
368 // Region for handling train driving such as above,
369 // only with perm_all_next_segments for permitting more than one track
370 region Travel:
371 initial state Entry
372 --> Continue with 'railContact(*_LN_5,0)' & perm_all_next_segments
373 --> Slowdown with 'railContact(*_LN_5,0)';
374
375 state Slowdown {
376 entry debug / 'println("[trainNum][ST-ST] Slowing down on *_LN_5")';
377 entry / 'railTrack(*_LN_5,FWD,trainNum,CAUTION)';
378 }
379 --> Waiting with 'railContact(*_LN_5,1)'
380 --> Continue with perm_all_next_segments;
381
382 state Waiting {
383 entry debug / 'println("[trainNum][ST-ST] Stopping on *_LN_5")';
384 entry / 'railTrackBrake(*_LN_5)';
385 }
386 --> Continue with perm_all_next_segments;
387
388 final state Continue {
389 entry debug / 'println("[trainNum][ST-ST] Continuing on *_LN_5")';
390 entry i_arrOnTrack == 1 / 'railTrack(*_ST_1,FWD,trainNum,NORMAL)';
391 entry i_arrOnTrack == 2 / 'railTrack(*_ST_2,FWD,trainNum,NORMAL)';
392 entry i_arrOnTrack == 3 / 'railTrack(*_ST_3,FWD,trainNum,NORMAL)';
393 //...
394 entry / arrTrack = i_arrOnTrack;
395 };
396
397 // Region for handling cleanup-functionalities such as above
398 region Cleanup:
399 initial state Entry
400 --> cleanup with 'railContact(*_LN_5,0)';
401
402 final state cleanup {
403 entry debug / 'println("[trainNum][ST-ST] Entered *_LN_5 completely")';
404 entry / 'railTrackOff(*_LN_4)';
405 entry / *_LN_4_req[trainNum] = false;
406 };
407
408 // Region for handling permissions of all needed tracks
409 region Permissions:
410 // State for requesting all needed tracks according to destination track and cleanup-Flag
411 initial state checking {
412 entry / *_ST_0_req[trainNum] = true;
413 entry destTrack == 1 | !cleanup / *_ST_1_req[trainNum] = true;
414 entry destTrack == 2 | !cleanup / *_ST_2_req[trainNum] = true;
415 entry destTrack == 3 | !cleanup / *_ST_3_req[trainNum] = true;
416 }
417 // Transitions for permitted tracks match wished tracks
418 --> success with destTrack == 1 & *_ST_0_perm == trainNum & *_ST_1_perm == trainNum / i_arrOnTrack = 1
419 --> success with destTrack == 2 & *_ST_0_perm == trainNum & *_ST_2_perm == trainNum / i_arrOnTrack = 2
420 --> success with destTrack == 3 & *_ST_0_perm == trainNum & *_ST_3_perm == trainNum / i_arrOnTrack = 3
421 // Transitions for permitted tracks don't match wished tracks
422 --> success with *_ST_0_perm == trainNum & *_ST_1_perm == trainNum / i_arrOnTrack = 1
423 --> success with *_ST_0_perm == trainNum & *_ST_2_perm == trainNum / i_arrOnTrack = 2
424 --> success with *_ST_0_perm == trainNum & *_ST_3_perm == trainNum / i_arrOnTrack = 3
425 // Transition for not all tracks permitted
426 --> resolving with *_ST_0_perm == trainNum | *_ST_3_perm == trainNum | *_ST_2_perm == trainNum | *_ST_1_perm == trainNum;
427
428 // State for waiting an additional tick
429 state resolving
430 --> resolving1;
431
432 // State for releasing track requests
433 state resolving1 {
434 entry / *_ST_0_req[trainNum] = false;
435 entry / *_ST_1_req[trainNum] = false;
436 entry / *_ST_2_req[trainNum] = false;
437 entry / *_ST_3_req[trainNum] = false;
438 }
439 // Transition for trying the requesting again
440 --> checking;
441
442 // State for waiting an additional tick
443 state success
444 --> success1;
445
446 // State for releasing not used track requests
447 final state success1 {
448 entry !(i_arrOnTrack == 1) / *_ST_1_req[trainNum] = false;
449 entry !(i_arrOnTrack == 2) / *_ST_2_req[trainNum] = false;
450 entry !(i_arrOnTrack == 3) / *_ST_3_req[trainNum] = false;
451 // Settting perm_all_next_segments to true
452 entry / perm_all_next_segments = true;
453 };
454 // Transition to station entry states
455 }>-> *_LN_5_*_ST;
456
457 // State waiting for station entry
458 state *_LN_5_*_ST
459 --> Arr_*_ST with i_arrOnTrack == 1 & 'railContact(*_ST_1,0)'
460  --> Arr_*_ST with i_arrOnTrack == 2 & 'railContact(*_ST_2,0)'
461 --> Arr_*_ST with i_arrOnTrack == 3 & 'railContact(*_ST_3,0)';
462
463 // State for setting tracks, points and signals according to i_arrOnTrack
464 // and releasing previous track request
465 state Arr_*_ST {
466 entry / 'railSignal(*_LN_5, FWD, RED)';
467 entry / 'railTrackOff(*_LN_5)';
468 entry / 'railTrack(*_ST_0,FWD,trainNum,SLOW)';
469 entry i_arrOnTrack == 1 / 'railTrack(*_ST_1,FWD,trainNum,SLOW)';
470 entry i_arrOnTrack == 2 / 'railTrack(*_ST_2,FWD,trainNum,SLOW)';
471 entry i_arrOnTrack == 3 / 'railTrack(*_ST_3,FWD,trainNum,SLOW)';
472 entry / *_LN_5_req[trainNum] = false;
473
474 initial state SlowEntry
475 --> Slow with i_arrOnTrack == 1 & 'railContact(*_ST_1,0)'
476 --> Slow with i_arrOnTrack == 2 & 'railContact(*_ST_2,0)'
477 --> Slow with i_arrOnTrack == 3 & 'railContact(*_ST_3,0)';
478
479 // State for switching off previous track and releasing the request
480 state Slow {
481 entry / 'railTrackOff(*_ST_0)';
482 entry / *_ST_0_req[trainNum] = false;
483 }
484 // Transitions to halt state, when train is at second contact of a track segment
485 --> Halt with i_arrOnTrack == 1 & 'railContact(*_ST_1,1)'
486 --> Halt with i_arrOnTrack == 2 & 'railContact(*_ST_2,1)'
487 --> Halt with i_arrOnTrack == 3 & 'railContact(*_ST_3,1)';
488
489
490 final state Halt {
491 // Entry-Actions for braking the train on correct track
492 entry i_arrOnTrack == 1 / 'railTrackBrake(*_ST_1)';
493 entry i_arrOnTrack == 2 / 'railTrackBrake(*_ST_2)';
494 entry i_arrOnTrack == 3 / 'railTrackBrake(*_ST_3)';
495 // Entry-Actions for waiting for timer on correct track
496 entry i_arrOnTrack == 1 / 'railArrival(trainNum, *_ST_1)';
497 entry i_arrOnTrack == 2 / 'railArrival(trainNum, *_ST_2)';
498 entry i_arrOnTrack == 3 / 'railArrival(trainNum, *_ST_3)';
499 };
500 }
501 >-> done;
502
503 state done
504 // Transition to final state, if timer is ready
505 --> reallyDone with 'railDeparture(trainNum)';
506
507 final state reallyDone;
508 }
509 {{/code}}