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, H2, I2, J2, K2, L2, M2, N2, O2, P2, Q2, R2, S2, T2, U2, V2, W2, X2, Y2, Z2, A3, B3, C3, D3, E3, F3, G3, H3, I3, J3, K3, L3, M3, N3, O3, P3, Q3, R3, S3, T3, U3, V3, W3, X3, Y3, Z3, A4, B4, C4, D4, E4, F4, G4, H4, I4, J4, K4, L4, M4;
  states f155, f168, f160, f163, f186, f196, f209, f213, f120, f219, f221, f223, f178, f165, f137, f105, f76, f0;
  transition t0 := {
    from   := f155;
    to     := f168;
    guard  := A = 7;
    action := B' = 7, A' = 7, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t1 := {
    from   := f155;
    to     := f160;
    guard  := 6 >= A;
    action := B' = A, C' = A, D' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t2 := {
    from   := f155;
    to     := f160;
    guard  := A > 7;
    action := B' = A, C' = A, D' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t3 := {
    from   := f163;
    to     := f163;
    guard  := true;
    action := X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t4 := {
    from   := f160;
    to     := f163;
    guard  := E > 0 && D > 0 && F > 0;
    action := G' = D, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t5 := {
    from   := f186;
    to     := f196;
    guard  := B = 7;
    action := B' = 7, H' = X3, I' = Y3, J' = Z3, K' = L, M' = A4, N' = B4, O' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t6 := {
    from   := f196;
    to     := f209;
    guard  := 0 >= O;
    action := P' = O, Q' = X3, R' = Y3, S' = Y3, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t7 := {
    from   := f213;
    to     := f120;
    guard  := T = 0;
    action := T' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t8 := {
    from   := f186;
    to     := f120;
    guard  := 6 >= B;
    action := X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t9 := {
    from   := f186;
    to     := f120;
    guard  := B > 7;
    action := X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t10 := {
    from   := f209;
    to     := f120;
    guard  := S = 7;
    action := U' = 1, S' = 7, V' = 7, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t11 := {
    from   := f209;
    to     := f213;
    guard  := 6 >= S;
    action := V' = S, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t12 := {
    from   := f209;
    to     := f213;
    guard  := S > 7;
    action := V' = S, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t13 := {
    from   := f213;
    to     := f120;
    guard  := 0 > T;
    action := U' = 1, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t14 := {
    from   := f213;
    to     := f120;
    guard  := T > 0;
    action := U' = 1, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t15 := {
    from   := f219;
    to     := f219;
    guard  := true;
    action := X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t16 := {
    from   := f221;
    to     := f223;
    guard  := true;
    action := X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t17 := {
    from   := f196;
    to     := f209;
    guard  := O > 0;
    action := P' = O, W' = O, X' = X3, Y' = O, Q' = Y3, R' = Z3, S' = Z3, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t18 := {
    from   := f178;
    to     := f186;
    guard  := 3 >= B;
    action := Z' = A1, B1' = A1, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t19 := {
    from   := f178;
    to     := f186;
    guard  := B > 4;
    action := Z' = A1, B1' = A1, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t20 := {
    from   := f178;
    to     := f196;
    guard  := B = 4;
    action := B' = 4, Z' = A1, B1' = A1, C1' = 1, H' = X3, I' = Y3, J' = Z3, K' = L, M' = A4, N' = B4, O' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t21 := {
    from   := f168;
    to     := f178;
    guard  := D1 > E1;
    action := B' = X3, F1' = 1, A1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t22 := {
    from   := f168;
    to     := f178;
    guard  := E1 >= D1;
    action := E1' = 0, B' = X3, F1' = 1, A1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t23 := {
    from   := f160;
    to     := f168;
    guard  := 0 >= D;
    action := G' = D, G1' = 1, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t24 := {
    from   := f165;
    to     := f155;
    guard  := true;
    action := H1' = X3, I1' = -1, A' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t25 := {
    from   := f160;
    to     := f155;
    guard  := D > 0 && 0 >= F;
    action := H1' = X3, I1' = -1, A' = 0, G' = D, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t26 := {
    from   := f160;
    to     := f155;
    guard  := 0 >= E && D > 0 && F > 0;
    action := H1' = X3, I1' = -1, A' = 0, G' = D, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t27 := {
    from   := f137;
    to     := f155;
    guard  := 0 >= J1;
    action := K1' = 0, L1' = 0, M1' = 0, N1' = 0, H1' = X3, I1' = -1, A' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t28 := {
    from   := f137;
    to     := f155;
    guard  := J1 > 1;
    action := K1' = 0, L1' = 0, M1' = 0, N1' = 0, H1' = X3, I1' = -1, A' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t29 := {
    from   := f137;
    to     := f178;
    guard  := J1 = 1;
    action := K1' = 0, B' = X3, J1' = 1, F1' = O1, L1' = 0, M1' = 0, N1' = 0, A1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t30 := {
    from   := f120;
    to     := f137;
    guard  := 0 >= U && 0 >= P1;
    action := Q1' = X3, R1' = Y3, S1' = 1, T1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t31 := {
    from   := f120;
    to     := f137;
    guard  := P1 > U1 && 0 >= U && P1 > 0;
    action := U1' = U1 + 1, Q1' = X3, V1' = U1, R1' = Y3, S1' = 1, T1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t32 := {
    from   := f120;
    to     := f137;
    guard  := P1 > 0 && 0 >= U && U1 >= P1;
    action := U1' = U1 + 1, Q1' = X3, V1' = U1, W1' = 0, R1' = Y3, S1' = 1, T1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t33 := {
    from   := f120;
    to     := f219;
    guard  := U > 0;
    action := X1' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t34 := {
    from   := f105;
    to     := f105;
    guard  := Y1 > 0;
    action := Y1' = Y1 - 1, Z1' = 0, A2' = 6, B2' = 1, C2' = 5, D2' = F1, E2' = X3, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t35 := {
    from   := f105;
    to     := f120;
    guard  := 0 >= Y1;
    action := F2' = 8, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t36 := {
    from   := f76;
    to     := f105;
    guard  := C4 > 0 && 0 >= G2;
    action := H2' = G2, I2' = X3, J2' = Y3, K2' = Z3, L2' = L, M2' = 0, N2' = A4, O2' = 1, P2' = 0, Q2' = J1, R2' = B4, S2' = 0, J1' = C4, F1' = O1, Y1' = C4, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t37 := {
    from   := f76;
    to     := f105;
    guard  := C4 > 0 && G2 > 0;
    action := H2' = G2, T2' = 1, I2' = X3, J2' = Y3, K2' = Z3, L2' = L, M2' = 0, N2' = A4, O2' = 1, P2' = 0, Q2' = J1, R2' = B4, S2' = 0, J1' = C4, F1' = O1, Y1' = C4, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t38 := {
    from   := f0;
    to     := f76;
    guard  := X3 > 0 && Y3 > 0;
    action := U2' = X3, K1' = 0, U' = 0, E1' = 0, V2' = 0, W2' = 0, X2' = 0, Y2' = 0, Z2' = 0, A3' = 256, B3' = 0, O1' = Y3, F2' = 9, L' = X3, C3' = Z3, D3' = Z3, E3' = Z3, U1' = 0, F3' = A4, G3' = B4, H3' = C4, I3' = D4, J3' = 0, K3' = E4, L3' = F4, M3' = G4, N3' = H4, O3' = I4, P3' = J4, Q3' = 0, R3' = 0, S3' = K4, T3' = L4, U3' = 7, V3' = 7, B' = 7, G2' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t39 := {
    from   := f0;
    to     := f76;
    guard  := 6 >= M4 && X3 > 0 && Y3 > 0;
    action := U2' = X3, K1' = 0, U' = 0, E1' = 0, V2' = 0, W2' = 0, X2' = 0, Y2' = 0, Z2' = 0, A3' = 256, B3' = 0, O1' = Y3, F2' = 9, L' = X3, C3' = Z3, D3' = Z3, E3' = Z3, U1' = 0, F3' = A4, G3' = B4, H3' = C4, I3' = D4, J3' = 0, K3' = E4, L3' = F4, M3' = G4, N3' = H4, O3' = I4, P3' = J4, Q3' = 0, R3' = 0, S3' = K4, T3' = L4, U3' = M4, V3' = M4, B' = M4, W3' = 1, G2' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
  transition t40 := {
    from   := f0;
    to     := f76;
    guard  := M4 > 7 && X3 > 0 && Y3 > 0;
    action := U2' = X3, K1' = 0, U' = 0, E1' = 0, V2' = 0, W2' = 0, X2' = 0, Y2' = 0, Z2' = 0, A3' = 256, B3' = 0, O1' = Y3, F2' = 9, L' = X3, C3' = Z3, D3' = Z3, E3' = Z3, U1' = 0, F3' = A4, G3' = B4, H3' = C4, I3' = D4, J3' = 0, K3' = E4, L3' = F4, M3' = G4, N3' = H4, O3' = I4, P3' = J4, Q3' = 0, R3' = 0, S3' = K4, T3' = L4, U3' = M4, V3' = M4, B' = M4, W3' = 1, G2' = 0, X3' = ?, Y3' = ?, Z3' = ?, A4' = ?, B4' = ?, C4' = ?, D4' = ?, E4' = ?, F4' = ?, G4' = ?, H4' = ?, I4' = ?, J4' = ?, K4' = ?, L4' = ?, M4' = ?;
  };
}
strategy dumb {
  Region init := { state = f0 };
}