Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f23 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [], cost: 1
      1: f23 -> f23 : F'=1+F, [ C>=1+F ], cost: 1
     26: f23 -> f29 : F'=0, [ F>=C ], cost: 1
      2: f29 -> f33 : G'=0, H'=0, [ C>=1+F ], cost: 1
     25: f29 -> f52 : F'=0, [ F>=C ], cost: 1
     24: f33 -> f29 : A'=0, F'=1+F, J'=0, [ H>=C && A==0 ], cost: 1
      3: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ 0>=1+G && C>=1+H ], cost: 1
      4: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ G>=1 && C>=1+H ], cost: 1
      5: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ C>=1+H && G==0 ], cost: 1
      6: f33 -> f33 : G'=0, H'=1+H, Q'=0, [ free_3>=1+free_2 && C>=1+H && G==0 ], cost: 1
      7: f33 -> f33 : G'=0, H'=1+H, Q'=0, [ C>=1+H && G==0 ], cost: 1
     22: f33 -> f44 : [ 0>=1+A && H>=C ], cost: 1
     23: f33 -> f44 : [ A>=1 && H>=C ], cost: 1
      8: f44 -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+G ], cost: 1
      9: f44 -> f29 : A'=1, F'=1+F, J'=1, [ G>=1 ], cost: 1
     10: f44 -> f29 : A'=0, F'=1+F, G'=0, J'=0, [ G==0 ], cost: 1
     15: f52 -> f52 : B'=0, F'=1+F, K'=0, [ C>=2+F && B==0 ], cost: 1
     11: f52 -> f55 : [ 0>=1+B && C>=2+F ], cost: 1
     12: f52 -> f55 : [ B>=1 && C>=2+F ], cost: 1
     19: f52 -> f63 : [ 0>=1+A && 1+F>=C ], cost: 1
     20: f52 -> f63 : [ A>=1 && 1+F>=C ], cost: 1
     21: f52 -> f71 : A'=0, L'=1, [ 1+F>=C && A==0 ], cost: 1
     13: f55 -> f52 : B'=1, F'=1+F, K'=1, [ free_5>=1+free_4 ], cost: 1
     14: f55 -> f52 : B'=0, F'=1+F, K'=0, [], cost: 1
     16: f63 -> f71 : L'=0, [ 0>=1+B ], cost: 1
     17: f63 -> f71 : L'=0, [ B>=1 ], cost: 1
     18: f63 -> f71 : B'=0, L'=1, [ B==0 ], cost: 1

Removing duplicate transition: 6.

Simplified the transitions:
  Start location: f0
      0: f0 -> f23 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [], cost: 1
      1: f23 -> f23 : F'=1+F, [ C>=1+F ], cost: 1
     26: f23 -> f29 : F'=0, [ F>=C ], cost: 1
      2: f29 -> f33 : G'=0, H'=0, [ C>=1+F ], cost: 1
     25: f29 -> f52 : F'=0, [ F>=C ], cost: 1
     24: f33 -> f29 : A'=0, F'=1+F, J'=0, [ H>=C && A==0 ], cost: 1
      3: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ 0>=1+G && C>=1+H ], cost: 1
      4: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ G>=1 && C>=1+H ], cost: 1
      5: f33 -> f33 : G'=1, H'=1+H, Q'=1, [ C>=1+H && G==0 ], cost: 1
      7: f33 -> f33 : G'=0, H'=1+H, Q'=0, [ C>=1+H && G==0 ], cost: 1
     22: f33 -> f44 : [ 0>=1+A && H>=C ], cost: 1
     23: f33 -> f44 : [ A>=1 && H>=C ], cost: 1
      8: f44 -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+G ], cost: 1
      9: f44 -> f29 : A'=1, F'=1+F, J'=1, [ G>=1 ], cost: 1
     10: f44 -> f29 : A'=0, F'=1+F, G'=0, J'=0, [ G==0 ], cost: 1
     15: f52 -> f52 : B'=0, F'=1+F, K'=0, [ C>=2+F && B==0 ], cost: 1
     11: f52 -> f55 : [ 0>=1+B && C>=2+F ], cost: 1
     12: f52 -> f55 : [ B>=1 && C>=2+F ], cost: 1
     13: f55 -> f52 : B'=1, F'=1+F, K'=1, [], cost: 1
     14: f55 -> f52 : B'=0, F'=1+F, K'=0, [], cost: 1

Eliminating 1 self-loops for location f23
  Self-Loop 1 has the metering function: -F+C, resulting in the new transition 27.
  Removing the self-loops: 1.
Eliminating 4 self-loops for location f33
  Self-Loop 4 has the metering function: -H+C, resulting in the new transition 29.
  Self-Loop 5 has the metering function: -G, resulting in the new transition 30.
  Self-Loop 7 has the metering function: -H+C, resulting in the new transition 31.
  Found this metering function when nesting loops: -G,
  Found this metering function when nesting loops: 1-G,
  Found this metering function when nesting loops: -G,
  and nested parallel self-loops 7 (outer loop) and 30 (inner loop), obtaining the new transitions: 32.
  Found this metering function when nesting loops: -G,
  Found this metering function when nesting loops: -G,
  and nested parallel self-loops 7 (outer loop) and 32 (inner loop), obtaining the new transitions: 33.
  Found this metering function when nesting loops: -G,
  Found this metering function when nesting loops: -G,
  and nested parallel self-loops 7 (outer loop) and 33 (inner loop), obtaining the new transitions: 34.
  Removing the self-loops: 3 4 5 7.
Adding an epsilon transition (to model nonexecution of the loops): 35.
Eliminating 1 self-loops for location f52
  Self-Loop 15 has the metering function: -1-F+C, resulting in the new transition 36.
  Removing the self-loops: 15.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f23 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [], cost: 1
     27: f23 -> [9] : F'=C, [ C>=1+F ], cost: -F+C
      2: f29 -> f33 : G'=0, H'=0, [ C>=1+F ], cost: 1
     25: f29 -> f52 : F'=0, [ F>=C ], cost: 1
     28: f33 -> [10] : G'=1, H'=1+H, Q'=1, [ 0>=1+G && C>=1+H ], cost: 1
     29: f33 -> [10] : G'=1, H'=C, Q'=1, [ G>=1 && C>=1+H ], cost: -H+C
     30: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 ], cost: -G
     31: f33 -> [10] : G'=0, H'=C, Q'=0, [ C>=1+H && G==0 ], cost: -H+C
     32: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 ], cost: -G
     33: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 && C>=3+H && 0==0 ], cost: -G
     34: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 && C>=3+H && 0==0 && C>=4+H && 0==0 ], cost: -G
     35: f33 -> [10] : [], cost: 0
      8: f44 -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+G ], cost: 1
      9: f44 -> f29 : A'=1, F'=1+F, J'=1, [ G>=1 ], cost: 1
     10: f44 -> f29 : A'=0, F'=1+F, G'=0, J'=0, [ G==0 ], cost: 1
     36: f52 -> [11] : B'=0, F'=-1+C, K'=0, [ C>=2+F && B==0 ], cost: -1-F+C
     13: f55 -> f52 : B'=1, F'=1+F, K'=1, [], cost: 1
     14: f55 -> f52 : B'=0, F'=1+F, K'=0, [], cost: 1
     26: [9] -> f29 : F'=0, [ F>=C ], cost: 1
     24: [10] -> f29 : A'=0, F'=1+F, J'=0, [ H>=C && A==0 ], cost: 1
     22: [10] -> f44 : [ 0>=1+A && H>=C ], cost: 1
     23: [10] -> f44 : [ A>=1 && H>=C ], cost: 1
     11: [11] -> f55 : [ 0>=1+B && C>=2+F ], cost: 1
     12: [11] -> f55 : [ B>=1 && C>=2+F ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f29 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [ 10>=1 && 10>=10 ], cost: 12
      2: f29 -> f33 : G'=0, H'=0, [ C>=1+F ], cost: 1
     25: f29 -> f52 : F'=0, [ F>=C ], cost: 1
     28: f33 -> [10] : G'=1, H'=1+H, Q'=1, [ 0>=1+G && C>=1+H ], cost: 1
     29: f33 -> [10] : G'=1, H'=C, Q'=1, [ G>=1 && C>=1+H ], cost: -H+C
     30: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 ], cost: -G
     31: f33 -> [10] : G'=0, H'=C, Q'=0, [ C>=1+H && G==0 ], cost: -H+C
     32: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 ], cost: -G
     33: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 && C>=3+H && 0==0 ], cost: -G
     34: f33 -> [10] : G'=1, H'=H-G, Q'=1, [ C>=1+H && G==0 && C>=2+H && 0==0 && C>=3+H && 0==0 && C>=4+H && 0==0 ], cost: -G
     35: f33 -> [10] : [], cost: 0
      8: f44 -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+G ], cost: 1
      9: f44 -> f29 : A'=1, F'=1+F, J'=1, [ G>=1 ], cost: 1
     10: f44 -> f29 : A'=0, F'=1+F, G'=0, J'=0, [ G==0 ], cost: 1
     36: f52 -> [11] : B'=0, F'=-1+C, K'=0, [ C>=2+F && B==0 ], cost: -1-F+C
     13: f55 -> f52 : B'=1, F'=1+F, K'=1, [], cost: 1
     14: f55 -> f52 : B'=0, F'=1+F, K'=0, [], cost: 1
     24: [10] -> f29 : A'=0, F'=1+F, J'=0, [ H>=C && A==0 ], cost: 1
     22: [10] -> f44 : [ 0>=1+A && H>=C ], cost: 1
     23: [10] -> f44 : [ A>=1 && H>=C ], cost: 1
     11: [11] -> f55 : [ 0>=1+B && C>=2+F ], cost: 1
     12: [11] -> f55 : [ B>=1 && C>=2+F ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f29 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [ 10>=1 && 10>=10 ], cost: 12
     25: f29 -> f52 : F'=0, [ F>=C ], cost: 1
     37: f29 -> [10] : G'=1, H'=0, Q'=1, [ C>=1+F && C>=1 && 0==0 ], cost: 1
     38: f29 -> [10] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     39: f29 -> [10] : G'=1, H'=0, Q'=1, [ C>=1+F && C>=1 && 0==0 && C>=2 && 0==0 ], cost: 1
     40: f29 -> [10] : G'=1, H'=0, Q'=1, [ C>=1+F && C>=1 && 0==0 && C>=2 && 0==0 && C>=3 && 0==0 ], cost: 1
     42: f29 -> [10] : G'=0, H'=0, [ C>=1+F ], cost: 1
     43: f52 -> [12] : B'=0, F'=-1+C, K'=0, [ C>=2+F && B==0 ], cost: -1-F+C
     44: f52 -> [13] : B'=0, F'=-1+C, K'=0, [ C>=2+F && B==0 ], cost: -1-F+C
     24: [10] -> f29 : A'=0, F'=1+F, J'=0, [ H>=C && A==0 ], cost: 1
     45: [10] -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+A && H>=C && 0>=1+G ], cost: 2
     46: [10] -> f29 : A'=1, F'=1+F, J'=1, [ 0>=1+A && H>=C && G>=1 ], cost: 2
     47: [10] -> f29 : A'=0, F'=1+F, G'=0, J'=0, [ 0>=1+A && H>=C && G==0 ], cost: 2
     48: [10] -> f29 : A'=1, F'=1+F, J'=1, [ A>=1 && H>=C && 0>=1+G ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f29 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [ 10>=1 && 10>=10 ], cost: 12
     53: f29 -> f29 : A'=0, F'=1+F, G'=0, H'=C, Q'=0, J'=0, [ C>=1+F && C>=1 && 0==0 && C>=C && A==0 ], cost: 2+C
     56: f29 -> f29 : A'=0, F'=1+F, G'=0, H'=C, Q'=0, J'=0, [ C>=1+F && C>=1 && 0==0 && 0>=1+A && C>=C && 0==0 ], cost: 3+C
     58: f29 -> f29 : A'=0, F'=1+F, G'=0, H'=0, J'=0, [ C>=1+F && 0>=C && A==0 ], cost: 2
     59: f29 -> f29 : A'=0, F'=1+F, G'=0, H'=0, J'=0, [ C>=1+F && 0>=1+A && 0>=C && 0==0 ], cost: 3
     51: f29 -> [12] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     52: f29 -> [13] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     54: f29 -> [14] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     55: f29 -> [15] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     57: f29 -> [16] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C

Eliminating 4 self-loops for location f29
  Self-Loop 53 has the metering function: -F+C, resulting in the new transition 60.
  Self-Loop 58 has the metering function: -F+C, resulting in the new transition 62.
  Removing the self-loops: 53 56 58 59.
Adding an epsilon transition (to model nonexecution of the loops): 64.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f29 : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [ 10>=1 && 10>=10 ], cost: 12
     60: f29 -> [17] : A'=0, F'=C, G'=0, H'=C, Q'=0, J'=0, [ C>=1+F && C>=1 && A==0 ], cost: -C*(F-C)-2*F+2*C
     61: f29 -> [17] : A'=0, F'=1+F, G'=0, H'=C, Q'=0, J'=0, [ C>=1+F && C>=1 && 0>=1+A ], cost: 3+C
     62: f29 -> [17] : A'=0, F'=C, G'=0, H'=0, J'=0, [ C>=1+F && 0>=C && A==0 ], cost: -2*F+2*C
     63: f29 -> [17] : A'=0, F'=1+F, G'=0, H'=0, J'=0, [ C>=1+F && 0>=1+A && 0>=C ], cost: 3
     64: f29 -> [17] : [], cost: 0
     51: [17] -> [12] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     52: [17] -> [13] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     54: [17] -> [14] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     55: [17] -> [15] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     57: [17] -> [16] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C


Applied chaining over branches and pruning:
  Start location: f0
     65: f0 -> [17] : A'=1, B'=1, C'=10, D'=free_1, E'=free, F'=0, [ 10>=1 && 10>=10 ], cost: 12
     51: [17] -> [12] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     52: [17] -> [13] : B'=0, F'=-1+C, K'=0, [ F>=C && C>=2 && B==0 ], cost: C
     54: [17] -> [14] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     55: [17] -> [15] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C
     57: [17] -> [16] : G'=0, H'=C, Q'=0, [ C>=1+F && C>=1 && 0==0 ], cost: 1+C


Applied chaining over branches and pruning:
  Start location: f0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

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

WORST_CASE(Omega(1),?)