Skip to Content

Wiki source code of Basic design

Version 17.1 by sna on 2014/08/13 02:54
Hide last authors
nbw 4.1 1
2
3 {{toc/}}
4
nbw 1.1 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
nbw 3.1 11 **For each block** we generate one mutex controller, similar to the following pattern.
nbw 1.1 12
13 [[image:attach:Mutex.png]]
14
nbw 3.1 15 **For each controlled train** one state and the corresponding transitions are added.
nbw 1.1 16
nbw 6.1 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.
csp 9.1 19 After leaving a segment the train **must** remove its request by setting <segment>_req[trainNum] to false again.
nbw 6.1 20
csp 9.1 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.
nbw 1.1 22
nbw 3.1 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.**
nbw 1.1 24
25 === Kicking Horse Pass ===
26
nbw 3.1 27 To prevent collisions on the track, a special controller manages the rights to enter or leave the Kicking Horse Pass.
nbw 1.1 28
29 [[image:attach:Mutex_KH.png]]
30
nbw 3.1 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"]]
nbw 1.1 32
csp 9.1 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.
nbw 3.1 34
35 == Train controller ==
36
krat 14.1 37 Each train controller is set in a separate region with a referenced state. This state has the following interface:
nbw 3.1 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
krat 14.1 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.
nbw 3.1 45
sna 17.1 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
nbw 3.1 188 == Station-2-Station controller ==
189
krat 14.1 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.
nbw 3.1 191
krat 14.1 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.
nbw 4.1 193
194 [[image:attach:ICIC.png]]
195
nbw 5.1 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.
sna 10.1 199
sna 15.1 200 === Structure  ===
sna 10.1 201
sna 15.1 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 " {
sna 10.1 207
sna 15.1 208 // Set of permission variables for required tracks
209 input int *_perm;
sna 10.1 210
sna 15.1 211 // Set of request variables for required tracks for 11 trains
212 output bool *_req[11];
sna 10.1 213
sna 15.1 214 // Train number
215 input int trainNum;
sna 10.1 216
sna 15.1 217 // Number of the departure track in a station
218 input int depTrack;
sna 10.1 219
sna 15.1 220 // Number of the destination track in a station
221 input int destTrack;
sna 10.1 222
sna 15.1 223 // Cleanup flag for selecting the destination track
224 input bool cleanup;
sna 10.1 225
sna 15.1 226 // Debug flag for additional output
227 input bool debug;
sna 10.1 228
sna 15.1 229 // Arrival track
230 output int arrTrack;
sna 10.1 231
sna 15.1 232 // Variable with value for arrTrack for selecting correct station elements
233 int i_arrOnTrack;
sna 10.1 234
sna 15.1 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] ... )';
sna 10.1 239
sna 15.1 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);
sna 10.1 249
sna 15.1 250 // State for waiting an additional tick when not all permissions are received
251 state backOff
252 --> backOff1;
sna 10.1 253
sna 15.1 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;
sna 10.1 261
sna 15.1 262 final state gotPerm;
263 }
264 // Transition to the departure state
265 >-> Dep_*_ST;
sna 10.1 266
sna 15.1 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)';
sna 10.1 280
281
282
sna 15.1 283 // .....................................................................................
284 // Set of track segment controlling states such as follows
285 // .....................................................................................
sna 10.1 286
sna 15.1 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;
sna 10.1 298
sna 15.1 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)';
sna 10.1 306
sna 15.1 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;
sna 10.1 317
sna 15.1 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;
sna 10.1 325
sna 15.1 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 };
sna 10.1 335
sna 15.1 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)';
sna 10.1 341
sna 15.1 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;
sna 10.1 352
sna 15.1 353 state *_LN_0_*_LN_1
354 // Transition to next track segment, if contact is triggered
355 --> *_LN_1 with 'railContact(*_LN_1,0)';
sna 10.1 356
sna 15.1 357 // ..................................................................................
sna 10.1 358
359
360
sna 15.1 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)';
sna 10.1 367
sna 15.1 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)';
sna 10.1 374
sna 15.1 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;
sna 10.1 381
sna 15.1 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;
sna 10.1 387
sna 15.1 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 };
sna 10.1 396
sna 15.1 397 // Region for handling cleanup-functionalities such as above
398 region Cleanup:
399 initial state Entry
400 --> cleanup with 'railContact(*_LN_5,0)';
sna 10.1 401
sna 15.1 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 };
sna 10.1 407
sna 15.1 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;
sna 10.1 427
sna 15.1 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;
sna 10.1 441
sna 15.1 442 // State for waiting an additional tick
443 state success
444 --> success1;
sna 10.1 445
sna 15.1 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;
sna 10.1 456
sna 15.1 457 // State waiting for station entry
458 state *_LN_5_*_ST
459 --> Arr_*_ST with i_arrOnTrack == 1 & 'railContact(*_ST_1,0)'
sna 16.1 460  --> Arr_*_ST with i_arrOnTrack == 2 & 'railContact(*_ST_2,0)'
sna 15.1 461 --> Arr_*_ST with i_arrOnTrack == 3 & 'railContact(*_ST_3,0)';
sna 10.1 462
sna 15.1 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;
sna 10.1 473
sna 15.1 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)';
sna 10.1 478
sna 15.1 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)';
sna 10.1 488
sna 15.1 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;
sna 10.1 502
sna 15.1 503 state done
504 // Transition to final state, if timer is ready
505 --> reallyDone with 'railDeparture(trainNum)';
sna 10.1 506
sna 15.1 507 final state reallyDone;
508 }
509 {{/code}}