Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
      1: f15 -> f25 : G'=free_1, H'=1, [ A>=1+F ], cost: 1
      8: f15 -> f48 : [ F>=A ], cost: 1
      7: f25 -> f15 : E'=-1+E, F'=1+F, [ H>=E ], cost: 1
      2: f25 -> f25 : G'=free_2, H'=1+H, [ E>=1+H ], cost: 1
      5: f25 -> f41 : [ H>=E && free_3>=1+free_4 ], cost: 1
      6: f25 -> f41 : [ H>=E ], cost: 1
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1

Removing duplicate transition: 5.

Simplified the transitions:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
      1: f15 -> f25 : G'=free_1, H'=1, [ A>=1+F ], cost: 1
      7: f25 -> f15 : E'=-1+E, F'=1+F, [ H>=E ], cost: 1
      2: f25 -> f25 : G'=free_2, H'=1+H, [ E>=1+H ], cost: 1
      6: f25 -> f41 : [ H>=E ], cost: 1
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1

Eliminating 1 self-loops for location f25
  Self-Loop 2 has the metering function: -H+E, resulting in the new transition 9.
  Removing the self-loops: 2.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
      1: f15 -> f25 : G'=free_1, H'=1, [ A>=1+F ], cost: 1
      9: f25 -> [5] : G'=free_2, H'=E, [ E>=1+H ], cost: -H+E
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1
      7: [5] -> f15 : E'=-1+E, F'=1+F, [ H>=E ], cost: 1
      6: [5] -> f41 : [ H>=E ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
      1: f15 -> [5] : G'=free_2, H'=E, [ A>=1+F && E>=2 ], cost: E
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1
      7: [5] -> f15 : E'=-1+E, F'=1+F, [ H>=E ], cost: 1
      6: [5] -> f41 : [ H>=E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
     10: f15 -> f15 : E'=-1+E, F'=1+F, G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E ], cost: 1+E
     11: f15 -> f41 : G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E ], cost: 1+E
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1

Eliminating 1 self-loops for location f15
  Removing the self-loops: 10 12 13.
Adding an epsilon transition (to model nonexecution of the loops): 15.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
     14: f15 -> [6] : E'=-1+E, F'=1+F, G'=free_2, H'=E, [ A>=1+F && E>=2 ], cost: 1+E
     15: f15 -> [6] : [], cost: 0
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1
     11: [6] -> f41 : G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E ], cost: 1+E


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
     16: f15 -> f41 : E'=-1+E, F'=1+F, G'=free_2, H'=-1+E, [ A>=1+F && E>=2 && A>=2+F && -1+E>=2 && -1+E>=-1+E ], cost: 1+2*E
     17: f15 -> f41 : G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E ], cost: 1+E
      3: f41 -> f15 : F'=1+F, [ E>=B ], cost: 1
      4: f41 -> f15 : E'=1+E, F'=1+F, [ B>=1+E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
     18: f15 -> f15 : E'=-1+E, F'=2+F, G'=free_2, H'=-1+E, [ A>=1+F && E>=2 && A>=2+F && -1+E>=2 && -1+E>=-1+E && -1+E>=B ], cost: 2+2*E
     19: f15 -> f15 : E'=E, F'=2+F, G'=free_2, H'=-1+E, [ A>=1+F && E>=2 && A>=2+F && -1+E>=2 && -1+E>=-1+E && B>=E ], cost: 2+2*E
     20: f15 -> f15 : F'=1+F, G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E && E>=B ], cost: 2+E
     21: f15 -> f15 : E'=1+E, F'=1+F, G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=E && B>=1+E ], cost: 2+E

Eliminating 4 self-loops for location f15
  Self-Loop 19 has the metering function: meter, resulting in the new transition 25.
  Self-Loop 20 has the metering function: -F+A, resulting in the new transition 26.
  Found this metering function when nesting loops: -1+E-B,
  and nested parallel self-loops 24 (outer loop) and 25 (inner loop), obtaining the new transitions: 28.
  Found this metering function when nesting loops: -1-E+B,
  Removing the self-loops: 18 19 20 21 22 23 24.
Adding an epsilon transition (to model nonexecution of the loops): 29.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=10, B'=35, C'=285, D'=free, E'=free, F'=0, [], cost: 1
     25: f15 -> [7] : F'=2*meter+F, G'=free_2, H'=-1+E, [ A>=2+F && -1+E>=2 && B>=E && 2*meter==-1-F+A ], cost: 2*meter+2*meter*E
     26: f15 -> [7] : F'=A, G'=free_2, H'=E, [ A>=1+F && E>=2 && E>=B ], cost: -E*(F-A)-2*F+2*A
     27: f15 -> [7] : E'=1+E, F'=1+F, G'=free_2, H'=E, [ A>=1+F && E>=2 && B>=1+E ], cost: 2+E
     28: f15 -> [7] : E'=1+B, F'=-2+2*E-2*B+2*meter*(-1+E-B)+F, G'=free_2, H'=B, [ A>=2+F && -1+E>=2 && -1+E>=B && A>=4+F && -2+E>=2 && B>=-1+E && 2*meter==-3-F+A ], cost: -3+3*E-meter*(-1+E-B)^2-3*B+meter*(-1+E-B)-(-1+E-B)^2+2*(-1+E-B)*E+2*meter*(-1+E-B)*E
     29: f15 -> [7] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: f0
     30: f0 -> [7] : A'=10, B'=35, C'=285, D'=free, E'=free, F'=10, G'=free_2, H'=free, [ 10>=1 && free>=2 && free>=35 ], cost: 21+10*free
     31: f0 -> [7] : A'=10, B'=35, C'=285, D'=free, E'=1+free, F'=1, G'=free_2, H'=free, [ 10>=1 && free>=2 && 35>=1+free ], cost: 3+free


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     30: f0 -> [7] : A'=10, B'=35, C'=285, D'=free, E'=free, F'=10, G'=free_2, H'=free, [ 10>=1 && free>=2 && free>=35 ], cost: 21+10*free
     31: f0 -> [7] : A'=10, B'=35, C'=285, D'=free, E'=1+free, F'=1, G'=free_2, H'=free, [ 10>=1 && free>=2 && 35>=1+free ], cost: 3+free


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 21+10*free
  and guard: 10>=1 && free>=2 && free>=35:
  free: Pos

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: 10>=1 && free>=2 && free>=35
  Final Cost:  21+10*free

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

WORST_CASE(INF,?)