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;
  states f14, f18, f15, f27, f1, f10, f11, f20, f12, f13, f16, f19;
  transition t0 := {
    from   := f14;
    to     := f18;
    guard  := A > 1 && X2 >= A && B >= 0 && C > 0 && Y2 > 0 && D = 1;
    action := C' = -1 + Y2, E' = -1, F' = -1 + Y2, G' = H, I' = Z2, J' = 1 + H, K' = A3, L' = B3, M' = Z2, D' = 1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t1 := {
    from   := f15;
    to     := f27;
    guard  := A > 1 && 0 >= C && H >= 0 && G = H && D = 1;
    action := H' = G, D' = 1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t2 := {
    from   := f15;
    to     := f18;
    guard  := A > 1 && C > 0 && Y2 > 0 && G >= 0;
    action := C' = -1 + Y2, G' = Z2, M' = A3, H' = -1 + Z2, D' = 2, N' = -1, O' = -1 + Y2, P' = 2, Q' = B3, R' = X2, S' = C3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t3 := {
    from   := f18;
    to     := f27;
    guard  := D >= 0 && H >= 0 && 0 >= C;
    action := H' = Y2, D' = Z2, T' = Z2, U' = Y2, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t4 := {
    from   := f18;
    to     := f18;
    guard  := A > 1 && D >= 0 && V > 0 && H >= 0 && C = V;
    action := C' = -1 + C, H' = -1 + H, D' = 1 + D, W' = 1 + D, X' = -1 + H, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t5 := {
    from   := f27;
    to     := f18;
    guard  := A > 1 && D >= 0 && 0 >= Y && H >= 0;
    action := C' = Y2, Z' = Z2, A1' = D, B1' = H, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t6 := {
    from   := f1;
    to     := f1;
    guard  := B >= 0 && C1 > B;
    action := B' = 1 + B, D1' = E1, F1' = E1, E1' = Y2, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t7 := {
    from   := f10;
    to     := f11;
    guard  := G1 >= 0;
    action := H1' = I1, G1' = Y2, J1' = -1 + Y2, K1' = -1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t8 := {
    from   := f10;
    to     := f20;
    guard  := G1 >= 0 && L1 = I1;
    action := M1' = Y2, N1' = Z2, O1' = A3, L1' = B3, I1' = X2, P1' = C3, H1' = D3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t9 := {
    from   := f11;
    to     := f11;
    guard  := A > 1 && J1 >= 0 && C > 0 && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0;
    action := Q1' = 0, M1' = R1, N1' = 0, O1' = R1, L1' = 0, H1' = I1, J1' = -1 + J1, S1' = -1 + J1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t10 := {
    from   := f11;
    to     := f20;
    guard  := J1 >= 0 && L1 = I1;
    action := A' = Y2, M1' = Z2, N1' = A3, O1' = B3, L1' = X2, I1' = C3, P1' = D3, H1' = E3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t11 := {
    from   := f12;
    to     := f13;
    guard  := T1 >= 0;
    action := H1' = I1, T1' = Y2, U1' = -1 + Y2, V1' = -1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t12 := {
    from   := f12;
    to     := f20;
    guard  := T1 >= 0 && L1 = I1;
    action := M1' = Y2, N1' = Z2, O1' = A3, L1' = B3, I1' = X2, P1' = C3, H1' = D3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t13 := {
    from   := f13;
    to     := f13;
    guard  := A > 1 && U1 >= 0 && 0 >= C && Q1 = 0 && R1 = O1 && N1 = 0 && M1 = O1 && L1 = 0;
    action := Q1' = 0, M1' = R1, N1' = 0, O1' = R1, L1' = 0, H1' = I1, U1' = -1 + U1, W1' = -1 + U1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t14 := {
    from   := f13;
    to     := f20;
    guard  := U1 >= 0 && L1 = I1;
    action := M1' = Y2, N1' = Z2, O1' = A3, L1' = B3, I1' = X2, P1' = C3, H1' = D3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t15 := {
    from   := f14;
    to     := f18;
    guard  := B3 >= A && A > 1 && H >= A && 0 >= C && H >= 0 && Q1 = R1 && B = H && D = 0;
    action := X1' = B, B' = Y2, C' = Z2, R1' = Q1, H' = B, D' = 0, Z' = A3, Y1' = Y2, Z1' = B3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t16 := {
    from   := f1;
    to     := f18;
    guard  := F3 >= A && B3 >= A && B >= C1 && A > 1 && H >= A && H >= 0 && B >= 0 && D = 0;
    action := B' = Y2, C' = Z2, Q1' = D1, R1' = D1, D' = 0, Z' = A3, Y1' = Y2, Z1' = B3, C1' = X2, D1' = C3, F1' = D3, E1' = E3, A2' = G3, B2' = H3, P1' = I3, C2' = H, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t17 := {
    from   := f16;
    to     := f16;
    guard  := 0 >= C && Q1 = R1 && A = 1;
    action := C' = Y2, R1' = Q1, A' = 1, D2' = E2, E2' = Z2, Z' = A3, F2' = Z2, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t18 := {
    from   := f15;
    to     := f11;
    guard  := Y2 >= 0 && A > 1 && C > 0 && Q1 = 0 && G = 0 && D = 1;
    action := Q1' = 0, G' = 0, D' = J1 + 1, M1' = R1, N1' = 0, O1' = R1, L1' = 0, I1' = R1, G2' = Y2, H1' = R1, H2' = -1, G1' = J1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t19 := {
    from   := f18;
    to     := f11;
    guard  := Z2 >= 0 && Y2 >= 0 && A > 1 && C > 0 && D >= 0 && H >= 0 && Q1 = 0;
    action := Q1' = 0, D' = J1 + 1, I2' = Y2, M1' = R1, N1' = 0, O1' = R1, L1' = 0, I1' = R1, G2' = Z2, H1' = R1, H2' = -1, G1' = J1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t20 := {
    from   := f27;
    to     := f13;
    guard  := Y2 >= 0 && A > 1 && 0 >= C && D >= 0 && H >= 0 && Q1 = 0;
    action := Q1' = 0, D' = U1 + 1, M1' = R1, N1' = 0, O1' = R1, L1' = 0, I1' = R1, J2' = Y2, H1' = R1, K2' = -1, T1' = U1, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t21 := {
    from   := f19;
    to     := f1;
    guard  := Y2 > 1 && E1 = A2;
    action := B' = 2, A' = Y2, E2' = Z2, Z' = A3, C1' = Y2, D1' = E1, F1' = E1, E1' = B3, L2' = X2, A2' = E1, M2' = 2, N2' = C3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t22 := {
    from   := f19;
    to     := f16;
    guard  := E1 = A2;
    action := B' = Y2, C' = Z2, Q1' = E1, R1' = E1, A' = 1, E2' = A3, Z' = B3, F2' = A3, C1' = X2, D1' = C3, F1' = D3, E1' = E3, L2' = G3, A2' = H3, B2' = I3, P1' = F3, O2' = J3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t23 := {
    from   := f19;
    to     := f20;
    guard  := 0 >= Z2;
    action := B' = Y2, Q1' = 0, R1' = 0, A' = Z2, M1' = A3, N1' = B3, O1' = X2, L1' = C3, I1' = D3, Z' = E3, C1' = G3, D1' = H3, F1' = I3, E1' = F3, A2' = J3, B2' = K3, P1' = L3, H1' = M3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t24 := {
    from   := f16;
    to     := f20;
    guard  := C > 0 && Y2 > 1 && Q1 = 0 && R1 = 0 && A = 1;
    action := C' = -1 + Y2, Q1' = 0, R1' = 0, A' = 1, E2' = Z2, P2' = -1, Q2' = -1 + Y2, R2' = A3, S2' = B3, T2' = X2, M1' = C3, N1' = D3, O1' = E3, L1' = G3, I1' = H3, U2' = Z2, P1' = I3, H1' = F3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
  transition t25 := {
    from   := f16;
    to     := f20;
    guard  := C > 0 && Q1 = 0 && R1 = 0 && A = 1;
    action := C' = 0, Q1' = 0, R1' = 0, A' = 1, E2' = Y2, P2' = -1, Q2' = 0, R2' = Z2, S2' = A3, V2' = B3, M1' = X2, N1' = C3, O1' = D3, L1' = E3, I1' = G3, W2' = Y2, P1' = H3, H1' = I3, X2' = ?, Y2' = ?, Z2' = ?, A3' = ?, B3' = ?, C3' = ?, D3' = ?, E3' = ?, F3' = ?, G3' = ?, H3' = ?, I3' = ?, J3' = ?, K3' = ?, L3' = ?, M3' = ?;
  };
}
strategy dumb {
  Region init := { state = f19 };
}