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