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, R4, S4, T4, U4, V4, W4, X4, Y4, Z4, A5, B5, C5, D5, E5;
  states f171, f172, f165, f185, f170, f173, f203, f213, f226, f230, f130, f236, f238, f240, f195, f175, f147, f116, f85, f0;
  transition t0 := {
    from   := f171;
    to     := f172;
    guard  := 0 > A;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t1 := {
    from   := f171;
    to     := f172;
    guard  := A > 0;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t2 := {
    from   := f165;
    to     := f185;
    guard  := B = 7;
    action := C' = 7, B' = 7, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t3 := {
    from   := f165;
    to     := f170;
    guard  := 6 >= B;
    action := C' = B, D' = B, E' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t4 := {
    from   := f165;
    to     := f170;
    guard  := B > 7;
    action := C' = B, D' = B, E' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t5 := {
    from   := f170;
    to     := f171;
    guard  := 0 > E;
    action := F' = E, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t6 := {
    from   := f170;
    to     := f171;
    guard  := E > 0;
    action := F' = E, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t7 := {
    from   := f172;
    to     := f173;
    guard  := 0 > G;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t8 := {
    from   := f172;
    to     := f173;
    guard  := G > 0;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t9 := {
    from   := f173;
    to     := f173;
    guard  := true;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t10 := {
    from   := f203;
    to     := f213;
    guard  := C = 7;
    action := C' = 7, H' = L4, I' = M4, J' = N4, K' = L, M' = O4, N' = P4, O' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t11 := {
    from   := f213;
    to     := f226;
    guard  := O = 0;
    action := O' = 0, P' = 0, Q' = L4, R' = M4, S' = M4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t12 := {
    from   := f230;
    to     := f130;
    guard  := T = U;
    action := U' = T, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t13 := {
    from   := f203;
    to     := f130;
    guard  := 6 >= C;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t14 := {
    from   := f203;
    to     := f130;
    guard  := C > 7;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t15 := {
    from   := f226;
    to     := f130;
    guard  := S = 7;
    action := V' = 1, S' = 7, W' = 7, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t16 := {
    from   := f226;
    to     := f230;
    guard  := 6 >= S;
    action := W' = S, T' = L4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t17 := {
    from   := f226;
    to     := f230;
    guard  := S > 7;
    action := W' = S, T' = L4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t18 := {
    from   := f230;
    to     := f130;
    guard  := T > U;
    action := V' = 1, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t19 := {
    from   := f230;
    to     := f130;
    guard  := U > T;
    action := V' = 1, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t20 := {
    from   := f236;
    to     := f236;
    guard  := true;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t21 := {
    from   := f238;
    to     := f240;
    guard  := true;
    action := L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t22 := {
    from   := f213;
    to     := f226;
    guard  := 0 > O;
    action := P' = O, X' = O, Y' = L4, Z' = O, Q' = M4, R' = N4, S' = N4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t23 := {
    from   := f213;
    to     := f226;
    guard  := O > 0;
    action := P' = O, X' = O, Y' = L4, Z' = O, Q' = M4, R' = N4, S' = N4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t24 := {
    from   := f195;
    to     := f203;
    guard  := 3 >= C;
    action := A1' = B1, C1' = B1, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t25 := {
    from   := f195;
    to     := f203;
    guard  := C > 4;
    action := A1' = B1, C1' = B1, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t26 := {
    from   := f195;
    to     := f213;
    guard  := C = 4;
    action := C' = 4, A1' = B1, C1' = B1, D1' = 1, H' = L4, I' = M4, J' = N4, K' = L, M' = O4, N' = P4, O' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t27 := {
    from   := f185;
    to     := f195;
    guard  := E1 > F1;
    action := C' = L4, G1' = 1, B1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t28 := {
    from   := f185;
    to     := f195;
    guard  := F1 >= E1;
    action := F1' = 0, C' = L4, G1' = 1, B1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t29 := {
    from   := f170;
    to     := f185;
    guard  := E = 0;
    action := E' = 0, F' = 0, H1' = 3, I1' = 2, J1' = C, K1' = L4, L1' = M4, M1' = 1, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t30 := {
    from   := f175;
    to     := f165;
    guard  := true;
    action := N1' = L4, O1' = -1, B' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t31 := {
    from   := f172;
    to     := f165;
    guard  := G = 0;
    action := N1' = L4, O1' = -1, B' = 0, G' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t32 := {
    from   := f171;
    to     := f165;
    guard  := A = 0;
    action := N1' = L4, O1' = -1, B' = 0, A' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t33 := {
    from   := f147;
    to     := f165;
    guard  := 0 >= P1;
    action := Q1' = 0, R1' = 0, S1' = 0, T1' = 0, N1' = L4, O1' = -1, B' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t34 := {
    from   := f147;
    to     := f165;
    guard  := P1 > 1;
    action := Q1' = 0, R1' = 0, S1' = 0, T1' = 0, N1' = L4, O1' = -1, B' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t35 := {
    from   := f147;
    to     := f195;
    guard  := P1 = 1;
    action := Q1' = 0, C' = L4, P1' = 1, G1' = U1, R1' = 0, S1' = 0, T1' = 0, B1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t36 := {
    from   := f130;
    to     := f147;
    guard  := 0 >= V1 && V = 0;
    action := V' = 0, W1' = L4, X1' = M4, Y1' = 1, Z1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t37 := {
    from   := f130;
    to     := f147;
    guard  := V1 > 0 && V1 > A2 && V = 0;
    action := V' = 0, A2' = A2 + 1, W1' = L4, B2' = A2, X1' = M4, Y1' = 1, Z1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t38 := {
    from   := f130;
    to     := f147;
    guard  := A2 >= V1 && V1 > 0 && V = 0;
    action := V' = 0, A2' = A2 + 1, W1' = L4, B2' = A2, C2' = 0, X1' = M4, Y1' = 1, Z1' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t39 := {
    from   := f130;
    to     := f236;
    guard  := 0 > V;
    action := D2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t40 := {
    from   := f130;
    to     := f236;
    guard  := V > 0;
    action := D2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t41 := {
    from   := f116;
    to     := f116;
    guard  := 0 > E2;
    action := F2' = F2 - 1, E2' = F2, G2' = 0, H2' = 6, I2' = 1, J2' = 5, K2' = G1, L2' = L4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t42 := {
    from   := f116;
    to     := f116;
    guard  := E2 > 0;
    action := F2' = F2 - 1, E2' = F2, G2' = 0, H2' = 6, I2' = 1, J2' = 5, K2' = G1, L2' = L4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t43 := {
    from   := f116;
    to     := f130;
    guard  := E2 = 0;
    action := M2' = 8, E2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t44 := {
    from   := f85;
    to     := f116;
    guard  := Q4 > 0 && N2 = 0;
    action := N2' = 0, O2' = 0, P2' = L4, Q2' = M4, R2' = N4, S2' = L, T2' = 0, U2' = O4, V2' = 1, W2' = 0, X2' = P1, Y2' = P4, Z2' = 0, P1' = Q4, G1' = U1, F2' = Q4 - 1, E2' = Q4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t45 := {
    from   := f85;
    to     := f116;
    guard  := Q4 > 0 && 0 > N2;
    action := O2' = N2, A3' = 1, P2' = L4, Q2' = M4, R2' = N4, S2' = L, T2' = 0, U2' = O4, V2' = 1, W2' = 0, X2' = P1, Y2' = P4, Z2' = 0, P1' = Q4, G1' = U1, F2' = Q4 - 1, E2' = Q4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t46 := {
    from   := f85;
    to     := f116;
    guard  := Q4 > 0 && N2 > 0;
    action := O2' = N2, A3' = 1, P2' = L4, Q2' = M4, R2' = N4, S2' = L, T2' = 0, U2' = O4, V2' = 1, W2' = 0, X2' = P1, Y2' = P4, Z2' = 0, P1' = Q4, G1' = U1, F2' = Q4 - 1, E2' = Q4, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t47 := {
    from   := f0;
    to     := f85;
    guard  := L4 > 0 && M4 > 0;
    action := B3' = L4, Q1' = 0, V' = 0, F1' = 0, C3' = 0, D3' = 0, E3' = 0, F3' = 0, G3' = 0, H3' = 256, I3' = 0, U1' = M4, M2' = 9, L' = L4, J3' = N4, K3' = N4, L3' = N4, A2' = 0, M3' = O4, N3' = P4, O3' = Q4, P3' = R4, Q3' = 0, R3' = S4, S3' = T4, T3' = U4, U3' = V4, V3' = W4, W3' = X4, X3' = 0, Y3' = 0, Z3' = Y4, A4' = Z4, B4' = 7, C4' = 7, C' = 7, N2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t48 := {
    from   := f0;
    to     := f85;
    guard  := 6 >= A5 && L4 > 0 && M4 > 0;
    action := B3' = L4, Q1' = 0, V' = 0, F1' = 0, C3' = 0, D3' = 0, E3' = 0, F3' = 0, G3' = 0, H3' = 256, I3' = 0, U1' = M4, M2' = 9, L' = L4, J3' = N4, K3' = N4, L3' = N4, A2' = 0, M3' = O4, N3' = P4, O3' = Q4, P3' = R4, Q3' = 0, R3' = S4, S3' = T4, T3' = U4, U3' = V4, V3' = W4, W3' = X4, X3' = 0, Y3' = 0, Z3' = Y4, A4' = Z4, B4' = A5, C4' = A5, C' = A5, D4' = 3, E4' = 1, F4' = A5, G4' = B5, H4' = C5, I4' = D5, J4' = E5, K4' = 1, N2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
  transition t49 := {
    from   := f0;
    to     := f85;
    guard  := A5 > 7 && L4 > 0 && M4 > 0;
    action := B3' = L4, Q1' = 0, V' = 0, F1' = 0, C3' = 0, D3' = 0, E3' = 0, F3' = 0, G3' = 0, H3' = 256, I3' = 0, U1' = M4, M2' = 9, L' = L4, J3' = N4, K3' = N4, L3' = N4, A2' = 0, M3' = O4, N3' = P4, O3' = Q4, P3' = R4, Q3' = 0, R3' = S4, S3' = T4, T3' = U4, U3' = V4, V3' = W4, W3' = X4, X3' = 0, Y3' = 0, Z3' = Y4, A4' = Z4, B4' = A5, C4' = A5, C' = A5, D4' = 3, E4' = 1, F4' = A5, G4' = B5, H4' = C5, I4' = D5, J4' = E5, K4' = 1, N2' = 0, L4' = ?, M4' = ?, N4' = ?, O4' = ?, P4' = ?, Q4' = ?, R4' = ?, S4' = ?, T4' = ?, U4' = ?, V4' = ?, W4' = ?, X4' = ?, Y4' = ?, Z4' = ?, A5' = ?, B5' = ?, C5' = ?, D5' = ?, E5' = ?;
  };
}
strategy dumb {
  Region init := { state = f0 };
}