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