Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop : L'=0, [ 1>=A && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      1: start -> lbl53 : D'=1, H'=0, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      2: start -> lbl53 : D'=1, H'=1, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      5: lbl53 -> lbl53 : D'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && A>=J && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
      6: lbl53 -> lbl53 : D'=J, H'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && A>=J && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
      4: lbl53 -> lbl91 : F'=free, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A ], cost: 1
      3: lbl91 -> lbl13 : B'=L, L'=1+L, [ D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A ], cost: 1
      7: lbl13 -> stop : [ 2+H>=A && A>=2 && A>=1+H && 1+L==A && 2+B==A && 1+D==A && N==A && J==A ], cost: 1
      8: lbl13 -> lbl53 : D'=1+L, H'=L, J'=2+L, [ A>=3+B && A>=2+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
      9: lbl13 -> lbl53 : D'=1+L, H'=1+L, J'=2+L, [ A>=3+B && A>=2+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=K, L'=M, N'=A, [], cost: 1


Simplified the transitions:
  Start location: start0
      1: start -> lbl53 : D'=1, H'=0, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      2: start -> lbl53 : D'=1, H'=1, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      5: lbl53 -> lbl53 : D'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
      6: lbl53 -> lbl53 : D'=J, H'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
      4: lbl53 -> lbl91 : F'=free, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A ], cost: 1
      3: lbl91 -> lbl13 : B'=L, L'=1+L, [ D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A ], cost: 1
      8: lbl13 -> lbl53 : D'=1+L, H'=L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
      9: lbl13 -> lbl53 : D'=1+L, H'=1+L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=K, L'=M, N'=A, [], cost: 1

Eliminating 2 self-loops for location lbl53
  Removing the self-loops: 5 6.
Adding an epsilon transition (to model nonexecution of the loops): 13.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      1: start -> lbl53 : D'=1, H'=0, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      2: start -> lbl53 : D'=1, H'=1, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
     11: lbl53 -> [6] : D'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
     12: lbl53 -> [6] : D'=J, H'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
     13: lbl53 -> [6] : [], cost: 0
      3: lbl91 -> lbl13 : B'=L, L'=1+L, [ D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A ], cost: 1
      8: lbl13 -> lbl53 : D'=1+L, H'=L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
      9: lbl13 -> lbl53 : D'=1+L, H'=1+L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=K, L'=M, N'=A, [], cost: 1
      4: [6] -> lbl91 : F'=free, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A ], cost: 1


Applied simple chaining:
  Start location: start0
      1: start -> lbl53 : D'=1, H'=0, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
      2: start -> lbl53 : D'=1, H'=1, J'=2, L'=0, [ A>=2 && B==C && D==E && F==G && H==Q && J==K && L==M && N==A ], cost: 1
     11: lbl53 -> [6] : D'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
     12: lbl53 -> [6] : D'=J, H'=J, J'=1+J, [ A>=1+J && D>=H && D>=1 && J>=1+D && 1+H>=D && 1+L==D && N==A ], cost: 1
     13: lbl53 -> [6] : [], cost: 0
      8: lbl13 -> lbl53 : D'=1+L, H'=L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
      9: lbl13 -> lbl53 : D'=1+L, H'=1+L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
     10: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=K, L'=M, N'=A, [], cost: 1
      4: [6] -> lbl13 : B'=L, F'=free, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     16: lbl53 -> lbl13 : B'=L, F'=free, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A ], cost: 2
      8: lbl13 -> lbl53 : D'=1+L, H'=L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
      9: lbl13 -> lbl53 : D'=1+L, H'=1+L, J'=2+L, [ A>=3+B && H>=B && B>=0 && 1+B>=H && L==1+B && D==1+B && N==A && J==A ], cost: 1
     14: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=0, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2
     15: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=1, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     17: lbl53 -> lbl53 : B'=L, D'=2+L, F'=free, H'=1+L, J'=3+L, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A && A>=3+L && H>=L && L>=0 && 1+L>=H && 1+L==1+L && D==1+L && N==A && J==A ], cost: 3
     18: lbl53 -> lbl53 : B'=L, D'=2+L, F'=free, H'=2+L, J'=3+L, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && D>=H && D>=1 && 1+H>=D && A>=1+D && N==A && 1+L==D && J==A && A>=3+L && H>=L && L>=0 && 1+L>=H && 1+L==1+L && D==1+L && N==A && J==A ], cost: 3
     14: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=0, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2
     15: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=1, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2

Eliminating 2 self-loops for location lbl53
  Removing the self-loops: 17 18.
Adding an epsilon transition (to model nonexecution of the loops): 21.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
     19: lbl53 -> [7] : B'=L, D'=2+L, F'=free, H'=1+L, J'=3+L, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && A>=3+L && H>=L && L>=0 && 1+L>=H ], cost: 3
     20: lbl53 -> [7] : B'=L, D'=2+L, F'=free, H'=2+L, J'=3+L, L'=1+L, [ D>=H && D>=1 && A>=1+D && 1+H>=D && J==A && 1+L==D && N==A && A>=3+L && H>=L && L>=0 && 1+L>=H ], cost: 3
     21: lbl53 -> [7] : [], cost: 0
     14: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=0, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2
     15: start0 -> lbl53 : B'=C, D'=1, F'=G, H'=1, J'=2, L'=0, N'=A, [ A>=2 && C==C && E==E && G==G && Q==Q && K==K && M==M && A==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

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

WORST_CASE(Omega(1),?)