Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: eval1 -> eval2 : B'=1, [ A>=0 ], cost: 1
      2: eval2 -> eval1 : A'=-1+A, [ A>=0 && B>=1 && B>=A ], cost: 1
      1: eval2 -> eval2 : B'=2*B, [ A>=0 && B>=1 && A>=1+B ], cost: 1
      3: start -> eval1 : [], cost: 1

Eliminating 1 self-loops for location eval2
  Removing the self-loops: 1.
Adding an epsilon transition (to model nonexecution of the loops): 5.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      0: eval1 -> eval2 : B'=1, [ A>=0 ], cost: 1
      4: eval2 -> [3] : B'=2*B, [ A>=0 && B>=1 && A>=1+B ], cost: 1
      5: eval2 -> [3] : [], cost: 0
      3: start -> eval1 : [], cost: 1
      2: [3] -> eval1 : A'=-1+A, [ A>=0 && B>=1 && B>=A ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      6: eval1 -> [3] : B'=2, [ A>=0 && A>=0 && 1>=1 && A>=2 ], cost: 2
      7: eval1 -> [3] : B'=1, [ A>=0 ], cost: 1
      3: start -> eval1 : [], cost: 1
      2: [3] -> eval1 : A'=-1+A, [ A>=0 && B>=1 && B>=A ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      8: eval1 -> eval1 : A'=-1+A, B'=2, [ A>=0 && A>=0 && 1>=1 && A>=2 && A>=0 && 2>=1 && 2>=A ], cost: 3
      9: eval1 -> eval1 : A'=-1+A, B'=1, [ A>=0 && A>=0 && 1>=1 && 1>=A ], cost: 2
      3: start -> eval1 : [], cost: 1

Eliminating 2 self-loops for location eval1
  Self-Loop 8 has the metering function: -1+A, resulting in the new transition 10.
  Self-Loop 9 has the metering function: 1+A, resulting in the new transition 11.
  Found this metering function when nesting loops: meter,
  Found this metering function when nesting loops: meter_1,
  Removing the self-loops: 8 9.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     10: eval1 -> [4] : A'=1, B'=2, [ 2-A==0 ], cost: -3+3*A
     11: eval1 -> [4] : A'=-1, B'=1, [ A>=0 && 1>=A ], cost: 2+2*A
      3: start -> eval1 : [], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     12: start -> [4] : A'=1, B'=2, [ 2-A==0 ], cost: -2+3*A
     13: start -> [4] : A'=-1, B'=1, [ A>=0 && 1>=A ], cost: 3+2*A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start
     12: start -> [4] : A'=1, B'=2, [ 2-A==0 ], cost: -2+3*A
     13: start -> [4] : A'=-1, B'=1, [ A>=0 && 1>=A ], cost: 3+2*A


Computing complexity for remaining 2 transitions.

Found new complexity const, because: const cost.


The final runtime is determined by this resulting transition:
  Final Guard: 2-A==0
  Final Cost:  4

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

WORST_CASE(Omega(1),?)