Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubbleentryin : [], cost: 1
      1: evalrealbubbleentryin -> evalrealbubblebb7in : A'=-1+A, [], cost: 1
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
      3: evalrealbubblebb7in -> evalrealbubblereturnin : [ 0>=A ], cost: 1
      4: evalrealbubblebb4in -> evalrealbubblebb1in : [ A>=1+B ], cost: 1
      5: evalrealbubblebb4in -> evalrealbubblebb5in : [ B>=A ], cost: 1
     14: evalrealbubblereturnin -> evalrealbubblestop : [], cost: 1
      6: evalrealbubblebb1in -> evalrealbubblebb2in : [ free>=1+free_1 ], cost: 1
      7: evalrealbubblebb1in -> evalrealbubblebb3in : D'=C, [ free_3>=free_2 ], cost: 1
     10: evalrealbubblebb5in -> evalrealbubblereturnin : [ C==0 ], cost: 1
     11: evalrealbubblebb5in -> evalrealbubblebb6in : [ 0>=1+C ], cost: 1
     12: evalrealbubblebb5in -> evalrealbubblebb6in : [ C>=1 ], cost: 1
      8: evalrealbubblebb2in -> evalrealbubblebb3in : D'=1, [], cost: 1
      9: evalrealbubblebb3in -> evalrealbubblebb4in : B'=1+B, C'=D, [], cost: 1
     13: evalrealbubblebb6in -> evalrealbubblebb7in : A'=-1+A, [], cost: 1


Simplified the transitions:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubbleentryin : [], cost: 1
      1: evalrealbubbleentryin -> evalrealbubblebb7in : A'=-1+A, [], cost: 1
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
      4: evalrealbubblebb4in -> evalrealbubblebb1in : [ A>=1+B ], cost: 1
      5: evalrealbubblebb4in -> evalrealbubblebb5in : [ B>=A ], cost: 1
      6: evalrealbubblebb1in -> evalrealbubblebb2in : [], cost: 1
      7: evalrealbubblebb1in -> evalrealbubblebb3in : D'=C, [], cost: 1
     11: evalrealbubblebb5in -> evalrealbubblebb6in : [ 0>=1+C ], cost: 1
     12: evalrealbubblebb5in -> evalrealbubblebb6in : [ C>=1 ], cost: 1
      8: evalrealbubblebb2in -> evalrealbubblebb3in : D'=1, [], cost: 1
      9: evalrealbubblebb3in -> evalrealbubblebb4in : B'=1+B, C'=D, [], cost: 1
     13: evalrealbubblebb6in -> evalrealbubblebb7in : A'=-1+A, [], cost: 1


Applied simple chaining:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
      4: evalrealbubblebb4in -> evalrealbubblebb1in : [ A>=1+B ], cost: 1
      5: evalrealbubblebb4in -> evalrealbubblebb5in : [ B>=A ], cost: 1
      7: evalrealbubblebb1in -> evalrealbubblebb3in : D'=C, [], cost: 1
      6: evalrealbubblebb1in -> evalrealbubblebb3in : D'=1, [], cost: 2
     11: evalrealbubblebb5in -> evalrealbubblebb6in : [ 0>=1+C ], cost: 1
     12: evalrealbubblebb5in -> evalrealbubblebb6in : [ C>=1 ], cost: 1
      9: evalrealbubblebb3in -> evalrealbubblebb4in : B'=1+B, C'=D, [], cost: 1
     13: evalrealbubblebb6in -> evalrealbubblebb7in : A'=-1+A, [], cost: 1


Applied chaining over branches and pruning:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
     15: evalrealbubblebb4in -> evalrealbubblebb3in : D'=C, [ A>=1+B ], cost: 2
     16: evalrealbubblebb4in -> evalrealbubblebb3in : D'=1, [ A>=1+B ], cost: 3
     17: evalrealbubblebb4in -> evalrealbubblebb6in : [ B>=A && 0>=1+C ], cost: 2
     18: evalrealbubblebb4in -> evalrealbubblebb6in : [ B>=A && C>=1 ], cost: 2
      9: evalrealbubblebb3in -> evalrealbubblebb4in : B'=1+B, C'=D, [], cost: 1
     13: evalrealbubblebb6in -> evalrealbubblebb7in : A'=-1+A, [], cost: 1


Applied chaining over branches and pruning:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
     21: evalrealbubblebb4in -> evalrealbubblebb7in : A'=-1+A, [ B>=A && 0>=1+C ], cost: 3
     22: evalrealbubblebb4in -> evalrealbubblebb7in : A'=-1+A, [ B>=A && C>=1 ], cost: 3
     19: evalrealbubblebb4in -> evalrealbubblebb4in : B'=1+B, C'=C, D'=C, [ A>=1+B ], cost: 3
     20: evalrealbubblebb4in -> evalrealbubblebb4in : B'=1+B, C'=1, D'=1, [ A>=1+B ], cost: 4

Eliminating 2 self-loops for location evalrealbubblebb4in
  Self-Loop 19 has the metering function: -B+A, resulting in the new transition 23.
  Self-Loop 20 has the metering function: -B+A, resulting in the new transition 24.
  Removing the self-loops: 19 20.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
      2: evalrealbubblebb7in -> evalrealbubblebb4in : B'=0, C'=0, [ A>=1 ], cost: 1
     23: evalrealbubblebb4in -> [11] : B'=A, D'=C, [ A>=1+B ], cost: -3*B+3*A
     24: evalrealbubblebb4in -> [11] : B'=A, C'=1, D'=1, [ A>=1+B ], cost: -4*B+4*A
     21: [11] -> evalrealbubblebb7in : A'=-1+A, [ B>=A && 0>=1+C ], cost: 3
     22: [11] -> evalrealbubblebb7in : A'=-1+A, [ B>=A && C>=1 ], cost: 3


Applied chaining over branches and pruning:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
     25: evalrealbubblebb7in -> [11] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     26: evalrealbubblebb7in -> [11] : B'=A, C'=1, D'=1, [ A>=1 && A>=1 ], cost: 1+4*A
     21: [11] -> evalrealbubblebb7in : A'=-1+A, [ B>=A && 0>=1+C ], cost: 3
     22: [11] -> evalrealbubblebb7in : A'=-1+A, [ B>=A && C>=1 ], cost: 3


Applied chaining over branches and pruning:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
     30: evalrealbubblebb7in -> evalrealbubblebb7in : A'=-1+A, B'=A, C'=1, D'=1, [ A>=1 && A>=1 && A>=A && 1>=1 ], cost: 4+4*A
     27: evalrealbubblebb7in -> [12] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     28: evalrealbubblebb7in -> [13] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     29: evalrealbubblebb7in -> [14] : B'=A, C'=1, D'=1, [ A>=1 && A>=1 ], cost: 1+4*A

Eliminating 1 self-loops for location evalrealbubblebb7in
  Self-Loop 30 has the metering function: A, resulting in the new transition 31.
  Removing the self-loops: 30.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> evalrealbubblebb7in : A'=-1+A, [], cost: 2
     31: evalrealbubblebb7in -> [15] : A'=0, B'=1, C'=1, D'=1, [ A>=1 ], cost: 2*A^2+6*A
     27: [15] -> [12] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     28: [15] -> [13] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     29: [15] -> [14] : B'=A, C'=1, D'=1, [ A>=1 && A>=1 ], cost: 1+4*A


Applied simple chaining:
  Start location: evalrealbubblestart
      0: evalrealbubblestart -> [15] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A
     27: [15] -> [12] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     28: [15] -> [13] : B'=A, C'=0, D'=0, [ A>=1 && A>=1 ], cost: 1+3*A
     29: [15] -> [14] : B'=A, C'=1, D'=1, [ A>=1 && A>=1 ], cost: 1+4*A


Applied chaining over branches and pruning:
  Start location: evalrealbubblestart
     32: evalrealbubblestart -> [16] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A
     33: evalrealbubblestart -> [17] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A
     34: evalrealbubblestart -> [18] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalrealbubblestart
     32: evalrealbubblestart -> [16] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A
     33: evalrealbubblestart -> [17] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A
     34: evalrealbubblestart -> [18] : A'=0, B'=1, C'=1, D'=1, [ -1+A>=1 ], cost: -4+2*(-1+A)^2+6*A


Computing complexity for remaining 3 transitions.

  Found configuration with infinitely models for cost: -4+2*(-1+A)^2+6*A
  and guard: -1+A>=1:
  A: Pos

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


The final runtime is determined by this resulting transition:
  Final Guard: -1+A>=1
  Final Cost:  -4+2*(-1+A)^2+6*A

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

WORST_CASE(Omega(n^2),?)