Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f10 : A'=1, B'=1, C'=free, D'=0, E'=2, F'=1, [ free>=0 ], cost: 1
      1: f10 -> f21 : B'=-1+B, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C ], cost: 1
      2: f10 -> f21 : A'=1+A, B'=1+A, C'=free_1, G'=free_2, [ free_2>=0 && 1>=free_2 && free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C ], cost: 1
      3: f10 -> f21 : C'=-1+C, G'=free_3, [ free_3>=0 && 1>=free_3 && F>=1 && C>=1 && E>=F ], cost: 1
      6: f10 -> f31 : [ 0>=F && E>=F ], cost: 1
      7: f10 -> f31 : [ F>=1+E ], cost: 1
      4: f21 -> f10 : F'=-1+F, [ 0>=G ], cost: 1
      5: f21 -> f10 : F'=1+F, [ G>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f10 : A'=1, B'=1, C'=free, D'=0, E'=2, F'=1, [ free>=0 ], cost: 1
      1: f10 -> f21 : B'=-1+B, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C ], cost: 1
      2: f10 -> f21 : A'=1+A, B'=1+A, C'=free_1, G'=free_2, [ free_2>=0 && 1>=free_2 && free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C ], cost: 1
      3: f10 -> f21 : C'=-1+C, G'=free_3, [ free_3>=0 && 1>=free_3 && F>=1 && C>=1 && E>=F ], cost: 1
      4: f21 -> f10 : F'=-1+F, [ 0>=G ], cost: 1
      5: f21 -> f10 : F'=1+F, [ G>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f10 : A'=1, B'=1, C'=free, D'=0, E'=2, F'=1, [ free>=0 ], cost: 1
      8: f10 -> f10 : B'=-1+B, F'=-1+F, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C && 0>=0 ], cost: 2
      9: f10 -> f10 : A'=1+A, B'=1+A, C'=free_1, F'=-1+F, G'=free_2, [ free_2>=0 && 1>=free_2 && free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C && 0>=free_2 ], cost: 2
     10: f10 -> f10 : A'=1+A, B'=1+A, C'=free_1, F'=1+F, G'=free_2, [ free_2>=0 && 1>=free_2 && free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C && free_2>=1 ], cost: 2
     11: f10 -> f10 : C'=-1+C, F'=-1+F, G'=free_3, [ free_3>=0 && 1>=free_3 && F>=1 && C>=1 && E>=F && 0>=free_3 ], cost: 2
     12: f10 -> f10 : C'=-1+C, F'=1+F, G'=free_3, [ free_3>=0 && 1>=free_3 && F>=1 && C>=1 && E>=F && free_3>=1 ], cost: 2

Eliminating 5 self-loops for location f10
  Self-Loop 13 has the metering function: F, resulting in the new transition 22.
  Self-Loop 14 has the metering function: B, resulting in the new transition 23.
  Self-Loop 18 has the metering function: F, resulting in the new transition 24.
  Self-Loop 19 has the metering function: C, resulting in the new transition 25.
  Found this metering function when nesting loops: -1+C,
  Found this metering function when nesting loops: -1+C,
  Found this metering function when nesting loops: -1+C,
  Found this metering function when nesting loops: -1+C,
  Found this metering function when nesting loops: -1+C,
  Found this metering function when nesting loops: -1+C,
  Removing the self-loops: 8 9 10 11 12 13 14 18 19.
Adding an epsilon transition (to model nonexecution of the loops): 26.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f10 : A'=1, B'=1, C'=free, D'=0, E'=2, F'=1, [ free>=0 ], cost: 1
     15: f10 -> [4] : B'=-1+B, F'=-1+F, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C ], cost: 2
     16: f10 -> [4] : A'=1+A, B'=1+A, C'=free_1, F'=-1+F, G'=0, [ free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C ], cost: 2
     17: f10 -> [4] : A'=1+A, B'=1+A, C'=free_1, F'=1+F, G'=1, [ free_1>=0 && F>=1 && E>=F && 0>=B && 0>=C ], cost: 2
     20: f10 -> [4] : C'=-1+C, F'=-1+F, G'=0, [ F>=1 && C>=1 && E>=F ], cost: 2
     21: f10 -> [4] : C'=-1+C, F'=1+F, G'=1, [ F>=1 && C>=1 && E>=F ], cost: 2
     22: f10 -> [4] : B'=B-F, F'=0, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C && B>F ], cost: 2*F
     23: f10 -> [4] : B'=0, F'=-B+F, G'=0, [ F>=1 && E>=F && B>=1 && 0>=C && F>B ], cost: 2*B
     24: f10 -> [4] : C'=-F+C, F'=0, G'=0, [ F>=1 && C>=1 && E>=F && C>F ], cost: 2*F
     25: f10 -> [4] : C'=0, F'=F-C, G'=0, [ F>=1 && C>=1 && E>=F && F>C ], cost: 2*C
     26: f10 -> [4] : [], cost: 0


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