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