Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f1
      0: f1 -> f2 : C'=1+B, [ A>=B && A>=1 && B>=1 ], cost: 1
      1: f2 -> f3 : [ B>=1+C ], cost: 1
      2: f2 -> f3 : [ C>=1+B ], cost: 1
      3: f3 -> f2 : C'=0, [ 1+A>=0 && C>=1 && C>=1+A ], cost: 1
      4: f3 -> f2 : C'=1+C, [ A>=C && 1+C>=0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f1
      0: f1 -> f2 : C'=1+B, [ A>=B && A>=1 && B>=1 ], cost: 1
      5: f2 -> f2 : C'=0, [ B>=1+C && 1+A>=0 && C>=1 && C>=1+A ], cost: 2
      6: f2 -> f2 : C'=1+C, [ B>=1+C && A>=C && 1+C>=0 ], cost: 2
      7: f2 -> f2 : C'=0, [ C>=1+B && 1+A>=0 && C>=1 && C>=1+A ], cost: 2
      8: f2 -> f2 : C'=1+C, [ C>=1+B && A>=C && 1+C>=0 ], cost: 2

Eliminating 4 self-loops for location f2
  Self-Loop 8 has the metering function: 1-C+A, resulting in the new transition 12.
  Found unbounded runtime when nesting loops,
  and nested parallel self-loops 11 (outer loop) and 12 (inner loop), obtaining the new transitions: 13, 14.
  Found this metering function when nesting loops: 1-C+A,
  Found unbounded runtime when nesting loops,
  Found unbounded runtime when nesting loops,
  Removing the self-loops: 5 6 7 8 11.
Adding an epsilon transition (to model nonexecution of the loops): 15.

Removed all Self-loops using metering functions (where possible):
  Start location: f1
      0: f1 -> f2 : C'=1+B, [ A>=B && A>=1 && B>=1 ], cost: 1
      9: f2 -> [3] : C'=0, [ B>=1+C && 1+A>=0 && C>=1 && C>=1+A ], cost: 2
     10: f2 -> [3] : C'=1+C, [ B>=1+C && A>=C && 1+C>=0 ], cost: 2
     12: f2 -> [3] : C'=1+A, [ C>=1+B && A>=C && 1+C>=0 ], cost: 2-2*C+2*A
     13: f2 -> [3] : [ C>=1+B && 1+A>=0 && C>=1 && C>=1+A && 0>=1+B && A>=0 && 1>=0 ], cost: INF
     14: f2 -> [3] : C'=1+A, [ C>=1+B && A>=C && 1+C>=0 && 1+A>=1+B && 1+A>=0 && 1+A>=1 && 1+A>=1+A && 0>=1+B && A>=0 && 1>=0 ], cost: INF
     15: f2 -> [3] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: f1
     16: f1 -> [3] : C'=1+A, [ A>=B && A>=1 && B>=1 && 1+B>=1+B && A>=1+B && 2+B>=0 ], cost: 1-2*B+2*A


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


Computing complexity for remaining 1 transitions.

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

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


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