Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop : [ A>=5 && B==C && D==E && F==G && H==A ], cost: 1
      1: start -> lbl92 : D'=H, F'=0, H'=1+H, [ 2>=A && B==C && D==E && F==G && H==A ], cost: 1
      2: start -> lbl82 : B'=0, F'=1, [ A>=3 && 4>=A && B==C && D==E && F==G && H==A ], cost: 1
      3: lbl92 -> stop : [ D>=4 && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      4: lbl92 -> lbl92 : D'=H, F'=0, H'=1+H, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      5: lbl92 -> lbl82 : B'=0, F'=1, [ D>=2 && 3>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      6: lbl82 -> lbl92 : D'=H, H'=1+H, [ 2>=H && 9>=B && B>=0 && H>=A && H>=3 && 4>=H && F==1+B ], cost: 1
      7: lbl82 -> lbl92 : D'=H, H'=1+H, [ H>=A && H>=3 && 4>=H && F==10 && B==9 ], cost: 1
      8: lbl82 -> lbl82 : B'=F, F'=1+F, [ H>=3 && 8>=B && 9>=B && B>=0 && H>=A && 4>=H && F==1+B ], cost: 1
      9: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1


Simplified the transitions:
  Start location: start0
      1: start -> lbl92 : D'=H, F'=0, H'=1+H, [ 2>=A && B==C && D==E && F==G && H==A ], cost: 1
      2: start -> lbl82 : B'=0, F'=1, [ A>=3 && 4>=A && B==C && D==E && F==G && H==A ], cost: 1
      4: lbl92 -> lbl92 : D'=H, F'=0, H'=1+H, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      5: lbl92 -> lbl82 : B'=0, F'=1, [ D>=2 && 3>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      6: lbl82 -> lbl92 : D'=H, H'=1+H, [ 2>=H && 9>=B && B>=0 && H>=A && H>=3 && F==1+B ], cost: 1
      7: lbl82 -> lbl92 : D'=H, H'=1+H, [ H>=A && H>=3 && 4>=H && F==10 && B==9 ], cost: 1
      8: lbl82 -> lbl82 : B'=F, F'=1+F, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B ], cost: 1
      9: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1

Eliminating 1 self-loops for location lbl92
  Self-Loop 4 has the metering function: meter, resulting in the new transition 10.
  Removing the self-loops: 4.
Eliminating 1 self-loops for location lbl82
  Self-Loop 8 has the metering function: meter_1, resulting in the new transition 11.
  Removing the self-loops: 8.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      1: start -> lbl92 : D'=H, F'=0, H'=1+H, [ 2>=A && B==C && D==E && F==G && H==A ], cost: 1
      2: start -> lbl82 : B'=0, F'=1, [ A>=3 && 4>=A && B==C && D==E && F==G && H==A ], cost: 1
     10: lbl92 -> [5] : D'=-1+H+meter, F'=0, H'=H+meter, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D && 2*meter==5-H-D ], cost: meter
     11: lbl82 -> [6] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
      9: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1
      5: [5] -> lbl82 : B'=0, F'=1, [ D>=2 && 3>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D ], cost: 1
      6: [6] -> lbl92 : D'=H, H'=1+H, [ 2>=H && 9>=B && B>=0 && H>=A && H>=3 && F==1+B ], cost: 1
      7: [6] -> lbl92 : D'=H, H'=1+H, [ H>=A && H>=3 && 4>=H && F==10 && B==9 ], cost: 1


Applied simple chaining:
  Start location: start0
      1: start -> lbl92 : D'=H, F'=0, H'=1+H, [ 2>=A && B==C && D==E && F==G && H==A ], cost: 1
      2: start -> lbl82 : B'=0, F'=1, [ A>=3 && 4>=A && B==C && D==E && F==G && H==A ], cost: 1
     10: lbl92 -> lbl82 : B'=0, D'=-1+H+meter, F'=1, H'=H+meter, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D && 2*meter==5-H-D && -1+H+meter>=2 && 3>=-1+H+meter && -1+H+meter>=A && 10>=-5+5*H+5*meter && 0>=0 && H+meter==H+meter ], cost: 1+meter
     11: lbl82 -> [6] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
      9: start0 -> start : B'=C, D'=E, F'=G, H'=A, [], cost: 1
      6: [6] -> lbl92 : D'=H, H'=1+H, [ 2>=H && 9>=B && B>=0 && H>=A && H>=3 && F==1+B ], cost: 1
      7: [6] -> lbl92 : D'=H, H'=1+H, [ H>=A && H>=3 && 4>=H && F==10 && B==9 ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     10: lbl92 -> lbl82 : B'=0, D'=-1+H+meter, F'=1, H'=H+meter, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D && 2*meter==5-H-D && -1+H+meter>=2 && 3>=-1+H+meter && -1+H+meter>=A && 10>=-5+5*H+5*meter && 0>=0 && H+meter==H+meter ], cost: 1+meter
     15: lbl82 -> lbl92 : B'=-1+F+meter_1, D'=H, F'=F+meter_1, H'=1+H, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F && H>=A && H>=3 && 4>=H && F+meter_1==10 && -1+F+meter_1==9 ], cost: 1+meter_1
     14: lbl82 -> [7] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
     12: start0 -> lbl92 : B'=C, D'=A, F'=0, H'=1+A, [ 2>=A && C==C && E==E && G==G && A==A ], cost: 2
     13: start0 -> lbl82 : B'=0, D'=E, F'=1, H'=A, [ A>=3 && 4>=A && C==C && E==E && G==G && A==A ], cost: 2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
     10: lbl92 -> lbl82 : B'=0, D'=-1+H+meter, F'=1, H'=H+meter, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D && 2*meter==5-H-D && -1+H+meter>=2 && 3>=-1+H+meter && -1+H+meter>=A && 10>=-5+5*H+5*meter && 0>=0 && H+meter==H+meter ], cost: 1+meter
     15: lbl82 -> lbl92 : B'=-1+F+meter_1, D'=H, F'=F+meter_1, H'=1+H, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F && H>=A && H>=3 && 4>=H && F+meter_1==10 && -1+F+meter_1==9 ], cost: 1+meter_1
     14: lbl82 -> [7] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
     12: start0 -> lbl92 : B'=C, D'=A, F'=0, H'=1+A, [ 2>=A && C==C && E==E && G==G && A==A ], cost: 2
     13: start0 -> lbl82 : B'=0, D'=E, F'=1, H'=A, [ A>=3 && 4>=A && C==C && E==E && G==G && A==A ], cost: 2

This is only a partial result (probably due to a timeout), trying to find max complexity

Removed transitions with const cost
  Start location: start0
     10: lbl92 -> lbl82 : B'=0, D'=-1+H+meter, F'=1, H'=H+meter, [ 1>=D && D>=A && 10+F>=5*D && F>=0 && H==1+D && 2*meter==5-H-D && -1+H+meter>=2 && 3>=-1+H+meter && -1+H+meter>=A && 10>=-5+5*H+5*meter && 0>=0 && H+meter==H+meter ], cost: 1+meter
     15: lbl82 -> lbl92 : B'=-1+F+meter_1, D'=H, F'=F+meter_1, H'=1+H, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F && H>=A && H>=3 && 4>=H && F+meter_1==10 && -1+F+meter_1==9 ], cost: 1+meter_1
     14: lbl82 -> [7] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
     12: start0 -> lbl92 : B'=C, D'=A, F'=0, H'=1+A, [ 2>=A && C==C && E==E && G==G && A==A ], cost: 2

Performed chaining from the start location:
  Start location: start0
     15: lbl82 -> lbl92 : B'=-1+F+meter_1, D'=H, F'=F+meter_1, H'=1+H, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F && H>=A && H>=3 && 4>=H && F+meter_1==10 && -1+F+meter_1==9 ], cost: 1+meter_1
     14: lbl82 -> [7] : B'=-1+F+meter_1, F'=F+meter_1, [ H>=3 && 8>=B && B>=0 && H>=A && 4>=H && F==1+B && 2*meter_1==19-B-F ], cost: meter_1
     16: start0 -> lbl82 : B'=0, D'=meter+A, F'=1, H'=1+meter+A, [ 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A ], cost: 3+meter

  Found configuration with infinitely models for cost: 3+meter
  and guard: 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A:
  E: Both, meter: Const, C: Both, G: Both, A: Const

Found new complexity const, because: Found infinity configuration.

Performed chaining from the start location:
  Start location: start0
     17: start0 -> lbl92 : B'=meter_1, D'=1+meter+A, F'=1+meter_1, H'=2+meter+A, [ 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A && 1+meter+A>=3 && 8>=0 && 0>=0 && 1+meter+A>=A && 4>=1+meter+A && 1==1 && 2*meter_1==18 && 1+meter+A>=A && 1+meter+A>=3 && 4>=1+meter+A && 1+meter_1==10 && meter_1==9 ], cost: 4+meter+meter_1
     18: start0 -> [7] : B'=meter_1, D'=meter+A, F'=1+meter_1, H'=1+meter+A, [ 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A && 1+meter+A>=3 && 8>=0 && 0>=0 && 1+meter+A>=A && 4>=1+meter+A && 1==1 && 2*meter_1==18 ], cost: 3+meter+meter_1

  Found configuration with infinitely models for cost: 4+meter+meter_1
  and guard: 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A && 1+meter+A>=3 && 8>=0 && 0>=0 && 1+meter+A>=A && 4>=1+meter+A && 1==1 && 2*meter_1==18 && 1+meter+A>=A && 1+meter+A>=3 && 4>=1+meter+A && 1+meter_1==10 && meter_1==9:
  E: Both, meter: Const, C: Both, meter_1: Both, G: Both, A: Const

  Found configuration with infinitely models for cost: 3+meter+meter_1
  and guard: 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A && 1+meter+A>=3 && 8>=0 && 0>=0 && 1+meter+A>=A && 4>=1+meter+A && 1==1 && 2*meter_1==18:
  E: Both, meter: Const, C: Both, meter_1: Const, G: Both, A: Const

Performed chaining from the start location:
  Start location: start0
    <empty>


The final runtime is determined by this resulting transition:
  Final Guard: 2>=A && C==C && E==E && G==G && A==A && 1>=A && A>=A && 10>=5*A && 0>=0 && 1+A==1+A && 2*meter==4-2*A && meter+A>=2 && 3>=meter+A && meter+A>=A && 10>=5*meter+5*A && 0>=0 && 1+meter+A==1+meter+A
  Final Cost:  4

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

WORST_CASE(Omega(1),?)