Trying to load file: main.koat Initial Control flow graph problem: Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectentryin : [], cost: 1 1: evalrealselectentryin -> evalrealselectbb6in : A'=0, [], cost: 1 2: evalrealselectbb6in -> evalrealselectbbin : [ B>=2+A ], cost: 1 3: evalrealselectbb6in -> evalrealselectreturnin : [ 1+A>=B ], cost: 1 4: evalrealselectbbin -> evalrealselectbb4in : C'=1+A, [], cost: 1 10: evalrealselectreturnin -> evalrealselectstop : [], cost: 1 5: evalrealselectbb4in -> evalrealselectbb1in : [ B>=1+C ], cost: 1 6: evalrealselectbb4in -> evalrealselectbb5in : [ C>=B ], cost: 1 7: evalrealselectbb1in -> evalrealselectbb4in : C'=1+C, [ free_1>=1+free ], cost: 1 8: evalrealselectbb1in -> evalrealselectbb4in : C'=1+C, [ free_2>=free_3 ], cost: 1 9: evalrealselectbb5in -> evalrealselectbb6in : A'=1+A, [], cost: 1 Removing duplicate transition: 7. Simplified the transitions: Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectentryin : [], cost: 1 1: evalrealselectentryin -> evalrealselectbb6in : A'=0, [], cost: 1 2: evalrealselectbb6in -> evalrealselectbbin : [ B>=2+A ], cost: 1 4: evalrealselectbbin -> evalrealselectbb4in : C'=1+A, [], cost: 1 5: evalrealselectbb4in -> evalrealselectbb1in : [ B>=1+C ], cost: 1 6: evalrealselectbb4in -> evalrealselectbb5in : [ C>=B ], cost: 1 8: evalrealselectbb1in -> evalrealselectbb4in : C'=1+C, [], cost: 1 9: evalrealselectbb5in -> evalrealselectbb6in : A'=1+A, [], cost: 1 Applied simple chaining: Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectbb6in : A'=0, [], cost: 2 2: evalrealselectbb6in -> evalrealselectbb4in : C'=1+A, [ B>=2+A ], cost: 2 6: evalrealselectbb4in -> evalrealselectbb6in : A'=1+A, [ C>=B ], cost: 2 5: evalrealselectbb4in -> evalrealselectbb4in : C'=1+C, [ B>=1+C ], cost: 2 Eliminating 1 self-loops for location evalrealselectbb4in Self-Loop 5 has the metering function: B-C, resulting in the new transition 11. Removing the self-loops: 5. Removed all Self-loops using metering functions (where possible): Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectbb6in : A'=0, [], cost: 2 2: evalrealselectbb6in -> evalrealselectbb4in : C'=1+A, [ B>=2+A ], cost: 2 11: evalrealselectbb4in -> [9] : C'=B, [ B>=1+C ], cost: 2*B-2*C 6: [9] -> evalrealselectbb6in : A'=1+A, [ C>=B ], cost: 2 Applied simple chaining: Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectbb6in : A'=0, [], cost: 2 2: evalrealselectbb6in -> evalrealselectbb6in : A'=1+A, C'=B, [ B>=2+A && B>=2+A && B>=B ], cost: 2+2*B-2*A Eliminating 1 self-loops for location evalrealselectbb6in Self-Loop 2 has the metering function: -1+B-A, resulting in the new transition 12. Removing the self-loops: 2. Removed all Self-loops using metering functions (where possible): Start location: evalrealselectstart 0: evalrealselectstart -> evalrealselectbb6in : A'=0, [], cost: 2 12: evalrealselectbb6in -> [10] : A'=-1+B, C'=B, [ B>=2+A ], cost: -3+3*B+2*B*(-1+B-A)-(-1+B-A)^2-3*A-2*(-1+B-A)*A Applied simple chaining: Start location: evalrealselectstart 0: evalrealselectstart -> [10] : A'=-1+B, C'=B, [ B>=2 ], cost: -1-(-1+B)^2+3*B+2*B*(-1+B) Final control flow graph problem, now checking costs for infinitely many models: Start location: evalrealselectstart 0: evalrealselectstart -> [10] : A'=-1+B, C'=B, [ B>=2 ], cost: -1-(-1+B)^2+3*B+2*B*(-1+B) Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: -1-(-1+B)^2+3*B+2*B*(-1+B) and guard: B>=2: B: Pos Found new complexity n^2, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: B>=2 Final Cost: -1-(-1+B)^2+3*B+2*B*(-1+B) Obtained the following complexity w.r.t. the length of the input n: Complexity class: n^2 Complexity value: 2 WORST_CASE(Omega(n^2),?)