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