Class REGION2 is
Vars:

---------------------------------------------------------------
T0: int[] := [ 1, 9,10,13,15,20,23]; -- G1
T1: int[] := [ 3, 9,10,13,15,20,24]; -- R1
T2: int[] := [ 5,27,11,13,16,20,25]; -- Y1
T3: int[] := [ 7,27,11,13,16,20,26]; -- B1
T4: int[] := [23,22,17,18,11, 9, 2]; -- G2
T5: int[] := [24,22,17,18,11, 9, 4]; -- R2
T6: int[] := [25,22,17,18,12,27, 6]; -- Y2
T7: int[] := [26,22,17,18,12,27, 8]; -- B2
----------------------------------------------------------------
P0: int :=0;
P1: int :=0;
P2: int :=0;
P3: int :=0;
P4: int :=0;
P5: int :=0;
P6: int :=0;
P7: int :=0;
----------------------------------------------------------------

------ region A: train constraints ------
A0: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- G1
A1: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- R1
A2: int[] := [ 0, 0, 1,-1, 0, 1, 0]; -- Y1
A3: int[] := [ 0, 0, 1,-1, 0, 0, 0]; -- B1
A4: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- G2
A5: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- R2
A6: int[] := [ 0, 0, 0,-1, 0, 0, 0]; -- Y2
A7: int[] := [ 0, 1, 0,-1, 0, 0, 0]; -- B2
------------------------------------------

------- region B: train constraints ------
B0: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- G1
B1: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- R1
B2: int[] := [ 0, 0, 1,-1, 0, 0, 0]; -- Y1
B3: int[] := [ 0, 0, 1,-1, 0, 1, 0]; -- B1
B4: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- G2
B5: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- R2
B6: int[] := [ 0, 1, 0,-1, 0, 0, 0]; -- Y2
B7: int[] := [ 0, 0, 0,-1, 0, 0, 0]; -- B2
------------------------------------------


-------------------------------------------------------------
RA: int :=1;  -- initial value for region RA
RB: int :=1;  -- initial value for region RB
LA: int :=7;  -- limit value for region RA
LB: int :=7;  -- limit value for region RB
-------------------------------------------------------------------

State Top =s1

Behavior:

------------------------- train 0 -----------------------------
s1 -> s1
 {- [P0 < 6 &
     T0[P0+1] != T1[P1] &
     T0[P0+1] != T2[P2] &
     T0[P0+1] != T3[P3] &
     T0[P0+1] != T4[P4] &
     T0[P0+1] != T5[P5] &
     T0[P0+1] != T6[P6] &
     T0[P0+1] != T7[P7] &
     RA + A0[P0+1] <= LA &
     RB + B0[P0+1] <= LB] /
  P0 := P0 +1;
  RA = RA + A0[P0];
  RB = RB + B0[P0];
 }

------------------------- train 1 -----------------------------
s1 -> s1 
 {- [P1 < 6 &
     T1[P1+1] != T0[P0] &
     T1[P1+1] != T2[P2] &
     T1[P1+1] != T3[P3] &
     T1[P1+1] != T4[P4] &
     T1[P1+1] != T5[P5] &
     T1[P1+1] != T6[P6] &
     T1[P1+1] != T7[P7] &
     RA + A1[P1+1] <= LA &
     RB + B1[P1+1] <= LB ] /
  P1 := P1 +1;
  RA = RA + A1[P1];
  RB = RB + B1[P1];
 }
     
------------------------- train 2 -----------------------------
s1 -> s1 
 {- [P2 < 6 &
     T2[P2+1] != T0[P0] &
     T2[P2+1] != T1[P1] &
     T2[P2+1] != T3[P3] &
     T2[P2+1] != T4[P4] &
     T2[P2+1] != T5[P5] &
     T2[P2+1] != T6[P6] &
     T2[P2+1] != T7[P7] &
     RA + A2[P2+1] <= LA &
     RB + B2[P2+1] <= LB ] /
  P2 := P2 +1;
  RA = RA + A2[P2];
  RB = RB + B2[P2];
 }

------------------------- train 3 -----------------------------
s1 -> s1 
 {- [P3 < 6 &
     T3[P3+1] != T0[P0] &
     T3[P3+1] != T1[P1] &
     T3[P3+1] != T2[P2] &
     T3[P3+1] != T4[P4] &
     T3[P3+1] != T5[P5] &
     T3[P3+1] != T6[P6] &
     T3[P3+1] != T7[P7] &
     RA + A3[P3+1] <= LA &
     RB + B3[P3+1] <= LB ] /
  P3 := P3 +1;
  RA = RA + A3[P3];
  RB = RB + B3[P3];
 }

------------------------- train 4 -----------------------------
s1 -> s1 
 {- [P4 < 6 &
     T4[P4+1] != T0[P0] &
     T4[P4+1] != T1[P1] &
     T4[P4+1] != T2[P2] &
     T4[P4+1] != T3[P3] &
     T4[P4+1] != T5[P5] &
     T4[P4+1] != T6[P6] &
     T4[P4+1] != T7[P7] &
     RA + A4[P4+1] <= LA &
     RB + B4[P4+1] <= LB ] /
  P4 := P4 +1;
  RA = RA + A4[P4];
  RB = RB + B4[P4];
 }

------------------------- train 5 -----------------------------
s1 -> s1 
 {- [P5 < 6 &
     T5[P5+1] != T0[P0] &
     T5[P5+1] != T1[P1] &
     T5[P5+1] != T2[P2] &
     T5[P5+1] != T3[P3] &
     T5[P5+1] != T4[P4] &
     T5[P5+1] != T6[P6] &
     T5[P5+1] != T7[P7] &
     RA + A5[P5+1] <= LA &
     RB + B5[P5+1] <= LB] /
  P5 := P5 +1;
  RA = RA + A5[P5];
  RB = RB + B5[P5];
 }

------------------------- train 6 -----------------------------
s1 -> s1 
 {- [P6 < 6 &
     T6[P6+1] != T0[P0] &
     T6[P6+1] != T1[P1] &
     T6[P6+1] != T2[P2] &
     T6[P6+1] != T3[P3] &
     T6[P6+1] != T4[P4] &
     T6[P6+1] != T5[P5] &
     T6[P6+1] != T7[P7] &
     RA + A6[P6+1] <= LA &
     RB + B6[P6+1] <= LB ] /
  P6 := P6 +1;
  RA = RA + A6[P6];
  RB = RB + B6[P6];
 } 

------------------------- train 7 -----------------------------
s1 -> s1 
 {- [P7 < 6 &
     T7[P7+1] != T0[P0] &
     T7[P7+1] != T1[P1] &
     T7[P7+1] != T2[P2] &
     T7[P7+1] != T3[P3] &
     T7[P7+1] != T4[P4] &
     T7[P7+1] != T5[P5] &
     T7[P7+1] != T6[P6] &
     RA + A7[P7+1] <= LA &
     RB + B7[P7+1] <= LB ] /
  P7 := P7 +1;
  RA = RA + A7[P7];
  RB = RB + B7[P7];
 }

------------------------- termination -----------------------------
 s1 -> s1 
 {- [(P0=6) and (P1=6) and (P2=6) and (P3=6)&
     (P4=6) and (P5=6) and (P6=6) and (P7=6)] / ARRIVED}
 
end REGION2;

Objects:
 Count: Token;
 SYS: REGION2;

Abstractions {
 Action ARRIVED -> ARRIVED
 Action Error -> Error
-- State: 
--   SYS.P0=0 and
--   SYS.P1=0 and
--   SYS.P2=0 and
--   SYS.P3=0 and
--   SYS.P4=0 and
--   SYS.P5=0 and
--   SYS.P6=0 and
--   SYS.P7=0 -> Home  -- abstract label on final state
}

-- time umc -m3 -100 umc_oneway8.txt AFARR.txt
--
-- > The Formula: "AF {ARRIVED} true"
-- > is: TRUE 
-- > (states generated= 1636545, computations fragments generated= 3273090, evaluation time= 37.538 sec.)
--
-- > real	0m36.980s
-- > user	1m23.800s
-- > sys	0m1.735s
-- USED VIRTUAL MEMORY: 2.98G
--
-- time mcstats -m3 umc_oneway8.txt
--
--  AFARR==   "AF {ARRIVED} true"
-------------------------------------------------------------------
-------------------------------------------------------------------