image/svg+xml A B C D E F G H I J K L M N R1 R3 R2 R4 R5 R10 R6 R9 R7 R8
Nr Name Value
1 GRN ?
2 LBT ?
3 OCC ?
4 TRK ?
5 frm ?
6 rdy ?
7 resbl ?
8 resrt ?
9 rsrtbl ?
Nr Name Value
1 rtbl #58:{(A|->R1),(A|->R2),...,(N|->R8),(N|->R10)}
2 lst #10:{(R1|->C),(R2|->G),...,(R9|->M),(R10|->M)}
3 nxt #10:{(R1|->{(A|->B),(B|->C),(L|->A)}),(R2|->#6:{(A|->B),(B|->D),...,(F|->G),(L|->A)}),...,(R9|->{(F|->K),(G|->F),(H|->M),(I|->H),(K|->I)}),(R10|->{(H|->M),(I|->H),(J|->I),(N|->J)})}
4 fst #10:{(R1|->L),(R2|->L),...,(R9|->G),(R10|->N)}
5 SIG {(C|->S4),(G|->S5),(L|->S1),(M|->S2),(N|->S3)}
6 rht {(B|->A),(D|->A),(F|->A),(I|->A),(J|->A)}
7 lft {(B|->B),(D|->B),(F|->B),(I|->B),(J|->B)}
8 blpt {B,D,F,I,J}
Nr Name Value
1 ROUTES {R1,R2,R3,R4,R5,...}
2 BLOCKS {A,B,C,D,E,...}
3 S {S1,S2,S3,S4,S5}
Nr Event Target State ID
1SETUP_CONSTANTS(rht={(B|->A),(D|->A),(F|->A),(I|->A),(J|->A)},lft={(B|->B),(D|->B),(F|->B),(I|->B),(J|->B)})State 0
2INITIALISATION(GRN={},LBT={},OCC={},TRK={},frm={},rdy={},resbl={},resrt={},rsrtbl={})
3route_reservation(R9)
4point_positionning(R9)
5route_reservation(R1)
6route_formation(R9)
7FRONT_MOVE_1(G)
8FRONT_MOVE_2(G)
9BACK_MOVE_2(G)
10FRONT_MOVE_2(F)
11BACK_MOVE_2(F)
12point_positionning(R1)
13FRONT_MOVE_2(K)
14BACK_MOVE_2(K)
15FRONT_MOVE_2(I)
16BACK_MOVE_2(I)
17FRONT_MOVE_2(H)
18BACK_MOVE_2(H)
19BACK_MOVE_1(M)
20route_freeing(R9)
21route_reservation(R4)
22route_formation(R1)
23FRONT_MOVE_1(L)
24FRONT_MOVE_2(L)
25point_positionning(R4)
26FRONT_MOVE_2(A)
27FRONT_MOVE_2(B)
28BACK_MOVE_2(L)
29BACK_MOVE_2(A)
30route_formation(R4)
31FRONT_MOVE_1(M)
32FRONT_MOVE_2(M)
33BACK_MOVE_2(B)
34BACK_MOVE_1(C)
35route_freeing(R1)
36FRONT_MOVE_2(H)
37BACK_MOVE_2(M)
38BACK_MOVE_2(H)
39FRONT_MOVE_2(I)
40BACK_MOVE_2(I)
41FRONT_MOVE_2(K)
42BACK_MOVE_2(K)
43FRONT_MOVE_2(F)
44BACK_MOVE_2(F)
45BACK_MOVE_1(G)
46route_freeing(R4)
Generated on 25/5/2022 at 17:23 using ProB version 1.12.0-nightly
Main specification file: train_4_POR_mch.eventb
Main VisB JSON file: train4.json (modified on 1/2/2022 at 16:37)