Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop1 : [ A>=0 && B>=0 && C>=0 && D==0 ], cost: 1
      1: start -> cont1 : [ D>=1 && A>=0 && B>=0 && C>=0 && D>=0 && A>=D ], cost: 1
      2: cont1 -> stop2 : C'=1, D'=-1+D, [ D>=1 && B>=0 && A>=D && C==0 ], cost: 1
      3: cont1 -> a : C'=-1+C, [ C>=1 && D>=1 && C>=0 && B>=0 && A>=D ], cost: 1
      4: a -> b : C'=free, D'=-1+D, [ A>=D && B>=0 && C>=0 && D>=1 ], cost: 1
      5: b -> start : [ C>=0 && D>=0 && B>=0 && A>=1+D ], cost: 1
      6: b -> stop3 : [ 0>=1+C && D>=0 && B>=0 && A>=1+D ], cost: 1
      7: start0 -> start : C'=B, D'=A, [ A>=0 && B>=0 ], cost: 1


Simplified the transitions:
  Start location: start0
      1: start -> cont1 : [ D>=1 && A>=0 && B>=0 && C>=0 && A>=D ], cost: 1
      3: cont1 -> a : C'=-1+C, [ C>=1 && D>=1 && B>=0 && A>=D ], cost: 1
      4: a -> b : C'=free, D'=-1+D, [ A>=D && B>=0 && C>=0 && D>=1 ], cost: 1
      5: b -> start : [ C>=0 && D>=0 && B>=0 && A>=1+D ], cost: 1
      7: start0 -> start : C'=B, D'=A, [ A>=0 && B>=0 ], cost: 1


Applied simple chaining:
  Start location: start0
      1: start -> start : C'=free, D'=-1+D, [ D>=1 && A>=0 && B>=0 && C>=0 && A>=D && C>=1 && D>=1 && B>=0 && A>=D && A>=D && B>=0 && -1+C>=0 && D>=1 && free>=0 && -1+D>=0 && B>=0 && A>=D ], cost: 4
      7: start0 -> start : C'=B, D'=A, [ A>=0 && B>=0 ], cost: 1

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

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      8: start -> [8] : C'=free, D'=-1+D, [ D>=1 && A>=0 && B>=0 && A>=D && C>=1 && free>=0 ], cost: 4
      9: start -> [8] : [], cost: 0
      7: start0 -> start : C'=B, D'=A, [ A>=0 && B>=0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
    <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),?)