model main {
  var A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1, X1, Y1, Z1, A2, B2, C2, D2, E2, F2, G2;
  states f1, f14, f10, f11, f7, f8, f16, f15;
  transition t0 := {
    from   := f1;
    to     := f14;
    guard  := A >= B && A >= 0 && M1 > 1 && 0 > C && N1 >= M1 && D >= M1 && E = 0;
    action := F' = M1, B' = O1, C' = P1, A' = D, G' = Q1, H' = R1, I' = S1, J' = T1, K' = U1, L' = C, M' = C, N' = C, O' = N1, E' = 0, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t1 := {
    from   := f1;
    to     := f14;
    guard  := A >= B && A >= 0 && M1 > 1 && C > 0 && N1 >= M1 && D >= M1 && E = 0;
    action := F' = M1, B' = O1, C' = P1, A' = D, G' = Q1, H' = R1, I' = S1, J' = T1, K' = U1, L' = C, M' = C, N' = C, O' = N1, E' = 0, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t2 := {
    from   := f1;
    to     := f1;
    guard  := B > A && A >= 0;
    action := C' = K, A' = 1 + A, J' = K, K' = M1, P' = O1, Q' = A, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t3 := {
    from   := f10;
    to     := f14;
    guard  := A >= 0 && M1 > 1 && 0 > N && R1 >= M1 && 0 > O1 && E = 1;
    action := F' = M1, L' = O1, M' = O1, E' = 1, R' = P1, S' = 1 + D, T' = Q1, U' = D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t4 := {
    from   := f10;
    to     := f14;
    guard  := A >= 0 && M1 > 1 && 0 > N && R1 >= M1 && O1 > 0 && E = 1;
    action := F' = M1, L' = O1, M' = O1, E' = 1, R' = P1, S' = 1 + D, T' = Q1, U' = D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t5 := {
    from   := f10;
    to     := f14;
    guard  := A >= 0 && M1 > 1 && N > 0 && R1 >= M1 && 0 > O1 && E = 1;
    action := F' = M1, L' = O1, M' = O1, E' = 1, R' = P1, S' = 1 + D, T' = Q1, U' = D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t6 := {
    from   := f10;
    to     := f14;
    guard  := A >= 0 && M1 > 1 && N > 0 && R1 >= M1 && O1 > 0 && E = 1;
    action := F' = M1, L' = O1, M' = O1, E' = 1, R' = P1, S' = 1 + D, T' = Q1, U' = D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t7 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && 0 > N && 0 > O1 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t8 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && 0 > N && 0 > O1 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t9 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && 0 > N && O1 > 0 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t10 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && 0 > N && O1 > 0 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t11 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && N > 0 && 0 > O1 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t12 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && N > 0 && 0 > O1 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t13 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && N > 0 && O1 > 0 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t14 := {
    from   := f11;
    to     := f14;
    guard  := U >= 0 && M1 > 1 && N > 0 && O1 > 0 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, V' = P1, W' = Q1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t15 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && 0 > R1 && 0 > O1 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t16 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && 0 > R1 && 0 > O1 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t17 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && 0 > R1 && O1 > 0 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t18 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && 0 > R1 && O1 > 0 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t19 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && R1 > 0 && 0 > O1 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t20 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && R1 > 0 && 0 > O1 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t21 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && R1 > 0 && O1 > 0 && 0 > Q1;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t22 := {
    from   := f14;
    to     := f14;
    guard  := E >= 0 && D >= 0 && M1 > 1 && R1 > 0 && O1 > 0 && Q1 > 0;
    action := F' = M1, L' = O1, M' = O1, E' = 1 + E, D' = -1 + D, R' = P1, X' = N, Y' = Q1, Z' = 1 + E, A1' = -1 + D, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t23 := {
    from   := f7;
    to     := f8;
    guard  := P1 > B1 && C1 >= 0 && M1 > 1 && O1 > P1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t24 := {
    from   := f7;
    to     := f8;
    guard  := P1 > B1 && C1 >= 0 && M1 > 1 && O1 > P1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t25 := {
    from   := f7;
    to     := f8;
    guard  := P1 > B1 && C1 >= 0 && M1 > 1 && P1 > O1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t26 := {
    from   := f7;
    to     := f8;
    guard  := P1 > B1 && C1 >= 0 && M1 > 1 && P1 > O1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t27 := {
    from   := f7;
    to     := f8;
    guard  := B1 > P1 && C1 >= 0 && M1 > 1 && O1 > P1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t28 := {
    from   := f7;
    to     := f8;
    guard  := B1 > P1 && C1 >= 0 && M1 > 1 && O1 > P1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t29 := {
    from   := f7;
    to     := f8;
    guard  := B1 > P1 && C1 >= 0 && M1 > 1 && P1 > O1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t30 := {
    from   := f7;
    to     := f8;
    guard  := B1 > P1 && C1 >= 0 && M1 > 1 && P1 > O1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, H1' = B1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t31 := {
    from   := f7;
    to     := f16;
    guard  := C1 >= 0 && 0 > P1 && M1 > 1 && D1 = B1;
    action := F' = M1, H' = O1, L' = P1, E1' = Q1, F1' = R1, G1' = S1, D1' = T1, B1' = U1, H1' = N1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t32 := {
    from   := f7;
    to     := f16;
    guard  := C1 >= 0 && P1 > 0 && M1 > 1 && D1 = B1;
    action := F' = M1, H' = O1, L' = P1, E1' = Q1, F1' = R1, G1' = S1, D1' = T1, B1' = U1, H1' = N1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t33 := {
    from   := f8;
    to     := f8;
    guard  := Q1 > B1 && I1 >= 0 && M1 > 1 && O1 > Q1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t34 := {
    from   := f8;
    to     := f8;
    guard  := Q1 > B1 && I1 >= 0 && M1 > 1 && O1 > Q1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t35 := {
    from   := f8;
    to     := f8;
    guard  := Q1 > B1 && I1 >= 0 && M1 > 1 && Q1 > O1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t36 := {
    from   := f8;
    to     := f8;
    guard  := Q1 > B1 && I1 >= 0 && M1 > 1 && Q1 > O1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t37 := {
    from   := f8;
    to     := f8;
    guard  := B1 > Q1 && I1 >= 0 && M1 > 1 && O1 > Q1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t38 := {
    from   := f8;
    to     := f8;
    guard  := B1 > Q1 && I1 >= 0 && M1 > 1 && O1 > Q1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t39 := {
    from   := f8;
    to     := f8;
    guard  := B1 > Q1 && I1 >= 0 && M1 > 1 && Q1 > O1 && 0 > O1 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t40 := {
    from   := f8;
    to     := f8;
    guard  := B1 > Q1 && I1 >= 0 && M1 > 1 && Q1 > O1 && O1 > 0 && D1 = 0;
    action := F' = M1, L' = O1, E1' = O1, F1' = 0, G1' = O1, D1' = 0, R' = P1, H1' = B1, I1' = -1 + I1, J1' = -1 + I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t41 := {
    from   := f8;
    to     := f16;
    guard  := M1 > 1 && I1 >= 0 && D1 = B1;
    action := F' = M1, H' = O1, E1' = P1, F1' = Q1, G1' = R1, D1' = S1, B1' = T1, H1' = U1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t42 := {
    from   := f15;
    to     := f1;
    guard  := O1 > 1;
    action := K1' = M1, F' = O1, B' = O1, C' = P1, A' = 2, I' = P1, J' = P1, K' = Q1, L1' = R1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t43 := {
    from   := f15;
    to     := f16;
    guard  := 0 >= V1 && 0 >= W1 && 0 >= O1 && 0 >= X1;
    action := K1' = M1, F' = O1, B' = P1, C' = Q1, A' = R1, G' = S1, H' = T1, I' = U1, J' = N1, K' = Y1, L' = 0, M' = Z1, N' = A2, E1' = B2, F1' = C2, G1' = D2, D1' = E2, B1' = F2, H1' = G2, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t44 := {
    from   := f11;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && U >= 0 && L > 0 && 0 > L && N = 0 && E = 1;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t45 := {
    from   := f11;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && U >= 0 && L > 0 && N = 0 && E = 1;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t46 := {
    from   := f11;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && U >= 0 && 0 > L && N = 0 && E = 1;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t47 := {
    from   := f11;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && U >= 0 && 0 > L && L > 0 && N = 0 && E = 1;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t48 := {
    from   := f14;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && D >= 0 && E >= 0 && L > 0 && 0 > L && N = 0;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t49 := {
    from   := f14;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && D >= 0 && E >= 0 && L > 0 && N = 0;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t50 := {
    from   := f14;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && D >= 0 && E >= 0 && 0 > L && N = 0;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
  transition t51 := {
    from   := f14;
    to     := f8;
    guard  := Q1 > 1 && M1 > 1 && D >= 0 && E >= 0 && 0 > L && L > 0 && N = 0;
    action := F' = M1, M' = O1, N' = P1, E' = I1 + 1, E1' = L, F1' = 0, G1' = L, D1' = 0, B1' = L, H1' = L, C1' = I1, M1' = ?, N1' = ?, O1' = ?, P1' = ?, Q1' = ?, R1' = ?, S1' = ?, T1' = ?, U1' = ?, V1' = ?, W1' = ?, X1' = ?, Y1' = ?, Z1' = ?, A2' = ?, B2' = ?, C2' = ?, D2' = ?, E2' = ?, F2' = ?, G2' = ?;
  };
}
strategy dumb {
  Region init := { state = f15 };
}