Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 1
      2: evalfbb5in -> evalfreturnin : [ C>=D ], cost: 1
      3: evalfbb5in -> evalfbbin : E'=1+C, [ D>=1+C ], cost: 1
     11: evalfreturnin -> evalfstop : [], cost: 1
      4: evalfbbin -> evalfbb1in : F'=B, [ 0>=1+free ], cost: 1
      5: evalfbbin -> evalfbb1in : F'=B, [ free_1>=1 ], cost: 1
      6: evalfbbin -> evalfbb3in : F'=A, [], cost: 1
      7: evalfbb1in -> evalfbb5in : B'=1+F, C'=E, [ F>=G ], cost: 1
      8: evalfbb1in -> evalfbb1in : F'=1+F, [ G>=1+F ], cost: 1
      9: evalfbb3in -> evalfbb5in : A'=1+F, C'=E, [ F>=G ], cost: 1
     10: evalfbb3in -> evalfbb3in : F'=1+F, [ G>=1+F ], cost: 1

Removing duplicate transition: 4.

Simplified the transitions:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 1
      3: evalfbb5in -> evalfbbin : E'=1+C, [ D>=1+C ], cost: 1
      5: evalfbbin -> evalfbb1in : F'=B, [], cost: 1
      6: evalfbbin -> evalfbb3in : F'=A, [], cost: 1
      7: evalfbb1in -> evalfbb5in : B'=1+F, C'=E, [ F>=G ], cost: 1
      8: evalfbb1in -> evalfbb1in : F'=1+F, [ G>=1+F ], cost: 1
      9: evalfbb3in -> evalfbb5in : A'=1+F, C'=E, [ F>=G ], cost: 1
     10: evalfbb3in -> evalfbb3in : F'=1+F, [ G>=1+F ], cost: 1

Eliminating 1 self-loops for location evalfbb1in
  Self-Loop 8 has the metering function: -F+G, resulting in the new transition 12.
  Removing the self-loops: 8.
Eliminating 1 self-loops for location evalfbb3in
  Self-Loop 10 has the metering function: -F+G, resulting in the new transition 13.
  Removing the self-loops: 10.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 1
      3: evalfbb5in -> evalfbbin : E'=1+C, [ D>=1+C ], cost: 1
      5: evalfbbin -> evalfbb1in : F'=B, [], cost: 1
      6: evalfbbin -> evalfbb3in : F'=A, [], cost: 1
     12: evalfbb1in -> [8] : F'=G, [ G>=1+F ], cost: -F+G
     13: evalfbb3in -> [9] : F'=G, [ G>=1+F ], cost: -F+G
      7: [8] -> evalfbb5in : B'=1+F, C'=E, [ F>=G ], cost: 1
      9: [9] -> evalfbb5in : A'=1+F, C'=E, [ F>=G ], cost: 1


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 2
      3: evalfbb5in -> evalfbbin : E'=1+C, [ D>=1+C ], cost: 1
      5: evalfbbin -> evalfbb5in : B'=1+G, C'=E, F'=G, [ G>=1+B && G>=G ], cost: 2-B+G
      6: evalfbbin -> evalfbb5in : A'=1+G, C'=E, F'=G, [ G>=1+A && G>=G ], cost: 2+G-A


Applied chaining over branches and pruning:
  Start location: evalfstart
      0: evalfstart -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 2
     14: evalfbb5in -> evalfbb5in : B'=1+G, C'=1+C, E'=1+C, F'=G, [ D>=1+C && G>=1+B && G>=G ], cost: 3-B+G
     15: evalfbb5in -> evalfbb5in : A'=1+G, C'=1+C, E'=1+C, F'=G, [ D>=1+C && G>=1+A && G>=G ], cost: 3+G-A

Eliminating 2 self-loops for location evalfbb5in
  Removing the self-loops: 14 15.
Adding an epsilon transition (to model nonexecution of the loops): 18.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb5in : A'=0, B'=0, C'=0, [], cost: 2
     16: evalfbb5in -> [10] : B'=1+G, C'=1+C, E'=1+C, F'=G, [ D>=1+C && G>=1+B ], cost: 3-B+G
     17: evalfbb5in -> [10] : A'=1+G, C'=1+C, E'=1+C, F'=G, [ D>=1+C && G>=1+A ], cost: 3+G-A
     18: evalfbb5in -> [10] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: evalfstart
     19: evalfstart -> [10] : A'=0, B'=1+G, C'=1, E'=1, F'=G, [ D>=1 && G>=1 ], cost: 5+G
     20: evalfstart -> [10] : A'=1+G, B'=0, C'=1, E'=1, F'=G, [ D>=1 && G>=1 ], cost: 5+G


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalfstart
     19: evalfstart -> [10] : A'=0, B'=1+G, C'=1, E'=1, F'=G, [ D>=1 && G>=1 ], cost: 5+G
     20: evalfstart -> [10] : A'=1+G, B'=0, C'=1, E'=1, F'=G, [ D>=1 && G>=1 ], cost: 5+G


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 5+G
  and guard: D>=1 && G>=1:
  G: Pos, D: Pos

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


The final runtime is determined by this resulting transition:
  Final Guard: D>=1 && G>=1
  Final Cost:  5+G

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