Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f2 -> f2 : A'=-1+A, [ A>=1 ], cost: 1 2: f2 -> f2 : A'=free_1, B'=-1+B, [ B>=1 && 0>=A ], cost: 1 1: f0 -> f2 : A'=free, B'=-1+B, [ B>=1 ], cost: 1 Eliminating 2 self-loops for location f2 Self-Loop 0 has the metering function: A, resulting in the new transition 3. Found this metering function when nesting loops: B, and nested parallel self-loops 4 (outer loop) and 3 (inner loop), obtaining the new transitions: 5, 6. Removing the self-loops: 0 2 4. Adding an epsilon transition (to model nonexecution of the loops): 7. Removed all Self-loops using metering functions (where possible): Start location: f0 3: f2 -> [2] : A'=0, [ A>=1 ], cost: A 5: f2 -> [2] : A'=0, B'=0, [ B>=1 && 0>=A && free_1>=1 ], cost: free_1*B+B 6: f2 -> [2] : A'=0, B'=0, [ A>=1 && B>=1 && 0>=0 && free_1>=1 ], cost: free_1*B+B+A 7: f2 -> [2] : [], cost: 0 1: f0 -> f2 : A'=free, B'=-1+B, [ B>=1 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 8: f0 -> [2] : A'=0, B'=-1+B, [ B>=1 && free>=1 ], cost: 1+free 9: f0 -> [2] : A'=0, B'=0, [ B>=1 && -1+B>=1 && 0>=free && free_1>=1 ], cost: B+free_1*(-1+B) 10: f0 -> [2] : A'=0, B'=0, [ B>=1 && free>=1 && -1+B>=1 && 0>=0 && free_1>=1 ], cost: B+free_1*(-1+B)+free Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 8: f0 -> [2] : A'=0, B'=-1+B, [ B>=1 && free>=1 ], cost: 1+free 9: f0 -> [2] : A'=0, B'=0, [ B>=1 && -1+B>=1 && 0>=free && free_1>=1 ], cost: B+free_1*(-1+B) 10: f0 -> [2] : A'=0, B'=0, [ B>=1 && free>=1 && -1+B>=1 && 0>=0 && free_1>=1 ], cost: B+free_1*(-1+B)+free Computing complexity for remaining 3 transitions. Found configuration with infinitely models for cost: 1+free and guard: B>=1 && free>=1: B: Pos, free: Pos Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: B>=1 && free>=1 Final Cost: 1+free Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)