Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb10in : A'=1, [], cost: 1
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      3: evalfbb10in -> evalfreturnin : [ A>=1+B ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
     13: evalfreturnin -> evalfstop : [], cost: 1
      6: evalfbb6in -> evalfbb4in : E'=1, [ B>=D ], cost: 1
      7: evalfbb6in -> evalfbb7in : [ D>=1+B ], cost: 1
      8: evalfbb4in -> evalfbb3in : [ D>=E ], cost: 1
      9: evalfbb4in -> evalfbb5in : [ E>=1+D ], cost: 1
     12: evalfbb7in -> evalfbb8in : C'=1+C, [], cost: 1
     10: evalfbb3in -> evalfbb4in : E'=1+E, [], cost: 1
     11: evalfbb5in -> evalfbb6in : D'=1+D, [], cost: 1


Simplified the transitions:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb10in : A'=1, [], cost: 1
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
      6: evalfbb6in -> evalfbb4in : E'=1, [ B>=D ], cost: 1
      7: evalfbb6in -> evalfbb7in : [ D>=1+B ], cost: 1
      8: evalfbb4in -> evalfbb3in : [ D>=E ], cost: 1
      9: evalfbb4in -> evalfbb5in : [ E>=1+D ], cost: 1
     12: evalfbb7in -> evalfbb8in : C'=1+C, [], cost: 1
     10: evalfbb3in -> evalfbb4in : E'=1+E, [], cost: 1
     11: evalfbb5in -> evalfbb6in : D'=1+D, [], cost: 1


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
      7: evalfbb6in -> evalfbb8in : C'=1+C, [ D>=1+B ], cost: 2
      6: evalfbb6in -> evalfbb4in : E'=1, [ B>=D ], cost: 1
      9: evalfbb4in -> evalfbb6in : D'=1+D, [ E>=1+D ], cost: 2
      8: evalfbb4in -> evalfbb4in : E'=1+E, [ D>=E ], cost: 2

Eliminating 1 self-loops for location evalfbb4in
  Self-Loop 8 has the metering function: 1-E+D, resulting in the new transition 14.
  Removing the self-loops: 8.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
      7: evalfbb6in -> evalfbb8in : C'=1+C, [ D>=1+B ], cost: 2
      6: evalfbb6in -> evalfbb4in : E'=1, [ B>=D ], cost: 1
     14: evalfbb4in -> [11] : E'=1+D, [ D>=E ], cost: 2-2*E+2*D
      9: [11] -> evalfbb6in : D'=1+D, [ E>=1+D ], cost: 2


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
      7: evalfbb6in -> evalfbb8in : C'=1+C, [ D>=1+B ], cost: 2
      6: evalfbb6in -> evalfbb6in : D'=1+D, E'=1+D, [ B>=D && D>=1 && 1+D>=1+D ], cost: 3+2*D

Eliminating 1 self-loops for location evalfbb6in
  Self-Loop 6 has the metering function: 1+B-D, resulting in the new transition 15.
  Removing the self-loops: 6.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb6in : D'=1+A, [ A>=C ], cost: 1
     15: evalfbb6in -> [12] : D'=1+B, E'=1+B, [ B>=D && D>=1 ], cost: 2+(1+B-D)^2+2*B+2*(1+B-D)*D-2*D
      7: [12] -> evalfbb8in : C'=1+C, [ D>=1+B ], cost: 2


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
      5: evalfbb8in -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1
      4: evalfbb8in -> evalfbb8in : C'=1+C, D'=1+B, E'=1+B, [ A>=C && B>=1+A && 1+A>=1 && 1+B>=1+B ], cost: 3+2*B+(B-A)^2+2*(B-A)*(1+A)-2*A

Eliminating 1 self-loops for location evalfbb8in
  Self-Loop 4 has the metering function: 1-C+A, resulting in the new transition 16.
  Removing the self-loops: 4.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb8in : C'=1, [ B>=A ], cost: 1
     16: evalfbb8in -> [13] : C'=1+A, D'=1+B, E'=1+B, [ A>=C && B>=1+A && 1+A>=1 ], cost: 3-B^2*(-1+C-A)+4*(-1+C-A)*A-3*C-4*B*(-1+C-A)+3*A+(-1+C-A)*A^2
      5: [13] -> evalfbb10in : A'=1+A, [ C>=1+A ], cost: 1


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
      2: evalfbb10in -> evalfbb10in : A'=1+A, C'=1+A, D'=1+B, E'=1+B, [ B>=A && A>=1 && B>=1+A && 1+A>=1 && 1+A>=1+A ], cost: 2-A^3-4*A^2+B^2*A+4*B*A+3*A

Eliminating 1 self-loops for location evalfbb10in
  Self-Loop 2 has the metering function: B-A, resulting in the new transition 17.
  Removing the self-loops: 2.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb10in : A'=1, [], cost: 2
     17: evalfbb10in -> [14] : A'=B, C'=B, D'=1+B, E'=1+B, [ A>=1 && B>=1+A ], cost: -(B-A)^3*A+2*(B-A)^2*B-3/2*(B-A)^2*A^2-1/6*B+4*(B-A)*B*A-5/2*(B-A)^2*A+1/2*(B-A)^2*B^2+13/4*(B-A)^2-5/6*(B-A)^3-1/4*(B-A)^4+(B-A)*B^2*A+13/2*(B-A)*A-1/2*(B-A)*B^2-2*(B-A)*B-5/2*(B-A)*A^2+1/6*A-(B-A)*A^3


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> [14] : A'=B, C'=B, D'=1+B, E'=1+B, [ 1>=1 && B>=2 ], cost: -5/6-3/4*(-1+B)^2+1/2*B^2*(-1+B)^2-11/6*(-1+B)^3+17/6*B+1/2*B^2*(-1+B)+2*B*(-1+B)-1/4*(-1+B)^4+2*B*(-1+B)^2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalfstart
      0: evalfstart -> [14] : A'=B, C'=B, D'=1+B, E'=1+B, [ 1>=1 && B>=2 ], cost: -5/6-3/4*(-1+B)^2+1/2*B^2*(-1+B)^2-11/6*(-1+B)^3+17/6*B+1/2*B^2*(-1+B)+2*B*(-1+B)-1/4*(-1+B)^4+2*B*(-1+B)^2


Computing complexity for remaining 1 transitions.

  Found configuration with infinitely models for cost: -5/6-3/4*(-1+B)^2+1/2*B^2*(-1+B)^2-11/6*(-1+B)^3+17/6*B+1/2*B^2*(-1+B)+2*B*(-1+B)-1/4*(-1+B)^4+2*B*(-1+B)^2
  and guard: 1>=1 && B>=2:
  B: Pos

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


The final runtime is determined by this resulting transition:
  Final Guard: 1>=1 && B>=2
  Final Cost:  -5/6-3/4*(-1+B)^2+1/2*B^2*(-1+B)^2-11/6*(-1+B)^3+17/6*B+1/2*B^2*(-1+B)+2*B*(-1+B)-1/4*(-1+B)^4+2*B*(-1+B)^2

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

WORST_CASE(Omega(n^4),?)