Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop : B'=0, D'=0, H'=0, [ 0>=A && B==C && D==E && F==G && H==Q && J==A ], cost: 1
      1: start -> lbl81 : B'=0, D'=0, F'=free, H'=1, [ A>=1 && B==C && D==E && F==G && H==Q && J==A ], cost: 1
     12: lbl81 -> lbl21 : [ 0>=1+F && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     13: lbl81 -> lbl21 : [ F>=4 && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     14: lbl81 -> lbl121 : D'=1+D, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==0 && J==A ], cost: 1
     15: lbl81 -> lbl141 : D'=-1+D, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==1 && J==A ], cost: 1
     16: lbl81 -> lbl171 : B'=1+B, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==2 && J==A ], cost: 1
     17: lbl81 -> lbl191 : B'=-1+B, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==3 && J==A ], cost: 1
      2: lbl21 -> stop : [ B+D+A>=1 && D+A>=1+B && B+A>=1+D && A>=1+B+D && H==A && J==A ], cost: 1
      3: lbl21 -> lbl81 : F'=free_1, H'=1+H, [ A>=1+H && A>=H && H+B+D>=1 && H+D>=1+B && H+B>=1+D && H>=1+B+D && J==A ], cost: 1
      4: lbl121 -> stop : [ B+D+A>=2 && D+A>=2+B && B+A>=D && A>=B+D && H==A && F==0 && J==A ], cost: 1
      5: lbl121 -> lbl81 : F'=free_2, H'=1+H, [ A>=1+H && A>=H && H+B+D>=2 && H+D>=2+B && H+B>=D && H>=B+D && F==0 && J==A ], cost: 1
      6: lbl141 -> stop : [ B+D+A>=0 && D+A>=B && B+A>=2+D && A>=2+B+D && H==A && F==1 && J==A ], cost: 1
      7: lbl141 -> lbl81 : F'=free_3, H'=1+H, [ A>=1+H && A>=H && H+B+D>=0 && H+D>=B && H+B>=2+D && H>=2+B+D && F==1 && J==A ], cost: 1
      8: lbl171 -> stop : [ B+D+A>=2 && D+A>=B && B+A>=2+D && A>=B+D && H==A && F==2 && J==A ], cost: 1
      9: lbl171 -> lbl81 : F'=free_4, H'=1+H, [ A>=1+H && A>=H && H+B+D>=2 && H+D>=B && H+B>=2+D && H>=B+D && F==2 && J==A ], cost: 1
     10: lbl191 -> stop : [ B+D+A>=0 && D+A>=2+B && B+A>=D && A>=2+B+D && H==A && F==3 && J==A ], cost: 1
     11: lbl191 -> lbl81 : F'=free_5, H'=1+H, [ A>=1+H && A>=H && H+B+D>=0 && H+D>=2+B && H+B>=D && H>=2+B+D && F==3 && J==A ], cost: 1
     18: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=A, [], cost: 1


Simplified the transitions:
  Start location: start0
      1: start -> lbl81 : B'=0, D'=0, F'=free, H'=1, [ A>=1 && B==C && D==E && F==G && H==Q && J==A ], cost: 1
     12: lbl81 -> lbl21 : [ 0>=1+F && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     13: lbl81 -> lbl21 : [ F>=4 && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     14: lbl81 -> lbl121 : D'=1+D, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==0 && J==A ], cost: 1
     15: lbl81 -> lbl141 : D'=-1+D, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==1 && J==A ], cost: 1
     16: lbl81 -> lbl171 : B'=1+B, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==2 && J==A ], cost: 1
     17: lbl81 -> lbl191 : B'=-1+B, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==3 && J==A ], cost: 1
      3: lbl21 -> lbl81 : F'=free_1, H'=1+H, [ A>=1+H && H+B+D>=1 && H+D>=1+B && H+B>=1+D && H>=1+B+D && J==A ], cost: 1
      5: lbl121 -> lbl81 : F'=free_2, H'=1+H, [ A>=1+H && H+B+D>=2 && H+D>=2+B && H+B>=D && H>=B+D && F==0 && J==A ], cost: 1
      7: lbl141 -> lbl81 : F'=free_3, H'=1+H, [ A>=1+H && H+B+D>=0 && H+D>=B && H+B>=2+D && H>=2+B+D && F==1 && J==A ], cost: 1
      9: lbl171 -> lbl81 : F'=free_4, H'=1+H, [ A>=1+H && H+B+D>=2 && H+D>=B && H+B>=2+D && H>=B+D && F==2 && J==A ], cost: 1
     11: lbl191 -> lbl81 : F'=free_5, H'=1+H, [ A>=1+H && H+B+D>=0 && H+D>=2+B && H+B>=D && H>=2+B+D && F==3 && J==A ], cost: 1
     18: start0 -> start : B'=C, D'=E, F'=G, H'=Q, J'=A, [], cost: 1


Applied simple chaining:
  Start location: start0
     14: lbl81 -> lbl81 : D'=1+D, F'=free_2, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==0 && J==A && A>=1+H && 1+H+B+D>=2 && 1+H+D>=2+B && H+B>=1+D && H>=1+B+D && F==0 && J==A ], cost: 2
     15: lbl81 -> lbl81 : D'=-1+D, F'=free_3, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==1 && J==A && A>=1+H && -1+H+B+D>=0 && -1+H+D>=B && H+B>=1+D && H>=1+B+D && F==1 && J==A ], cost: 2
     16: lbl81 -> lbl81 : B'=1+B, F'=free_4, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==2 && J==A && A>=1+H && 1+H+B+D>=2 && H+D>=1+B && 1+H+B>=2+D && H>=1+B+D && F==2 && J==A ], cost: 2
     17: lbl81 -> lbl81 : B'=-1+B, F'=free_5, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && F==3 && J==A && A>=1+H && -1+H+B+D>=0 && H+D>=1+B && -1+H+B>=D && H>=1+B+D && F==3 && J==A ], cost: 2
     12: lbl81 -> lbl21 : [ 0>=1+F && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     13: lbl81 -> lbl21 : [ F>=4 && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
      3: lbl21 -> lbl81 : F'=free_1, H'=1+H, [ A>=1+H && H+B+D>=1 && H+D>=1+B && H+B>=1+D && H>=1+B+D && J==A ], cost: 1
     18: start0 -> lbl81 : B'=0, D'=0, F'=free, H'=1, J'=A, [ A>=1 && C==C && E==E && G==G && Q==Q && A==A ], cost: 2

Eliminating 4 self-loops for location lbl81
  Removing the self-loops: 14 15 16 17.
Adding an epsilon transition (to model nonexecution of the loops): 23.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
     19: lbl81 -> [9] : D'=1+D, F'=free_2, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=1+H ], cost: 2
     20: lbl81 -> [9] : D'=-1+D, F'=free_3, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==1 && J==A && A>=1+H ], cost: 2
     21: lbl81 -> [9] : B'=1+B, F'=free_4, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=1+H ], cost: 2
     22: lbl81 -> [9] : B'=-1+B, F'=free_5, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==3 && J==A && A>=1+H ], cost: 2
     23: lbl81 -> [9] : [], cost: 0
      3: lbl21 -> lbl81 : F'=free_1, H'=1+H, [ A>=1+H && H+B+D>=1 && H+D>=1+B && H+B>=1+D && H>=1+B+D && J==A ], cost: 1
     18: start0 -> lbl81 : B'=0, D'=0, F'=free, H'=1, J'=A, [ A>=1 && C==C && E==E && G==G && Q==Q && A==A ], cost: 2
     12: [9] -> lbl21 : [ 0>=1+F && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1
     13: [9] -> lbl21 : [ F>=4 && H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && A>=H && J==A ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     24: lbl81 -> lbl21 : D'=1+D, F'=free_2, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=1+H && 0>=1+free_2 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A ], cost: 3
     25: lbl81 -> lbl21 : D'=1+D, F'=free_2, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=1+H && free_2>=4 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A ], cost: 3
     27: lbl81 -> lbl21 : D'=-1+D, F'=free_3, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==1 && J==A && A>=1+H && free_3>=4 && H+D>=1+B && 1+H+B>=D && 1+H>=B+D && H+B+D>=1 && A>=1+H && J==A ], cost: 3
     28: lbl81 -> lbl21 : B'=1+B, F'=free_4, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=1+H && 0>=1+free_4 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A ], cost: 3
     29: lbl81 -> lbl21 : B'=1+B, F'=free_4, H'=1+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=1+H && free_4>=4 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A ], cost: 3
      3: lbl21 -> lbl81 : F'=free_1, H'=1+H, [ A>=1+H && H+B+D>=1 && H+D>=1+B && H+B>=1+D && H>=1+B+D && J==A ], cost: 1
     18: start0 -> lbl81 : B'=0, D'=0, F'=free, H'=1, J'=A, [ A>=1 && C==C && E==E && G==G && Q==Q && A==A ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     34: lbl81 -> lbl81 : D'=1+D, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=1+H && 0>=1+free_2 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A && A>=2+H && 2+H+B+D>=1 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && J==A ], cost: 4
     35: lbl81 -> lbl81 : D'=1+D, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=1+H && free_2>=4 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A && A>=2+H && 2+H+B+D>=1 && 2+H+D>=1+B && 1+H+B>=2+D && 1+H>=2+B+D && J==A ], cost: 4
     36: lbl81 -> lbl81 : D'=-1+D, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==1 && J==A && A>=1+H && free_3>=4 && H+D>=1+B && 1+H+B>=D && 1+H>=B+D && H+B+D>=1 && A>=1+H && J==A && A>=2+H && H+B+D>=1 && H+D>=1+B && 1+H+B>=D && 1+H>=B+D && J==A ], cost: 4
     37: lbl81 -> lbl81 : B'=1+B, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=1+H && 0>=1+free_4 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A && A>=2+H && 2+H+B+D>=1 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && J==A ], cost: 4
     38: lbl81 -> lbl81 : B'=1+B, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=1+H && free_4>=4 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && 2+H+B+D>=1 && A>=1+H && J==A && A>=2+H && 2+H+B+D>=1 && 1+H+D>=2+B && 2+H+B>=1+D && 1+H>=2+B+D && J==A ], cost: 4
     18: start0 -> lbl81 : B'=0, D'=0, F'=free, H'=1, J'=A, [ A>=1 && C==C && E==E && G==G && Q==Q && A==A ], cost: 2

Eliminating 5 self-loops for location lbl81
  Removing the self-loops: 34 35 36 37 38.
Adding an epsilon transition (to model nonexecution of the loops): 44.
Removing duplicate transition: 39.
Removing duplicate transition: 42.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
     40: lbl81 -> [10] : D'=1+D, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==0 && J==A && A>=2+H ], cost: 4
     41: lbl81 -> [10] : D'=-1+D, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==1 && J==A && A>=2+H ], cost: 4
     43: lbl81 -> [10] : B'=1+B, F'=free_1, H'=2+H, [ H+D>=1+B && H+B>=1+D && H>=1+B+D && H+B+D>=1 && F==2 && J==A && A>=2+H ], cost: 4
     44: lbl81 -> [10] : [], cost: 0
     18: start0 -> lbl81 : B'=0, D'=0, F'=free, H'=1, J'=A, [ A>=1 && C==C && E==E && G==G && Q==Q && 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),?)