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