Trying to load file: main.koat

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


Simplified the transitions:
  Start location: start0
      1: start -> lbl42 : B'=-1+B, [ A>=0 && C>=0 && B==C && D==A && E==F && G==H ], cost: 1
      2: start -> cut : D'=-1+D, [ A>=0 && B==C && D==A && E==F && G==H ], cost: 1
      3: start -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=C && A>=0 && B==C && D==A && E==F && G==H ], cost: 1
      6: lbl42 -> lbl42 : B'=-1+B, [ B>=0 && D>=0 && A>=D && G==H ], cost: 1
      7: lbl42 -> cut : D'=-1+D, [ 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
      8: lbl42 -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
     10: cut -> lbl42 : B'=-1+B, [ D>=0 && B>=0 && A>=1+D && G==H ], cost: 1
     11: cut -> cut : D'=-1+D, [ D>=0 && A>=1+D && G==H ], cost: 1
     12: cut -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && D>=0 && A>=1+D && G==H ], cost: 1
      4: lbl72 -> cut : [ A>=1+D && 1+D>=0 && 1+H>=B && 1+E==B && G==H ], cost: 1
      5: lbl72 -> lbl72 : B'=1+B, E'=B, [ H>=B && A>=1+D && 1+D>=0 && 1+E==B && G==H ], cost: 1
     13: start0 -> start : B'=C, D'=A, E'=F, G'=H, [], cost: 1

Eliminating 1 self-loops for location lbl42
  Self-Loop 6 has the metering function: 1+B, resulting in the new transition 14.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location cut
  Self-Loop 11 has the metering function: 1+D, resulting in the new transition 15.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location lbl72
  Self-Loop 5 has the metering function: 1+H-B, resulting in the new transition 16.
  Removing the self-loops: 5.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      1: start -> lbl42 : B'=-1+B, [ A>=0 && C>=0 && B==C && D==A && E==F && G==H ], cost: 1
      2: start -> cut : D'=-1+D, [ A>=0 && B==C && D==A && E==F && G==H ], cost: 1
      3: start -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=C && A>=0 && B==C && D==A && E==F && G==H ], cost: 1
     14: lbl42 -> [6] : B'=-1, [ B>=0 && D>=0 && A>=D && G==H ], cost: 1+B
     15: cut -> [7] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     16: lbl72 -> [8] : B'=1+H, E'=H, [ H>=B && A>=1+D && 1+D>=0 && 1+E==B && G==H ], cost: 1+H-B
     13: start0 -> start : B'=C, D'=A, E'=F, G'=H, [], cost: 1
      7: [6] -> cut : D'=-1+D, [ 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
      8: [6] -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
     10: [7] -> lbl42 : B'=-1+B, [ D>=0 && B>=0 && A>=1+D && G==H ], cost: 1
     12: [7] -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && D>=0 && A>=1+D && G==H ], cost: 1
      4: [8] -> cut : [ A>=1+D && 1+D>=0 && 1+H>=B && 1+E==B && G==H ], cost: 1


Applied simple chaining:
  Start location: start0
      1: start -> lbl42 : B'=-1+B, [ A>=0 && C>=0 && B==C && D==A && E==F && G==H ], cost: 1
      2: start -> cut : D'=-1+D, [ A>=0 && B==C && D==A && E==F && G==H ], cost: 1
      3: start -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=C && A>=0 && B==C && D==A && E==F && G==H ], cost: 1
     14: lbl42 -> [6] : B'=-1, [ B>=0 && D>=0 && A>=D && G==H ], cost: 1+B
     15: cut -> [7] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     16: lbl72 -> cut : B'=1+H, E'=H, [ H>=B && A>=1+D && 1+D>=0 && 1+E==B && G==H && A>=1+D && 1+D>=0 && 1+H>=1+H && 1+H==1+H && G==H ], cost: 2+H-B
     13: start0 -> start : B'=C, D'=A, E'=F, G'=H, [], cost: 1
      7: [6] -> cut : D'=-1+D, [ 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
      8: [6] -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && 1+B>=0 && D>=0 && A>=D && G==H ], cost: 1
     10: [7] -> lbl42 : B'=-1+B, [ D>=0 && B>=0 && A>=1+D && G==H ], cost: 1
     12: [7] -> lbl72 : B'=1+B, D'=-1+D, E'=B, [ H>=B && D>=0 && A>=1+D && G==H ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     20: lbl42 -> cut : B'=-1, D'=-1+D, [ B>=0 && D>=0 && A>=D && G==H && 0>=0 && D>=0 && A>=D && G==H ], cost: 2+B
     21: lbl42 -> lbl72 : B'=0, D'=-1+D, E'=-1, [ B>=0 && D>=0 && A>=D && G==H && H>=-1 && 0>=0 && D>=0 && A>=D && G==H ], cost: 2+B
     22: cut -> [9] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     23: cut -> [10] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     16: lbl72 -> cut : B'=1+H, E'=H, [ H>=B && A>=1+D && 1+D>=0 && 1+E==B && G==H && A>=1+D && 1+D>=0 && 1+H>=1+H && 1+H==1+H && G==H ], cost: 2+H-B
     17: start0 -> lbl42 : B'=-1+C, D'=A, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H ], cost: 2
     18: start0 -> cut : B'=C, D'=-1+A, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H ], cost: 2
     19: start0 -> lbl72 : B'=1+C, D'=-1+A, E'=C, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H ], cost: 2


Applied chaining over branches and pruning:
  Start location: start0
     22: cut -> [9] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     23: cut -> [10] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     16: lbl72 -> cut : B'=1+H, E'=H, [ H>=B && A>=1+D && 1+D>=0 && 1+E==B && G==H && A>=1+D && 1+D>=0 && 1+H>=1+H && 1+H==1+H && G==H ], cost: 2+H-B
     18: start0 -> cut : B'=C, D'=-1+A, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H ], cost: 2
     24: start0 -> cut : B'=-1, D'=-1+A, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H ], cost: 3+C
     19: start0 -> lbl72 : B'=1+C, D'=-1+A, E'=C, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H ], cost: 2
     25: start0 -> lbl72 : B'=0, D'=-1+A, E'=-1, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H ], cost: 3+C


Applied chaining over branches and pruning:
  Start location: start0
     22: cut -> [9] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     23: cut -> [10] : D'=-1, [ D>=0 && A>=1+D && G==H ], cost: 1+D
     18: start0 -> cut : B'=C, D'=-1+A, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H ], cost: 2
     24: start0 -> cut : B'=-1, D'=-1+A, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H ], cost: 3+C
     26: start0 -> cut : B'=1+H, D'=-1+A, E'=H, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H && H>=1+C && A>=A && A>=0 && 1+C==1+C && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H ], cost: 3+H-C
     27: start0 -> cut : B'=1+H, D'=-1+A, E'=H, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H && H>=0 && A>=A && A>=0 && 0==0 && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H ], cost: 5+H+C


Applied chaining over branches and pruning:
  Start location: start0
     28: start0 -> [9] : B'=C, D'=-1, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H ], cost: 2+A
     30: start0 -> [9] : B'=-1, D'=-1, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+C+A
     32: start0 -> [9] : B'=1+H, D'=-1, E'=H, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H && H>=1+C && A>=A && A>=0 && 1+C==1+C && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+H-C+A
     34: start0 -> [9] : B'=1+H, D'=-1, E'=H, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H && H>=0 && A>=A && A>=0 && 0==0 && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 5+H+C+A
     29: start0 -> [10] : B'=C, D'=-1, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H ], cost: 2+A
     31: start0 -> [10] : B'=-1, D'=-1, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+C+A
     33: start0 -> [10] : B'=1+H, D'=-1, E'=H, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H && H>=1+C && A>=A && A>=0 && 1+C==1+C && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+H-C+A
     35: start0 -> [10] : B'=1+H, D'=-1, E'=H, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H && H>=0 && A>=A && A>=0 && 0==0 && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 5+H+C+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
     28: start0 -> [9] : B'=C, D'=-1, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H ], cost: 2+A
     30: start0 -> [9] : B'=-1, D'=-1, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+C+A
     32: start0 -> [9] : B'=1+H, D'=-1, E'=H, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H && H>=1+C && A>=A && A>=0 && 1+C==1+C && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+H-C+A
     34: start0 -> [9] : B'=1+H, D'=-1, E'=H, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H && H>=0 && A>=A && A>=0 && 0==0 && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 5+H+C+A
     29: start0 -> [10] : B'=C, D'=-1, E'=F, G'=H, [ A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H ], cost: 2+A
     31: start0 -> [10] : B'=-1, D'=-1, E'=F, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && 0>=0 && A>=0 && A>=A && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+C+A
     33: start0 -> [10] : B'=1+H, D'=-1, E'=H, G'=H, [ H>=C && A>=0 && C==C && A==A && F==F && H==H && H>=1+C && A>=A && A>=0 && 1+C==1+C && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 3+H-C+A
     35: start0 -> [10] : B'=1+H, D'=-1, E'=H, G'=H, [ A>=0 && C>=0 && C==C && A==A && F==F && H==H && -1+C>=0 && A>=0 && A>=A && H==H && H>=-1 && 0>=0 && A>=0 && A>=A && H==H && H>=0 && A>=A && A>=0 && 0==0 && H==H && A>=A && A>=0 && 1+H>=1+H && 1+H==1+H && H==H && -1+A>=0 && A>=A && H==H ], cost: 5+H+C+A


Computing complexity for remaining 8 transitions.

  Found configuration with infinitely models for cost: 2+A
  and guard: A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H:
  H: Both, F: Both, C: Both, A: Pos

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


The final runtime is determined by this resulting transition:
  Final Guard: A>=0 && C==C && A==A && F==F && H==H && -1+A>=0 && A>=A && H==H
  Final Cost:  2+A

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),?)