Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f8 -> f8 : A'=-1+A, [ A>=0 ], cost: 1 6: f8 -> f19 : B'=999, [ 0>=1+A ], cost: 1 1: f19 -> f19 : B'=-1+B, [ B>=0 ], cost: 1 4: f19 -> f28 : C'=999, [ 0>=1+B ], cost: 1 2: f28 -> f28 : C'=-1+C, [ C>=0 ], cost: 1 3: f28 -> f36 : [ 0>=1+C ], cost: 1 5: f0 -> f19 : B'=999, D'=1, [], cost: 1 Simplified the transitions: Start location: f0 1: f19 -> f19 : B'=-1+B, [ B>=0 ], cost: 1 4: f19 -> f28 : C'=999, [ 0>=1+B ], cost: 1 2: f28 -> f28 : C'=-1+C, [ C>=0 ], cost: 1 5: f0 -> f19 : B'=999, D'=1, [], cost: 1 Eliminating 1 self-loops for location f19 Self-Loop 1 has the metering function: 1+B, resulting in the new transition 7. Removing the self-loops: 1. Eliminating 1 self-loops for location f28 Self-Loop 2 has the metering function: 1+C, resulting in the new transition 8. Removing the self-loops: 2. Removed all Self-loops using metering functions (where possible): Start location: f0 7: f19 -> [5] : B'=-1, [ B>=0 ], cost: 1+B 8: f28 -> [6] : C'=-1, [ C>=0 ], cost: 1+C 5: f0 -> f19 : B'=999, D'=1, [], cost: 1 4: [5] -> f28 : C'=999, [ 0>=1+B ], cost: 1 Applied simple chaining: Start location: f0 5: f0 -> [6] : B'=-1, C'=-1, D'=1, [ 999>=0 && 0>=0 && 999>=0 ], cost: 2002 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 5: f0 -> [6] : B'=-1, C'=-1, D'=1, [ 999>=0 && 0>=0 && 999>=0 ], cost: 2002 Computing complexity for remaining 1 transitions. Found new complexity const, because: const cost. The final runtime is determined by this resulting transition: Final Guard: 999>=0 && 0>=0 && 999>=0 Final Cost: 2002 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)