Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f9 : A'=0, B'=1, C'=1, D'=0, E'=0, F'=free, [ free>=1 ], cost: 1
      1: f9 -> f20 : C'=-1+C, E'=D, F'=0, G'=-2+A, H'=1, Q'=-2+A, [ A>=3 && C>=1 && D==E && F==0 ], cost: 1
      2: f9 -> f20 : C'=-1+C, E'=D, F'=0, G'=A, H'=0, Q'=A, [ 2>=A && C>=1 && D==E && F==0 ], cost: 1
      3: f9 -> f20 : A'=0, B'=1+B, C'=1+B, E'=D, F'=free_1, [ free_1>=1 && A>=3 && 0>=C && D==E && F==0 ], cost: 1
      4: f9 -> f20 : A'=1+A, B'=1+B, C'=1+B, E'=D, F'=free_2, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 ], cost: 1
      5: f9 -> f20 : E'=D, F'=-1+F, H'=free_4, Q'=free_3, [ 0>=1+F && D==E ], cost: 1
      6: f9 -> f20 : E'=D, F'=-1+F, H'=free_6, Q'=free_5, [ F>=1 && D==E ], cost: 1
     13: f9 -> f38 : [ E>=1+D ], cost: 1
     14: f9 -> f38 : [ D>=1+E ], cost: 1
      7: f20 -> f32 : D'=0, Q'=0, [ Q==0 ], cost: 1
      8: f20 -> f32 : D'=1, [ 0>=1+Q ], cost: 1
      9: f20 -> f32 : D'=1, [ Q>=1 ], cost: 1
     10: f32 -> f9 : E'=0, H'=0, [ H==0 ], cost: 1
     11: f32 -> f9 : E'=1, [ 0>=1+H ], cost: 1
     12: f32 -> f9 : E'=1, [ H>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f9 : A'=0, B'=1, C'=1, D'=0, E'=0, F'=free, [ free>=1 ], cost: 1
      1: f9 -> f20 : C'=-1+C, E'=D, F'=0, G'=-2+A, H'=1, Q'=-2+A, [ A>=3 && C>=1 && D==E && F==0 ], cost: 1
      2: f9 -> f20 : C'=-1+C, E'=D, F'=0, G'=A, H'=0, Q'=A, [ 2>=A && C>=1 && D==E && F==0 ], cost: 1
      3: f9 -> f20 : A'=0, B'=1+B, C'=1+B, E'=D, F'=free_1, [ free_1>=1 && A>=3 && 0>=C && D==E && F==0 ], cost: 1
      4: f9 -> f20 : A'=1+A, B'=1+B, C'=1+B, E'=D, F'=free_2, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 ], cost: 1
      5: f9 -> f20 : E'=D, F'=-1+F, H'=free_4, Q'=free_3, [ 0>=1+F && D==E ], cost: 1
      6: f9 -> f20 : E'=D, F'=-1+F, H'=free_6, Q'=free_5, [ F>=1 && D==E ], cost: 1
      7: f20 -> f32 : D'=0, Q'=0, [ Q==0 ], cost: 1
      8: f20 -> f32 : D'=1, [ 0>=1+Q ], cost: 1
      9: f20 -> f32 : D'=1, [ Q>=1 ], cost: 1
     10: f32 -> f9 : E'=0, H'=0, [ H==0 ], cost: 1
     11: f32 -> f9 : E'=1, [ 0>=1+H ], cost: 1
     12: f32 -> f9 : E'=1, [ H>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f9 : A'=0, B'=1, C'=1, D'=0, E'=0, F'=free, [ free>=1 ], cost: 1
     15: f9 -> f32 : C'=-1+C, D'=1, E'=D, F'=0, G'=-2+A, H'=1, Q'=-2+A, [ A>=3 && C>=1 && D==E && F==0 && -2+A>=1 ], cost: 2
     16: f9 -> f32 : C'=-1+C, D'=0, E'=D, F'=0, G'=A, H'=0, Q'=0, [ 2>=A && C>=1 && D==E && F==0 && A==0 ], cost: 2
     18: f9 -> f32 : C'=-1+C, D'=1, E'=D, F'=0, G'=A, H'=0, Q'=A, [ 2>=A && C>=1 && D==E && F==0 && A>=1 ], cost: 2
     22: f9 -> f32 : A'=1+A, B'=1+B, C'=1+B, D'=0, E'=D, F'=free_2, Q'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q==0 ], cost: 2
     24: f9 -> f32 : A'=1+A, B'=1+B, C'=1+B, D'=1, E'=D, F'=free_2, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q>=1 ], cost: 2
     10: f32 -> f9 : E'=0, H'=0, [ H==0 ], cost: 1
     11: f32 -> f9 : E'=1, [ 0>=1+H ], cost: 1
     12: f32 -> f9 : E'=1, [ H>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f9 : A'=0, B'=1, C'=1, D'=0, E'=0, F'=free, [ free>=1 ], cost: 1
     31: f9 -> f9 : C'=-1+C, D'=1, E'=1, F'=0, G'=-2+A, H'=1, Q'=-2+A, [ A>=3 && C>=1 && D==E && F==0 && -2+A>=1 && 1>=1 ], cost: 3
     32: f9 -> f9 : C'=-1+C, D'=0, E'=0, F'=0, G'=A, H'=0, Q'=0, [ 2>=A && C>=1 && D==E && F==0 && A==0 && 0==0 ], cost: 3
     34: f9 -> f9 : A'=1+A, B'=1+B, C'=1+B, D'=0, E'=0, F'=free_2, H'=0, Q'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q==0 && H==0 ], cost: 3
     35: f9 -> f9 : A'=1+A, B'=1+B, C'=1+B, D'=0, E'=1, F'=free_2, Q'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q==0 && 0>=1+H ], cost: 3
     37: f9 -> f9 : A'=1+A, B'=1+B, C'=1+B, D'=1, E'=0, F'=free_2, H'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q>=1 && H==0 ], cost: 3

Eliminating 5 self-loops for location f9
  Self-Loop 31 has the metering function: C, resulting in the new transition 40.
  Self-Loop 32 has the metering function: C, resulting in the new transition 41.
  Self-Loop 34 has the metering function: -F, resulting in the new transition 42.
  Self-Loop 35 has the metering function: -E+D, resulting in the new transition 43.
  Self-Loop 37 has the metering function: E-D, resulting in the new transition 44.
  Found this metering function when nesting loops: -A,
  and nested parallel self-loops 34 (outer loop) and 41 (inner loop), obtaining the new transitions: 45.
  Found this metering function when nesting loops: -F,
  and nested parallel self-loops 32 (outer loop) and 42 (inner loop), obtaining the new transitions: 46.
  Found this metering function when nesting loops: -A,
  Found this metering function when nesting loops: -F,
  and nested parallel self-loops 32 (outer loop) and 46 (inner loop), obtaining the new transitions: 47.
  Found this metering function when nesting loops: -F,
  and nested parallel self-loops 32 (outer loop) and 47 (inner loop), obtaining the new transitions: 48.
  Removing the self-loops: 31 32 34 35 37.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f9 : A'=0, B'=1, C'=1, D'=0, E'=0, F'=free, [ free>=1 ], cost: 1
     40: f9 -> [5] : C'=0, D'=1, E'=1, F'=0, G'=-2+A, H'=1, Q'=-2+A, [ A>=3 && C>=1 && D==E && F==0 ], cost: 3*C
     41: f9 -> [5] : C'=0, D'=0, E'=0, F'=0, G'=A, H'=0, Q'=0, [ C>=1 && D==E && F==0 && A==0 ], cost: 3*C
     42: f9 -> [5] : A'=-F+A, B'=B-F, C'=B-F, D'=0, E'=0, F'=1, H'=0, Q'=0, [ 1>=1 && 2>=A && 0>=C && D==E && F==0 && Q==0 && H==0 ], cost: -3*F
     43: f9 -> [5] : A'=-E+D+A, B'=-E+B+D, C'=-E+B+D, D'=0, E'=1, F'=free_2, Q'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q==0 && 0>=1+H ], cost: -3*E+3*D
     44: f9 -> [5] : A'=E-D+A, B'=E+B-D, C'=E+B-D, D'=1, E'=0, F'=free_2, H'=0, [ free_2>=1 && 2>=A && 0>=C && D==E && F==0 && Q>=1 && H==0 ], cost: 3*E-3*D
     45: f9 -> [5] : A'=0, B'=B-A, C'=B-A, D'=0, E'=0, F'=free_2, G'=-1, H'=0, Q'=0, [ C>=1 && D==E && F==0 && A==0 && free_2>=1 && 2>=A && 0>=0 && 0==0 && 0==0 && 0==0 && 0==0 ], cost: 3/2*A^2-3*B*A-3/2*A
     46: f9 -> [5] : A'=A, B'=B, C'=B, D'=0, E'=0, F'=1, G'=A, H'=0, Q'=0, [ C>=1 && D==E && F==0 && A==0 && 1>=1 && 2>=A && 0>=-1+C && 0==0 && 0==0 && 0==0 && 0==0 ], cost: -3*F
     47: f9 -> [5] : A'=A, B'=B, C'=B, D'=0, E'=0, F'=1, G'=A, H'=0, Q'=0, [ C>=1 && D==E && F==0 && A==0 && -1+C>=1 && 0==0 && 0==0 && A==0 && 1>=1 && 2>=A && 0>=-2+C && 0==0 && 0==0 && 0==0 && 0==0 ], cost: -3*F
     48: f9 -> [5] : A'=A, B'=B, C'=B, D'=0, E'=0, F'=1, G'=A, H'=0, Q'=0, [ C>=1 && D==E && F==0 && A==0 && -1+C>=1 && 0==0 && 0==0 && A==0 && -2+C>=1 && 0==0 && 0==0 && A==0 && 1>=1 && 2>=A && 0>=-3+C && 0==0 && 0==0 && 0==0 && 0==0 ], cost: -3*F


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