Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f1 : [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 ], cost: 1
      1: f1 -> f2 : F'=1+D, [ 1+B>=2*D ], cost: 1
      2: f1 -> f2 : F'=-1+D, [ 2*D>=4+B ], cost: 1
      3: f1 -> f2 : F'=D, [ 2+B==2*D ], cost: 1
      4: f1 -> f2 : F'=D, [ 3+B==2*D ], cost: 1
      5: f2 -> f3 : G'=1+E, [ D+A>=1+2*E ], cost: 1
      6: f2 -> f3 : G'=-1+E, [ 2*E>=2+D+A ], cost: 1
      7: f2 -> f3 : G'=E, [ D+A==2*E ], cost: 1
      8: f2 -> f3 : G'=E, [ 1+D+A==2*E ], cost: 1
      9: f3 -> f1 : D'=F, E'=G, [ D>=1+F ], cost: 1
     10: f3 -> f1 : D'=F, E'=G, [ F>=1+D ], cost: 1
     11: f3 -> f1 : D'=F, E'=G, [ E>=1+G ], cost: 1
     12: f3 -> f1 : D'=F, E'=G, [ G>=1+E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f1 : [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 ], cost: 1
     13: f1 -> f3 : F'=1+D, G'=1+E, [ 1+B>=2*D && D+A>=1+2*E ], cost: 2
     14: f1 -> f3 : F'=1+D, G'=-1+E, [ 1+B>=2*D && 2*E>=2+D+A ], cost: 2
     16: f1 -> f3 : F'=1+D, G'=E, [ 1+B>=2*D && 1+D+A==2*E ], cost: 2
     20: f1 -> f3 : F'=-1+D, G'=E, [ 2*D>=4+B && 1+D+A==2*E ], cost: 2
     22: f1 -> f3 : F'=D, G'=-1+E, [ 2+B==2*D && 2*E>=2+D+A ], cost: 2
      9: f3 -> f1 : D'=F, E'=G, [ D>=1+F ], cost: 1
     10: f3 -> f1 : D'=F, E'=G, [ F>=1+D ], cost: 1
     11: f3 -> f1 : D'=F, E'=G, [ E>=1+G ], cost: 1
     12: f3 -> f1 : D'=F, E'=G, [ G>=1+E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f1 : [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 ], cost: 1
     29: f1 -> f1 : D'=1+D, E'=1+E, F'=1+D, G'=1+E, [ 1+B>=2*D && D+A>=1+2*E && 1+D>=1+D ], cost: 3
     30: f1 -> f1 : D'=1+D, E'=1+E, F'=1+D, G'=1+E, [ 1+B>=2*D && D+A>=1+2*E && 1+E>=1+E ], cost: 3
     31: f1 -> f1 : D'=1+D, E'=-1+E, F'=1+D, G'=-1+E, [ 1+B>=2*D && 2*E>=2+D+A && 1+D>=1+D ], cost: 3
     32: f1 -> f1 : D'=1+D, E'=-1+E, F'=1+D, G'=-1+E, [ 1+B>=2*D && 2*E>=2+D+A && E>=E ], cost: 3
     33: f1 -> f1 : D'=1+D, E'=E, F'=1+D, G'=E, [ 1+B>=2*D && 1+D+A==2*E && 1+D>=1+D ], cost: 3

Eliminating 5 self-loops for location f1
  Self-Loop 33 has the metering function: -1+2*E-D-A, resulting in the new transition 48.
  Found this metering function when nesting loops: meter,
  Found this metering function when nesting loops: meter_1,
  Removing the self-loops: 29 30 31 32 33 36 37 39 40 42 43 45 46.
Adding an epsilon transition (to model nonexecution of the loops): 49.
Removing duplicate transition: 38.
Removing duplicate transition: 44.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f1 : [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 ], cost: 1
     41: f1 -> [4] : D'=1+D, E'=1+E, F'=1+D, G'=1+E, [ 1+B>=2*D && D+A>=1+2*E ], cost: 3
     47: f1 -> [4] : D'=1+D, E'=-1+E, F'=1+D, G'=-1+E, [ 1+B>=2*D && 2*E>=2+D+A ], cost: 3
     48: f1 -> [4] : D'=-1+2*E-A, F'=-1+2*E-A, G'=E, [ 1+B>=2*D && 1+D+A==2*E ], cost: -3+6*E-3*D-3*A
     49: f1 -> [4] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: f0
     52: f0 -> [4] : D'=-1+2*E-A, F'=-1+2*E-A, G'=E, [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 && 1+B>=2*D && 1+D+A==2*E ], cost: -2+6*E-3*D-3*A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     52: f0 -> [4] : D'=-1+2*E-A, F'=-1+2*E-A, G'=E, [ A>=0 && 3>=A && B>=0 && 3>=B && 3>=C && D>=0 && 3>=E && E>=0 && 1+B>=2*D && 1+D+A==2*E ], cost: -2+6*E-3*D-3*A


Computing complexity for remaining 1 transitions.

Found new complexity const, because: const cost.


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