const N=2
range T = 0..N
range ID = 1..N

DEPASSE_PAS_AB1 = C1[1],
C1[i:ID] = ( [i].entreeAB -> C1[i%N+1] ).
DEPASSE_PAS_AB2 = C2[1],
C2[i:ID] = ( [i].sortieAB -> C2[i%N+1] ).

DEPASSE_PAS_BC1 = C1[1],
C1[i:ID] = ( [i].entreeBC -> C1[i%N+1] ).
DEPASSE_PAS_BC2 = C2[1],
C2[i:ID] = ( [i].sortieBC -> C2[i%N+1] ).

DEPASSE_PAS_ABC1 = C1[1],
C1[i:ID] = ( [i].entreeABC -> C1[i%N+1] ).
DEPASSE_PAS_ABC2 = C2[1],
C2[i:ID] = ( [i].sortieABC -> C2[i%N+1] ).

||CONVOI_A = ([i:ID]:TrainA2 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
||CONVOI_B = ([i:ID]:TrainB2 || DEPASSE_PAS_AB1 || DEPASSE_PAS_AB2 ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).
||CONVOI_C = ([i:ID]:TrainC2  ||DEPASSE_PAS_BC1 || DEPASSE_PAS_BC2 || DEPASSE_PAS_ABC1 || DEPASSE_PAS_ABC2 ).

||TRAINS = (trainA:CONVOI_A || trainB: CONVOI_B || trainC: CONVOI_C).

CHEMIN_AB = CHEMIN_AB[0][0],
CHEMIN_AB[na:T][nb:T]= (
    when (nb ==0) trainA[i:ID].entreeAB -> CHEMIN_AB[na+1][nb]|
    trainA[j:ID].sortieAB -> CHEMIN_AB[na-1][nb]|
    when (na ==0) trainB[i:ID].entreeAB -> CHEMIN_AB[na][nb+1]|
    trainB[j:ID].sortieAB -> CHEMIN_AB[na][nb-1]).

CHEMIN_BC = CHEMIN_BC[0][0],
CHEMIN_BC[nb:T][nc:T]= (
    when (nc ==0) trainB[i:ID].entreeBC -> CHEMIN_BC[nb+1][nc]|
    trainB[j:ID].sortieBC -> CHEMIN_BC[nb-1][nc]|
    when (nb ==0) trainC[i:ID].entreeBC -> CHEMIN_BC[nb][nc+1]|
    trainC[j:ID].sortieBC -> CHEMIN_BC[nb][nc-1]).

CHEMIN_ABC = CHEMIN_ABC[0][0][0],
CHEMIN_ABC[na:T][nb:T][nc:T]= (
    when (nc ==0 && na ==0) trainB[i:ID].entreeABC -> CHEMIN_ABC[na][nb+1][nc]|
    trainB[j:ID].sortieABC -> CHEMIN_ABC[na][nb-1][nc]|
    when (nc ==0 && nb ==0) trainA[i:ID].entreeABC -> CHEMIN_ABC[na+1][nb][nc]|
    trainA[j:ID].sortieABC -> CHEMIN_ABC[na-1][nb][nc]|
    when (na ==0 && nb ==0) trainC[i:ID].entreeABC -> CHEMIN_ABC[na][nb][nc+1]|
    trainC[j:ID].sortieABC -> CHEMIN_ABC[na][nb][nc-1]).

||Reseau3 = ( CHEMIN_AB || CHEMIN_BC || CHEMIN_ABC || TRAINS).