Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
      1: f5 -> f9 : C'=0, [ A>=1+B ], cost: 1
     20: f5 -> f1 : [ B>=A && 0>=1+free_14 ], cost: 1
     21: f5 -> f1 : [ B>=A && free_15>=1 ], cost: 1
     22: f5 -> f1 : [ B>=A ], cost: 1
     17: f9 -> f5 : B'=1+B, C'=0, R'=0, [ D>=1+A && C==0 ], cost: 1
      2: f9 -> f9 : D'=1+D, E'=C, F'=free, G'=free, [ C>=1+free && A>=D ], cost: 1
      3: f9 -> f9 : C'=free_1, D'=1+D, E'=C, F'=free_1, G'=free_1, [ free_1>=C && A>=D ], cost: 1
     18: f9 -> f26 : [ 0>=1+C && D>=1+A ], cost: 1
     19: f9 -> f26 : [ C>=1 && D>=1+A ], cost: 1
      4: f26 -> f26 : D'=1+D, [ A>=D ], cost: 1
     16: f26 -> f32 : [ D>=1+A ], cost: 1
      5: f32 -> f32 : D'=1+D, H'=0, Q'=0, [ A>=D ], cost: 1
      6: f32 -> f32 : D'=1+D, H'=free_2, Q'=free_3, J'=free_3+J, [ 0>=1+free_2 && A>=D ], cost: 1
      7: f32 -> f32 : D'=1+D, H'=free_4, Q'=free_5, J'=free_5+J, [ free_4>=1 && A>=D ], cost: 1
     14: f32 -> f52 : M'=free_8, N'=free_9, O'=free_9, [ free_10>=0 && D>=1+A ], cost: 1
     15: f32 -> f52 : O'=-free_11, P'=free_12, Q_1'=free_11, [ 0>=1+free_13 && D>=1+A ], cost: 1
     13: f52 -> f5 : B'=1+B, [ K>=1+A ], cost: 1
      8: f52 -> f55 : [ A>=K ], cost: 1
      9: f55 -> f55 : D'=1+D, J'=free_6, [ A>=D ], cost: 1
     12: f55 -> f62 : L'=free_7, [ D>=1+A ], cost: 1
     11: f62 -> f52 : K'=1+K, [ D>=1+A ], cost: 1
     10: f62 -> f62 : D'=1+D, [ A>=D ], cost: 1


Simplified the transitions:
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
      1: f5 -> f9 : C'=0, [ A>=1+B ], cost: 1
     17: f9 -> f5 : B'=1+B, C'=0, R'=0, [ D>=1+A && C==0 ], cost: 1
      2: f9 -> f9 : D'=1+D, E'=C, F'=free, G'=free, [ C>=1+free && A>=D ], cost: 1
      3: f9 -> f9 : C'=free_1, D'=1+D, E'=C, F'=free_1, G'=free_1, [ free_1>=C && A>=D ], cost: 1
     18: f9 -> f26 : [ 0>=1+C && D>=1+A ], cost: 1
     19: f9 -> f26 : [ C>=1 && D>=1+A ], cost: 1
      4: f26 -> f26 : D'=1+D, [ A>=D ], cost: 1
     16: f26 -> f32 : [ D>=1+A ], cost: 1
      5: f32 -> f32 : D'=1+D, H'=0, Q'=0, [ A>=D ], cost: 1
      6: f32 -> f32 : D'=1+D, H'=free_2, Q'=free_3, J'=free_3+J, [ 0>=1+free_2 && A>=D ], cost: 1
      7: f32 -> f32 : D'=1+D, H'=free_4, Q'=free_5, J'=free_5+J, [ free_4>=1 && A>=D ], cost: 1
     14: f32 -> f52 : M'=free_8, N'=free_9, O'=free_9, [ D>=1+A ], cost: 1
     15: f32 -> f52 : O'=-free_11, P'=free_12, Q_1'=free_11, [ D>=1+A ], cost: 1
     13: f52 -> f5 : B'=1+B, [ K>=1+A ], cost: 1
      8: f52 -> f55 : [ A>=K ], cost: 1
      9: f55 -> f55 : D'=1+D, J'=free_6, [ A>=D ], cost: 1
     12: f55 -> f62 : L'=free_7, [ D>=1+A ], cost: 1
     11: f62 -> f52 : K'=1+K, [ D>=1+A ], cost: 1
     10: f62 -> f62 : D'=1+D, [ A>=D ], cost: 1

Eliminating 2 self-loops for location f9
  Self-Loop 2 has the metering function: 1-D+A, resulting in the new transition 23.
  Self-Loop 3 has the metering function: 1-D+A, resulting in the new transition 24.
  Removing the self-loops: 2 3.
Eliminating 1 self-loops for location f26
  Self-Loop 4 has the metering function: 1-D+A, resulting in the new transition 25.
  Removing the self-loops: 4.
Eliminating 3 self-loops for location f32
  Self-Loop 5 has the metering function: 1-D+A, resulting in the new transition 26.
  Self-Loop 6 has the metering function: 1-D+A, resulting in the new transition 27.
  Self-Loop 7 has the metering function: 1-D+A, resulting in the new transition 28.
  Removing the self-loops: 5 6 7.
Eliminating 1 self-loops for location f55
  Self-Loop 9 has the metering function: 1-D+A, resulting in the new transition 29.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f62
  Self-Loop 10 has the metering function: 1-D+A, resulting in the new transition 30.
  Removing the self-loops: 10.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
      1: f5 -> f9 : C'=0, [ A>=1+B ], cost: 1
     23: f9 -> [9] : D'=1+A, E'=C, F'=free, G'=free, [ C>=1+free && A>=D ], cost: 1-D+A
     24: f9 -> [9] : C'=C, D'=1+A, E'=C, F'=C, G'=C, [ C>=C && A>=D ], cost: 1-D+A
     25: f26 -> [10] : D'=1+A, [ A>=D ], cost: 1-D+A
     26: f32 -> [11] : D'=1+A, H'=0, Q'=0, [ A>=D ], cost: 1-D+A
     27: f32 -> [11] : D'=1+A, H'=free_2, Q'=free_3, J'=-(-1+D-A)*free_3+J, [ 0>=1+free_2 && A>=D ], cost: 1-D+A
     28: f32 -> [11] : D'=1+A, H'=free_4, Q'=free_5, J'=-(-1+D-A)*free_5+J, [ free_4>=1 && A>=D ], cost: 1-D+A
     13: f52 -> f5 : B'=1+B, [ K>=1+A ], cost: 1
      8: f52 -> f55 : [ A>=K ], cost: 1
     29: f55 -> [12] : D'=1+A, J'=free_6, [ A>=D ], cost: 1-D+A
     30: f62 -> [13] : D'=1+A, [ A>=D ], cost: 1-D+A
     17: [9] -> f5 : B'=1+B, C'=0, R'=0, [ D>=1+A && C==0 ], cost: 1
     18: [9] -> f26 : [ 0>=1+C && D>=1+A ], cost: 1
     19: [9] -> f26 : [ C>=1 && D>=1+A ], cost: 1
     16: [10] -> f32 : [ D>=1+A ], cost: 1
     14: [11] -> f52 : M'=free_8, N'=free_9, O'=free_9, [ D>=1+A ], cost: 1
     15: [11] -> f52 : O'=-free_11, P'=free_12, Q_1'=free_11, [ D>=1+A ], cost: 1
     12: [12] -> f62 : L'=free_7, [ D>=1+A ], cost: 1
     11: [13] -> f52 : K'=1+K, [ D>=1+A ], cost: 1


Applied simple chaining:
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
      1: f5 -> f9 : C'=0, [ A>=1+B ], cost: 1
     23: f9 -> [9] : D'=1+A, E'=C, F'=free, G'=free, [ C>=1+free && A>=D ], cost: 1-D+A
     24: f9 -> [9] : C'=C, D'=1+A, E'=C, F'=C, G'=C, [ C>=C && A>=D ], cost: 1-D+A
     25: f26 -> f32 : D'=1+A, [ A>=D && 1+A>=1+A ], cost: 2-D+A
     26: f32 -> [11] : D'=1+A, H'=0, Q'=0, [ A>=D ], cost: 1-D+A
     27: f32 -> [11] : D'=1+A, H'=free_2, Q'=free_3, J'=-(-1+D-A)*free_3+J, [ 0>=1+free_2 && A>=D ], cost: 1-D+A
     28: f32 -> [11] : D'=1+A, H'=free_4, Q'=free_5, J'=-(-1+D-A)*free_5+J, [ free_4>=1 && A>=D ], cost: 1-D+A
     13: f52 -> f5 : B'=1+B, [ K>=1+A ], cost: 1
      8: f52 -> f62 : D'=1+A, J'=free_6, L'=free_7, [ A>=K && A>=D && 1+A>=1+A ], cost: 3-D+A
     30: f62 -> f52 : D'=1+A, K'=1+K, [ A>=D && 1+A>=1+A ], cost: 2-D+A
     17: [9] -> f5 : B'=1+B, C'=0, R'=0, [ D>=1+A && C==0 ], cost: 1
     18: [9] -> f26 : [ 0>=1+C && D>=1+A ], cost: 1
     19: [9] -> f26 : [ C>=1 && D>=1+A ], cost: 1
     14: [11] -> f52 : M'=free_8, N'=free_9, O'=free_9, [ D>=1+A ], cost: 1
     15: [11] -> f52 : O'=-free_11, P'=free_12, Q_1'=free_11, [ D>=1+A ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
     31: f5 -> [9] : C'=0, D'=1+A, E'=0, F'=free, G'=free, [ A>=1+B && 0>=1+free && A>=D ], cost: 2-D+A
     32: f5 -> [9] : C'=0, D'=1+A, E'=0, F'=0, G'=0, [ A>=1+B && 0>=0 && A>=D ], cost: 2-D+A
     17: [9] -> f5 : B'=1+B, C'=0, R'=0, [ D>=1+A && C==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
     33: f5 -> f5 : B'=1+B, C'=0, D'=1+A, E'=0, F'=free, G'=free, R'=0, [ A>=1+B && 0>=1+free && A>=D && 1+A>=1+A && 0==0 ], cost: 3-D+A
     34: f5 -> f5 : B'=1+B, C'=0, D'=1+A, E'=0, F'=0, G'=0, R'=0, [ A>=1+B && 0>=0 && A>=D && 1+A>=1+A && 0==0 ], cost: 3-D+A

Eliminating 2 self-loops for location f5
  Removing the self-loops: 33 34.
Adding an epsilon transition (to model nonexecution of the loops): 37.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      0: f2 -> f5 : [ A>=2 ], cost: 1
     35: f5 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=free, G'=free, R'=0, [ A>=1+B && 0>=1+free && A>=D ], cost: 3-D+A
     36: f5 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=0, G'=0, R'=0, [ A>=1+B && A>=D ], cost: 3-D+A
     37: f5 -> [14] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: f2
     38: f2 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=free, G'=free, R'=0, [ A>=2 && A>=1+B && 0>=1+free && A>=D ], cost: 4-D+A
     39: f2 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=0, G'=0, R'=0, [ A>=2 && A>=1+B && A>=D ], cost: 4-D+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f2
     38: f2 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=free, G'=free, R'=0, [ A>=2 && A>=1+B && 0>=1+free && A>=D ], cost: 4-D+A
     39: f2 -> [14] : B'=1+B, C'=0, D'=1+A, E'=0, F'=0, G'=0, R'=0, [ A>=2 && A>=1+B && A>=D ], cost: 4-D+A


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 4-D+A
  and guard: A>=2 && A>=1+B && 0>=1+free && A>=D:
  B: Pos, free: Neg, D: Pos, A: Pos, where: A > B A > D

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


The final runtime is determined by this resulting transition:
  Final Guard: A>=2 && A>=1+B && 0>=1+free && A>=D
  Final Cost:  4-D+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),?)