Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f999
      2: f1 -> f1 : A'=1+A, B'=1+B, C'=-1+H+C, H'=0, [ H+C>=1 ], cost: 1
      7: f1 -> f1 : A'=1+R+S+A, B'=1+Q_1+B+P, C'=-1+O+C, O'=0, P'=0, Q_1'=0, R'=0, S'=0, [ C>=1 ], cost: 1
      0: f1 -> f2 : A'=0, B'=0, C'=0, D'=C+D, E'=-1+E+B, F'=-1+F+A, G'=1+G, [ A>=1 && B>=1 ], cost: 1
      3: f2 -> f1 : A'=1+A, B'=1+B, C'=-1+H+C+D, D'=0, H'=0, [ H+D>=1 ], cost: 1
      5: f2 -> f1 : A'=1+L+A, B'=1+B+J, C'=-1+Q+C+D, D'=0, E'=0, F'=0, G'=0, Q'=0, J'=0, K'=K+E, L'=0, M'=F+M, N'=N+G, [ D>=1 ], cost: 1
      6: f2 -> f1 : A'=1+A, B'=1+B, C'=-2+H+Q+C+D, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=1+J, K'=K+E, L'=1+L, M'=F+M, N'=N+G, [ H+Q+D>=2 && D>=1 ], cost: 1
      4: f2 -> f2 : D'=-1+Q+D, E'=K+E, F'=F+M, G'=N+G, Q'=0, J'=1+J, K'=0, L'=1+L, M'=0, N'=0, [ D>=1 ], cost: 1
      8: f2 -> f2 : D'=1+U+D+T, E'=-1+E+V+W, F'=X+B1+F+Z, G'=A1+Y+G, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ G>=1 && F>=C1 && C1>=1 && E>=C1 ], cost: 1
      1: f999 -> f1 : A'=1, B'=1, C'=-1+H, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 ], cost: 1

Eliminating 2 self-loops for location f1
  Self-Loop 2 has the metering function: H+C, resulting in the new transition 9.
  Removing the self-loops: 2 7.
Adding an epsilon transition (to model nonexecution of the loops): 11.
Eliminating 2 self-loops for location f2
  Removing the self-loops: 4 8.
Adding an epsilon transition (to model nonexecution of the loops): 14.

Removed all Self-loops using metering functions (where possible):
  Start location: f999
      9: f1 -> [3] : A'=H+C+A, B'=H+B+C, C'=-H, H'=0, [ H+C>=1 ], cost: H+C
     10: f1 -> [3] : A'=1+R+S+A, B'=1+Q_1+B+P, C'=-1+O+C, O'=0, P'=0, Q_1'=0, R'=0, S'=0, [ C>=1 ], cost: 1
     11: f1 -> [3] : [], cost: 0
     12: f2 -> [4] : D'=-1+Q+D, E'=K+E, F'=F+M, G'=N+G, Q'=0, J'=1+J, K'=0, L'=1+L, M'=0, N'=0, [ D>=1 ], cost: 1
     13: f2 -> [4] : D'=1+U+D+T, E'=-1+E+V+W, F'=X+B1+F+Z, G'=A1+Y+G, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ G>=1 && F>=C1 && C1>=1 && E>=C1 ], cost: 1
     14: f2 -> [4] : [], cost: 0
      1: f999 -> f1 : A'=1, B'=1, C'=-1+H, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 ], cost: 1
      0: [3] -> f2 : A'=0, B'=0, C'=0, D'=C+D, E'=-1+E+B, F'=-1+F+A, G'=1+G, [ A>=1 && B>=1 ], cost: 1
      3: [4] -> f1 : A'=1+A, B'=1+B, C'=-1+H+C+D, D'=0, H'=0, [ H+D>=1 ], cost: 1
      5: [4] -> f1 : A'=1+L+A, B'=1+B+J, C'=-1+Q+C+D, D'=0, E'=0, F'=0, G'=0, Q'=0, J'=0, K'=K+E, L'=0, M'=F+M, N'=N+G, [ D>=1 ], cost: 1
      6: [4] -> f1 : A'=1+A, B'=1+B, C'=-2+H+Q+C+D, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=1+J, K'=K+E, L'=1+L, M'=F+M, N'=N+G, [ H+Q+D>=2 && D>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f999
     15: f1 -> f2 : A'=0, B'=0, C'=0, D'=-H+D, E'=-1+H+E+B+C, F'=-1+H+F+C+A, G'=1+G, H'=0, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 ], cost: 1+H+C
     16: f1 -> f2 : A'=0, B'=0, C'=0, D'=-1+O+C+D, E'=Q_1+E+B+P, F'=R+F+S+A, G'=1+G, O'=0, P'=0, Q_1'=0, R'=0, S'=0, [ C>=1 && 1+R+S+A>=1 && 1+Q_1+B+P>=1 ], cost: 2
     17: f1 -> f2 : A'=0, B'=0, C'=0, D'=C+D, E'=-1+E+B, F'=-1+F+A, G'=1+G, [ A>=1 && B>=1 ], cost: 1
     18: f2 -> f1 : A'=1+A, B'=1+B, C'=-2+H+Q+C+D, D'=0, E'=K+E, F'=F+M, G'=N+G, H'=0, Q'=0, J'=1+J, K'=0, L'=1+L, M'=0, N'=0, [ D>=1 && -1+H+Q+D>=1 ], cost: 2
     19: f2 -> f1 : A'=2+L+A, B'=2+B+J, C'=-2+Q+C+D, D'=0, E'=0, F'=0, G'=0, Q'=0, J'=0, K'=K+E, L'=0, M'=F+M, N'=N+G, [ D>=1 && -1+Q+D>=1 ], cost: 2
     21: f2 -> f1 : A'=1+A, B'=1+B, C'=H+U+C+D+T, D'=0, E'=-1+E+V+W, F'=X+B1+F+Z, G'=A1+Y+G, H'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ G>=1 && F>=C1 && C1>=1 && E>=C1 && 1+H+U+D+T>=1 ], cost: 2
     22: f2 -> f1 : A'=1+L+A, B'=1+B+J, C'=U+Q+C+D+T, D'=0, E'=0, F'=0, G'=0, Q'=0, J'=0, K'=-1+K+E+V+W, L'=0, M'=X+B1+F+M+Z, N'=N+A1+Y+G, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ G>=1 && F>=C1 && C1>=1 && E>=C1 && 1+U+D+T>=1 ], cost: 2
     24: f2 -> f1 : A'=1+A, B'=1+B, C'=-1+H+C+D, D'=0, H'=0, [ H+D>=1 ], cost: 1
      1: f999 -> f1 : A'=1, B'=1, C'=-1+H, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f999
     27: f1 -> f1 : A'=1, B'=1, C'=-2-H+Q+D, D'=0, E'=-1+K+H+E+B+C, F'=-1+H+F+C+M+A, G'=1+N+G, H'=0, Q'=0, J'=1+J, K'=0, L'=1+L, M'=0, N'=0, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 && -1-H+Q+D>=1 ], cost: 3+H+C
     28: f1 -> f1 : A'=2+L, B'=2+J, C'=-2-H+Q+D, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-1+K+H+E+B+C, L'=0, M'=-1+H+F+C+M+A, N'=1+N+G, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 && -1-H+Q+D>=1 ], cost: 3+H+C
     29: f1 -> f1 : A'=1, B'=1, C'=-H+U+D+T, D'=0, E'=-2+H+E+B+V+C+W, F'=-1+H+X+B1+F+C+Z+A, G'=1+A1+Y+G, H'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && 1+G>=1 && -1+H+F+C+A>=C1 && C1>=1 && -1+H+E+B+C>=C1 && 1-H+U+D+T>=1 ], cost: 3+H+C
     30: f1 -> f1 : A'=1+L, B'=1+J, C'=-H+U+Q+D+T, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-2+K+H+E+B+V+C+W, L'=0, M'=-1+H+X+B1+F+C+M+Z+A, N'=1+N+A1+Y+G, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && 1+G>=1 && -1+H+F+C+A>=C1 && C1>=1 && -1+H+E+B+C>=C1 && 1-H+U+D+T>=1 ], cost: 3+H+C
     31: f1 -> f1 : A'=1, B'=1, C'=-1-H+D, D'=0, E'=-1+H+E+B+C, F'=-1+H+F+C+A, G'=1+G, H'=0, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 ], cost: 2+H+C
      1: f999 -> f1 : A'=1, B'=1, C'=-1+H, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 ], cost: 1

Eliminating 5 self-loops for location f1
  Removing the self-loops: 27 28 29 30 31.
Adding an epsilon transition (to model nonexecution of the loops): 47.

Removed all Self-loops using metering functions (where possible):
  Start location: f999
     42: f1 -> [5] : A'=1, B'=1, C'=-2-H+Q+D, D'=0, E'=-1+K+H+E+B+C, F'=-1+H+F+C+M+A, G'=1+N+G, H'=0, Q'=0, J'=1+J, K'=0, L'=1+L, M'=0, N'=0, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 && -1-H+Q+D>=1 ], cost: 3+H+C
     43: f1 -> [5] : A'=2+L, B'=2+J, C'=-2-H+Q+D, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-1+K+H+E+B+C, L'=0, M'=-1+H+F+C+M+A, N'=1+N+G, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 && -1-H+Q+D>=1 ], cost: 3+H+C
     44: f1 -> [5] : A'=1, B'=1, C'=-H+U+D+T, D'=0, E'=-2+H+E+B+V+C+W, F'=-1+H+X+B1+F+C+Z+A, G'=1+A1+Y+G, H'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && 1+G>=1 && -1+H+F+C+A>=C1 && C1>=1 && -1+H+E+B+C>=C1 && 1-H+U+D+T>=1 ], cost: 3+H+C
     45: f1 -> [5] : A'=1+L, B'=1+J, C'=-H+U+Q+D+T, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-2+K+H+E+B+V+C+W, L'=0, M'=-1+H+X+B1+F+C+M+Z+A, N'=1+N+A1+Y+G, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && 1+G>=1 && -1+H+F+C+A>=C1 && C1>=1 && -1+H+E+B+C>=C1 && 1-H+U+D+T>=1 ], cost: 3+H+C
     46: f1 -> [5] : A'=1, B'=1, C'=-1-H+D, D'=0, E'=-1+H+E+B+C, F'=-1+H+F+C+A, G'=1+G, H'=0, [ H+C>=1 && H+C+A>=1 && H+B+C>=1 && -H+D>=1 ], cost: 2+H+C
     47: f1 -> [5] : [], cost: 0
      1: f999 -> f1 : A'=1, B'=1, C'=-1+H, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f999
     48: f999 -> [5] : A'=1, B'=1, C'=0, D'=0, E'=-2+H, F'=-1+H, G'=1, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1 ], cost: 3+H
     49: f999 -> [5] : A'=1, B'=1, C'=0, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-2+H, L'=0, M'=-1+H, N'=1, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1 ], cost: 3+H


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f999
     48: f999 -> [5] : A'=1, B'=1, C'=0, D'=0, E'=-2+H, F'=-1+H, G'=1, H'=0, Q'=0, J'=0, K'=0, L'=0, M'=0, N'=0, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1 ], cost: 3+H
     49: f999 -> [5] : A'=1, B'=1, C'=0, D'=0, E'=0, F'=0, G'=0, H'=0, Q'=0, J'=0, K'=-2+H, L'=0, M'=-1+H, N'=1, O'=0, P'=0, Q_1'=0, R'=0, S'=0, T'=0, U'=0, V'=0, W'=0, X'=0, Y'=0, Z'=0, A1'=0, B1'=0, C1'=free, [ H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1 ], cost: 3+H


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 3+H
  and guard: H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1:
  Q_1: Both, K: Both, N: Both, A1: Both, H: Pos, X: Both, E: Both, U: Both, B: Both, R: Both, L: Both, O: Both, B1: Both, Q: Both, Y: Both, F: Both, V: Both, C: Both, S: Both, M: Both, P: Both, C1: Pos, J: Both, Z: Both, G: Both, W: Both, D: Both, T: Both, A: Both, where: H > C1

Found new complexity n^1, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: H>=1 && C==0 && B==0 && A==0 && D==0 && E==0 && F==0 && G==0 && Q==0 && J==0 && K==0 && L==0 && M==0 && N==0 && O==0 && P==0 && Q_1==0 && R==0 && S==0 && T==0 && U==0 && V==0 && W==0 && X==0 && Y==0 && Z==0 && A1==0 && B1==0 && -1+H>=1 && H>=1 && H>=1 && 1>=1 && -1+H>=C1 && C1>=1 && -1+H>=C1 && 1>=1
  Final Cost:  3+H

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: n^1
  Complexity value: 1

WORST_CASE(Omega(n^1),?)