Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
      2: eval2 -> eval3 : C'=A, D'=2*A, [ B>=2 ], cost: 1
      5: eval3 -> eval3 : C'=D, D'=2*D, [ B>=D && B>=1+D && D>=1 ], cost: 1
      6: eval3 -> eval3 : C'=1+D, D'=2+2*D, [ B>=D && B>=1+D && D>=1 ], cost: 1
      8: eval3 -> eval3 : C'=D, D'=2*D, [ D>=1 && B==D ], cost: 1
      3: eval3 -> eval4 : [ B>=D && B>=1+D ], cost: 1
      4: eval3 -> eval4 : D'=1+D, [ B>=D && B>=1+D ], cost: 1
      7: eval3 -> eval4 : [ B==D ], cost: 1
      9: eval4 -> eval2 : A'=-1+A, [ A>=2 && A>=1 && B>=2 ], cost: 1
     10: eval4 -> eval2 : B'=-1+B, [ B>=2 && A==1 ], cost: 1


Simplified the transitions:
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
      2: eval2 -> eval3 : C'=A, D'=2*A, [ B>=2 ], cost: 1
      5: eval3 -> eval3 : C'=D, D'=2*D, [ B>=1+D && D>=1 ], cost: 1
      6: eval3 -> eval3 : C'=1+D, D'=2+2*D, [ B>=1+D && D>=1 ], cost: 1
      8: eval3 -> eval3 : C'=D, D'=2*D, [ D>=1 && B==D ], cost: 1
      3: eval3 -> eval4 : [ B>=1+D ], cost: 1
      4: eval3 -> eval4 : D'=1+D, [ B>=1+D ], cost: 1
      7: eval3 -> eval4 : [ B==D ], cost: 1
      9: eval4 -> eval2 : A'=-1+A, [ A>=2 && B>=2 ], cost: 1
     10: eval4 -> eval2 : B'=-1+B, [ B>=2 && A==1 ], cost: 1

Eliminating 3 self-loops for location eval3
  Removing the self-loops: 5 6 8.
Adding an epsilon transition (to model nonexecution of the loops): 14.

Removed all Self-loops using metering functions (where possible):
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
      2: eval2 -> eval3 : C'=A, D'=2*A, [ B>=2 ], cost: 1
     11: eval3 -> [4] : C'=D, D'=2*D, [ B>=1+D && D>=1 ], cost: 1
     12: eval3 -> [4] : C'=1+D, D'=2+2*D, [ B>=1+D && D>=1 ], cost: 1
     13: eval3 -> [4] : C'=D, D'=2*D, [ D>=1 && B==D ], cost: 1
     14: eval3 -> [4] : [], cost: 0
      9: eval4 -> eval2 : A'=-1+A, [ A>=2 && B>=2 ], cost: 1
     10: eval4 -> eval2 : B'=-1+B, [ B>=2 && A==1 ], cost: 1
      3: [4] -> eval4 : [ B>=1+D ], cost: 1
      4: [4] -> eval4 : D'=1+D, [ B>=1+D ], cost: 1
      7: [4] -> eval4 : [ B==D ], cost: 1


Applied chaining over branches and pruning:
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
     15: eval2 -> [4] : C'=2*A, D'=4*A, [ B>=2 && B>=1+2*A && 2*A>=1 ], cost: 2
     16: eval2 -> [4] : C'=1+2*A, D'=2+4*A, [ B>=2 && B>=1+2*A && 2*A>=1 ], cost: 2
     17: eval2 -> [4] : C'=2*A, D'=4*A, [ B>=2 && 2*A>=1 && B==2*A ], cost: 2
     18: eval2 -> [4] : C'=A, D'=2*A, [ B>=2 ], cost: 1
     19: [4] -> eval2 : A'=-1+A, [ B>=1+D && A>=2 && B>=2 ], cost: 2
     20: [4] -> eval2 : B'=-1+B, [ B>=1+D && B>=2 && A==1 ], cost: 2
     21: [4] -> eval2 : A'=-1+A, D'=1+D, [ B>=1+D && A>=2 && B>=2 ], cost: 2
     22: [4] -> eval2 : B'=-1+B, D'=1+D, [ B>=1+D && B>=2 && A==1 ], cost: 2
     24: [4] -> eval2 : B'=-1+B, [ B==D && B>=2 && A==1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
     25: eval2 -> eval2 : A'=-1+A, C'=2*A, D'=4*A, [ B>=2 && B>=1+2*A && 2*A>=1 && B>=1+4*A && A>=2 && B>=2 ], cost: 4
     26: eval2 -> eval2 : B'=-1+B, C'=2*A, D'=4*A, [ B>=2 && B>=1+2*A && 2*A>=1 && B>=1+4*A && B>=2 && A==1 ], cost: 4
     28: eval2 -> eval2 : B'=-1+B, C'=2*A, D'=1+4*A, [ B>=2 && B>=1+2*A && 2*A>=1 && B>=1+4*A && B>=2 && A==1 ], cost: 4
     32: eval2 -> eval2 : A'=-1+A, C'=1+2*A, D'=3+4*A, [ B>=2 && B>=1+2*A && 2*A>=1 && B>=3+4*A && A>=2 && B>=2 ], cost: 4
     33: eval2 -> eval2 : B'=-1+B, C'=1+2*A, D'=3+4*A, [ B>=2 && B>=1+2*A && 2*A>=1 && B>=3+4*A && B>=2 && A==1 ], cost: 4

Eliminating 5 self-loops for location eval2
  Self-Loop 25 has the metering function: -1+A, resulting in the new transition 40.
  Self-Loop 26 has the metering function: B-4*A, resulting in the new transition 41.
  Self-Loop 28 has the metering function: B-4*A, resulting in the new transition 42.
  Self-Loop 32 has the metering function: -1+A, resulting in the new transition 43.
  Self-Loop 33 has the metering function: -2+B-4*A, resulting in the new transition 44.
  Found this metering function when nesting loops: -2+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -2+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -2+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -2+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -1+A,
  Found this metering function when nesting loops: -1+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -1+A,
  Found this metering function when nesting loops: 1-A,
  Found this metering function when nesting loops: -2+A,
  Removing the self-loops: 25 26 28 32 33.

Removed all Self-loops using metering functions (where possible):
  Start location: eval1
      0: eval1 -> eval2 : A'=-1+A, [ A>=2 ], cost: 1
      1: eval1 -> eval2 : B'=-1+B, [ 1>=A ], cost: 1
     40: eval2 -> [5] : A'=1, C'=4, D'=8, [ B>=2 && B>=1+2*A && B>=1+4*A && A>=2 ], cost: -4+4*A
     41: eval2 -> [5] : B'=4*A, C'=2*A, D'=4*A, [ B>=2 && B>=1+2*A && B>=1+4*A && A==1 ], cost: 4*B-16*A
     42: eval2 -> [5] : B'=4*A, C'=2*A, D'=1+4*A, [ B>=2 && B>=1+2*A && B>=1+4*A && A==1 ], cost: 4*B-16*A
     43: eval2 -> [5] : A'=1, C'=5, D'=11, [ B>=2 && B>=1+2*A && B>=3+4*A && A>=2 ], cost: -4+4*A
     44: eval2 -> [5] : B'=2+4*A, C'=1+2*A, D'=3+4*A, [ B>=2 && B>=1+2*A && B>=3+4*A && A==1 ], cost: -8+4*B-16*A


Applied chaining over branches and pruning:
  Start location: eval1
     45: eval1 -> [5] : A'=1, C'=4, D'=8, [ A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A>=2 ], cost: -7+4*A
     46: eval1 -> [5] : A'=-1+A, B'=-4+4*A, C'=-2+2*A, D'=-4+4*A, [ A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A==1 ], cost: 17+4*B-16*A
     48: eval1 -> [5] : A'=1, C'=5, D'=11, [ A>=2 && B>=2 && B>=-1+2*A && B>=-1+4*A && -1+A>=2 ], cost: -7+4*A
     49: eval1 -> [5] : A'=-1+A, B'=-2+4*A, C'=-1+2*A, D'=-1+4*A, [ A>=2 && B>=2 && B>=-1+2*A && B>=-1+4*A && -1+A==1 ], cost: 9+4*B-16*A
     50: eval1 -> [5] : B'=4*A, C'=2*A, D'=4*A, [ 1>=A && -1+B>=2 && -1+B>=1+2*A && -1+B>=1+4*A && A==1 ], cost: -3+4*B-16*A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: eval1
     45: eval1 -> [5] : A'=1, C'=4, D'=8, [ A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A>=2 ], cost: -7+4*A
     46: eval1 -> [5] : A'=-1+A, B'=-4+4*A, C'=-2+2*A, D'=-4+4*A, [ A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A==1 ], cost: 17+4*B-16*A
     48: eval1 -> [5] : A'=1, C'=5, D'=11, [ A>=2 && B>=2 && B>=-1+2*A && B>=-1+4*A && -1+A>=2 ], cost: -7+4*A
     49: eval1 -> [5] : A'=-1+A, B'=-2+4*A, C'=-1+2*A, D'=-1+4*A, [ A>=2 && B>=2 && B>=-1+2*A && B>=-1+4*A && -1+A==1 ], cost: 9+4*B-16*A
     50: eval1 -> [5] : B'=4*A, C'=2*A, D'=4*A, [ 1>=A && -1+B>=2 && -1+B>=1+2*A && -1+B>=1+4*A && A==1 ], cost: -3+4*B-16*A


Computing complexity for remaining 5 transitions.

  Found configuration with infinitely models for cost: -7+4*A
  and guard: A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A>=2:
  B: Pos, A: Pos, where: B > A

Found new complexity n^1, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: A>=2 && B>=2 && B>=-1+2*A && B>=-3+4*A && -1+A>=2
  Final Cost:  -7+4*A

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

WORST_CASE(Omega(n^1),?)