Trying to load file: main.koat Initial Control flow graph problem: Start location: evaleasy2start 0: evaleasy2start -> evaleasy2entryin : [], cost: 1 1: evaleasy2entryin -> evaleasy2bb1in : [], cost: 1 2: evaleasy2bb1in -> evaleasy2bbin : [ A>=1 ], cost: 1 3: evaleasy2bb1in -> evaleasy2returnin : [ 0>=A ], cost: 1 4: evaleasy2bbin -> evaleasy2bb1in : A'=-1+A, [], cost: 1 5: evaleasy2returnin -> evaleasy2stop : [], cost: 1 Simplified the transitions: Start location: evaleasy2start 0: evaleasy2start -> evaleasy2entryin : [], cost: 1 1: evaleasy2entryin -> evaleasy2bb1in : [], cost: 1 2: evaleasy2bb1in -> evaleasy2bbin : [ A>=1 ], cost: 1 4: evaleasy2bbin -> evaleasy2bb1in : A'=-1+A, [], cost: 1 Applied simple chaining: Start location: evaleasy2start 0: evaleasy2start -> evaleasy2bb1in : [], cost: 2 2: evaleasy2bb1in -> evaleasy2bb1in : A'=-1+A, [ A>=1 ], cost: 2 Eliminating 1 self-loops for location evaleasy2bb1in Self-Loop 2 has the metering function: A, resulting in the new transition 6. Removing the self-loops: 2. Removed all Self-loops using metering functions (where possible): Start location: evaleasy2start 0: evaleasy2start -> evaleasy2bb1in : [], cost: 2 6: evaleasy2bb1in -> [6] : A'=0, [ A>=1 ], cost: 2*A Applied simple chaining: Start location: evaleasy2start 0: evaleasy2start -> [6] : A'=0, [ A>=1 ], cost: 2+2*A Final control flow graph problem, now checking costs for infinitely many models: Start location: evaleasy2start 0: evaleasy2start -> [6] : A'=0, [ A>=1 ], cost: 2+2*A Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: 2+2*A and guard: A>=1: A: Pos Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: A>=1 Final Cost: 2+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),?)