Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f10 : A'=1, [], cost: 1 1: f10 -> f13 : B'=1, [ 5>=A ], cost: 1 10: f10 -> f21 : A'=1, [ A>=6 ], cost: 1 9: f13 -> f10 : A'=1+A, [ B>=6 ], cost: 1 2: f13 -> f13 : B'=1+B, [ 5>=B ], cost: 1 3: f21 -> f24 : B'=1, [ 5>=A ], cost: 1 8: f21 -> f39 : [ A>=6 ], cost: 1 7: f24 -> f21 : A'=1+A, [ B>=6 ], cost: 1 4: f24 -> f27 : C'=1, [ 5>=B ], cost: 1 6: f27 -> f24 : B'=1+B, [ C>=6 ], cost: 1 5: f27 -> f27 : C'=1+C, [ 5>=C ], cost: 1 Simplified the transitions: Start location: f0 0: f0 -> f10 : A'=1, [], cost: 1 1: f10 -> f13 : B'=1, [ 5>=A ], cost: 1 10: f10 -> f21 : A'=1, [ A>=6 ], cost: 1 9: f13 -> f10 : A'=1+A, [ B>=6 ], cost: 1 2: f13 -> f13 : B'=1+B, [ 5>=B ], cost: 1 3: f21 -> f24 : B'=1, [ 5>=A ], cost: 1 7: f24 -> f21 : A'=1+A, [ B>=6 ], cost: 1 4: f24 -> f27 : C'=1, [ 5>=B ], cost: 1 6: f27 -> f24 : B'=1+B, [ C>=6 ], cost: 1 5: f27 -> f27 : C'=1+C, [ 5>=C ], cost: 1 Eliminating 1 self-loops for location f13 Self-Loop 2 has the metering function: 6-B, resulting in the new transition 11. Removing the self-loops: 2. Eliminating 1 self-loops for location f27 Self-Loop 5 has the metering function: 6-C, resulting in the new transition 12. Removing the self-loops: 5. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f10 : A'=1, [], cost: 1 1: f10 -> f13 : B'=1, [ 5>=A ], cost: 1 10: f10 -> f21 : A'=1, [ A>=6 ], cost: 1 11: f13 -> [7] : B'=6, [ 5>=B ], cost: 6-B 3: f21 -> f24 : B'=1, [ 5>=A ], cost: 1 7: f24 -> f21 : A'=1+A, [ B>=6 ], cost: 1 4: f24 -> f27 : C'=1, [ 5>=B ], cost: 1 12: f27 -> [8] : C'=6, [ 5>=C ], cost: 6-C 9: [7] -> f10 : A'=1+A, [ B>=6 ], cost: 1 6: [8] -> f24 : B'=1+B, [ C>=6 ], cost: 1 Applied simple chaining: Start location: f0 0: f0 -> f10 : A'=1, [], cost: 1 1: f10 -> f10 : A'=1+A, B'=6, [ 5>=A && 5>=1 && 6>=6 ], cost: 7 10: f10 -> f21 : A'=1, [ A>=6 ], cost: 1 3: f21 -> f24 : B'=1, [ 5>=A ], cost: 1 7: f24 -> f21 : A'=1+A, [ B>=6 ], cost: 1 4: f24 -> f24 : B'=1+B, C'=6, [ 5>=B && 5>=1 && 6>=6 ], cost: 7 Eliminating 1 self-loops for location f10 Self-Loop 1 has the metering function: 6-A, resulting in the new transition 13. Removing the self-loops: 1. Eliminating 1 self-loops for location f24 Self-Loop 4 has the metering function: 6-B, resulting in the new transition 14. Removing the self-loops: 4. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f10 : A'=1, [], cost: 1 13: f10 -> [9] : A'=6, B'=6, [ 5>=A ], cost: 42-7*A 3: f21 -> f24 : B'=1, [ 5>=A ], cost: 1 14: f24 -> [10] : B'=6, C'=6, [ 5>=B ], cost: 42-7*B 10: [9] -> f21 : A'=1, [ A>=6 ], cost: 1 7: [10] -> f21 : A'=1+A, [ B>=6 ], cost: 1 Applied simple chaining: Start location: f0 0: f0 -> f21 : A'=1, B'=6, [ 5>=1 && 6>=6 ], cost: 37 3: f21 -> f21 : A'=1+A, B'=6, C'=6, [ 5>=A && 5>=1 && 6>=6 ], cost: 37 Eliminating 1 self-loops for location f21 Self-Loop 3 has the metering function: 6-A, resulting in the new transition 15. Removing the self-loops: 3. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f21 : A'=1, B'=6, [ 5>=1 && 6>=6 ], cost: 37 15: f21 -> [11] : A'=6, B'=6, C'=6, [ 5>=A ], cost: 222-37*A Applied simple chaining: Start location: f0 0: f0 -> [11] : A'=6, B'=6, C'=6, [ 5>=1 && 6>=6 && 5>=1 ], cost: 222 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 0: f0 -> [11] : A'=6, B'=6, C'=6, [ 5>=1 && 6>=6 && 5>=1 ], cost: 222 Computing complexity for remaining 1 transitions. Found new complexity const, because: const cost. The final runtime is determined by this resulting transition: Final Guard: 5>=1 && 6>=6 && 5>=1 Final Cost: 222 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)