Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
      1: f8 -> f10 : [ 29>=D ], cost: 1
      8: f8 -> f28 : C'=1, F'=1, [ D>=30 ], cost: 1
      7: f10 -> f8 : D'=2+D, E'=-10+E, [ E>=D ], cost: 1
      2: f10 -> f14 : E'=free, [ D>=1+E && E>=6 ], cost: 1
      3: f10 -> f14 : E'=2+E, [ D>=1+E && 5>=E ], cost: 1
      4: f14 -> f10 : D'=10+D, [ 12>=E && E>=10 ], cost: 1
      5: f14 -> f10 : D'=1+D, [ E>=13 ], cost: 1
      6: f14 -> f10 : D'=1+D, [ 9>=E ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
      1: f8 -> f10 : [ 29>=D ], cost: 1
      7: f10 -> f8 : D'=2+D, E'=-10+E, [ E>=D ], cost: 1
      2: f10 -> f14 : E'=free, [ D>=1+E && E>=6 ], cost: 1
      3: f10 -> f14 : E'=2+E, [ D>=1+E && 5>=E ], cost: 1
      4: f14 -> f10 : D'=10+D, [ 12>=E && E>=10 ], cost: 1
      5: f14 -> f10 : D'=1+D, [ E>=13 ], cost: 1
      6: f14 -> f10 : D'=1+D, [ 9>=E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
      1: f8 -> f10 : [ 29>=D ], cost: 1
      7: f10 -> f8 : D'=2+D, E'=-10+E, [ E>=D ], cost: 1
      9: f10 -> f10 : D'=10+D, E'=free, [ D>=1+E && E>=6 && 12>=free && free>=10 ], cost: 2
     10: f10 -> f10 : D'=1+D, E'=free, [ D>=1+E && E>=6 && free>=13 ], cost: 2
     11: f10 -> f10 : D'=1+D, E'=free, [ D>=1+E && E>=6 && 9>=free ], cost: 2
     12: f10 -> f10 : D'=1+D, E'=2+E, [ D>=1+E && 5>=E && 9>=2+E ], cost: 2

Eliminating 4 self-loops for location f10
  Self-Loop 10 has the metering function: meter, resulting in the new transition 14.
  Self-Loop 11 has the metering function: meter_1, resulting in the new transition 15.
  Self-Loop 17 has unbounded runtime, resulting in the new transition 19.
  Found this metering function when nesting loops: meter_2,
  Found this metering function when nesting loops: meter_3,
  Removing the self-loops: 9 10 11 12 16 17.
Adding an epsilon transition (to model nonexecution of the loops): 20.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
      1: f8 -> f10 : [ 29>=D ], cost: 1
     13: f10 -> [5] : D'=10+D, E'=free, [ D>=1+E && E>=6 && 12>=free && free>=10 ], cost: 2
     14: f10 -> [5] : D'=meter+D, E'=13, [ D>=1+E && E>=6 && 13>=13 && 6*meter==-E+D ], cost: 2*meter
     15: f10 -> [5] : D'=meter_1+D, E'=9, [ D>=1+E && E>=6 && 9>=9 && 2*meter_1==-E+D ], cost: 2*meter_1
     18: f10 -> [5] : D'=1+D, E'=2+E, [ D>=1+E && 5>=E ], cost: 2
     19: f10 -> [5] : [ D>=1+E && 5>=E && E>D ], cost: INF
     20: f10 -> [5] : [], cost: 0
      7: [5] -> f8 : D'=2+D, E'=-10+E, [ E>=D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
     21: f8 -> [5] : D'=10+D, E'=free, [ 29>=D && D>=1+E && E>=6 && 12>=free && free>=10 ], cost: 3
     22: f8 -> [5] : D'=meter+D, E'=13, [ 29>=D && D>=1+E && E>=6 && 13>=13 && 6*meter==-E+D ], cost: 1+2*meter
     23: f8 -> [5] : D'=meter_1+D, E'=9, [ 29>=D && D>=1+E && E>=6 && 9>=9 && 2*meter_1==-E+D ], cost: 1+2*meter_1
     24: f8 -> [5] : D'=1+D, E'=2+E, [ 29>=D && D>=1+E && 5>=E ], cost: 3
     25: f8 -> [5] : [ 29>=D ], cost: 1
      7: [5] -> f8 : D'=2+D, E'=-10+E, [ E>=D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
     26: f8 -> f8 : D'=2+meter+D, E'=3, [ 29>=D && D>=1+E && E>=6 && 13>=13 && 6*meter==-E+D && 13>=meter+D ], cost: 2+2*meter
     27: f8 -> f8 : D'=2+meter_1+D, E'=-1, [ 29>=D && D>=1+E && E>=6 && 9>=9 && 2*meter_1==-E+D && 9>=meter_1+D ], cost: 2+2*meter_1
     28: f8 -> f8 : D'=3+D, E'=-8+E, [ 29>=D && D>=1+E && 5>=E && 2+E>=1+D ], cost: 4
     29: f8 -> f8 : D'=2+D, E'=-10+E, [ 29>=D && E>=D ], cost: 2

Eliminating 4 self-loops for location f8
  Self-Loop 28 has the metering function: meter_4, resulting in the new transition 32.
  Self-Loop 33 has unbounded runtime, resulting in the new transition 36.
  Found this metering function when nesting loops: meter_5,
  and nested parallel self-loops 35 (outer loop) and 32 (inner loop), obtaining the new transitions: 37.
  Removing the self-loops: 26 27 28 29 33 34 35.
Adding an epsilon transition (to model nonexecution of the loops): 38.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f8 : A'=1, B'=1, C'=0, D'=1, E'=1, [], cost: 1
     30: f8 -> [6] : D'=2+meter+D, E'=3, [ 29>=D && D>=1+E && E>=6 && 6*meter==-E+D && 13>=meter+D ], cost: 2+2*meter
     31: f8 -> [6] : D'=2+meter_1+D, E'=-1, [ 29>=D && D>=1+E && E>=6 && 2*meter_1==-E+D && 9>=meter_1+D ], cost: 2+2*meter_1
     32: f8 -> [6] : D'=3*meter_4+D, E'=E-8*meter_4, [ 29>=D && 1+E-D==0 && 5>=E && 11*meter_4==1+E-D ], cost: 4*meter_4
     36: f8 -> [6] : [ 29>=D && E>=D && D>E ], cost: INF
     37: f8 -> [6] : D'=3*meter_4*meter_5+D+2*meter_5, E'=E-8*meter_4*meter_5-10*meter_5, [ 29>=D && E>=D && 29>=2+D && -11+E-D==0 && 5>=-10+E && 11*meter_4==-11+E-D && 12*meter_5==-11+E-D ], cost: 4*meter_4*meter_5+2*meter_5
     38: f8 -> [6] : [], 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),?)