Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f63 -> f11 : [ A>=1+B ], cost: 1 17: f63 -> f11 : D'=J, [ B>=A ], cost: 1 2: f11 -> f11 : G'=1, [ D>=E && G==0 ], cost: 1 3: f11 -> f11 : G'=1, [ 1+D>=E && E>=2+D && G==0 ], cost: 1 4: f11 -> f11 : E'=1+D, G'=1, [ E==1+D && G==0 ], cost: 1 5: f11 -> f11 : E'=1+D, G'=1, H'=free, [ free_1>=1+free_2 && E==1+D && G==0 ], cost: 1 6: f11 -> f40 : A'=E, G'=0, H'=free_3, Q'=free_4, J'=1+D, K'=free_5, [ E>=2+D && G==0 ], cost: 1 21: f11 -> f69 : [ 0>=1+G ], cost: 1 22: f11 -> f69 : [ G>=1 ], cost: 1 1: f0 -> f11 : B'=10, C'=20, D'=1, E'=20, F'=0, G'=0, [], cost: 1 7: f40 -> f59 : [ 0>=1+F ], cost: 1 8: f40 -> f59 : [ F>=1 ], cost: 1 9: f40 -> f43 : F'=0, J'=1+J, [ F==0 ], cost: 1 15: f59 -> f63 : [ B>=1+A ], cost: 1 16: f59 -> f63 : E'=-1+A, [ A>=B ], cost: 1 10: f43 -> f43 : J'=1+J, [ K>=1+free_6 ], cost: 1 20: f43 -> f48 : A'=-1+A, [], cost: 1 11: f48 -> f48 : A'=-1+A, [], cost: 1 18: f48 -> f54 : [ A>=J ], cost: 1 19: f48 -> f54 : F'=1, [ J>=1+A ], cost: 1 12: f54 -> f40 : [ 0>=1+F ], cost: 1 13: f54 -> f40 : [ F>=1 ], cost: 1 14: f54 -> f40 : F'=0, H'=free_7, [ F==0 ], cost: 1 Simplified the transitions: Start location: f0 0: f63 -> f11 : [ A>=1+B ], cost: 1 17: f63 -> f11 : D'=J, [ B>=A ], cost: 1 2: f11 -> f11 : G'=1, [ D>=E && G==0 ], cost: 1 3: f11 -> f11 : G'=1, [ 1+D>=E && E>=2+D && G==0 ], cost: 1 4: f11 -> f11 : E'=1+D, G'=1, [ E==1+D && G==0 ], cost: 1 5: f11 -> f11 : E'=1+D, G'=1, H'=free, [ E==1+D && G==0 ], cost: 1 6: f11 -> f40 : A'=E, G'=0, H'=free_3, Q'=free_4, J'=1+D, K'=free_5, [ E>=2+D && G==0 ], cost: 1 1: f0 -> f11 : B'=10, C'=20, D'=1, E'=20, F'=0, G'=0, [], cost: 1 7: f40 -> f59 : [ 0>=1+F ], cost: 1 8: f40 -> f59 : [ F>=1 ], cost: 1 9: f40 -> f43 : F'=0, J'=1+J, [ F==0 ], cost: 1 15: f59 -> f63 : [ B>=1+A ], cost: 1 16: f59 -> f63 : E'=-1+A, [ A>=B ], cost: 1 10: f43 -> f43 : J'=1+J, [], cost: 1 20: f43 -> f48 : A'=-1+A, [], cost: 1 11: f48 -> f48 : A'=-1+A, [], cost: 1 18: f48 -> f54 : [ A>=J ], cost: 1 19: f48 -> f54 : F'=1, [ J>=1+A ], cost: 1 12: f54 -> f40 : [ 0>=1+F ], cost: 1 13: f54 -> f40 : [ F>=1 ], cost: 1 14: f54 -> f40 : F'=0, H'=free_7, [ F==0 ], cost: 1 Eliminating 4 self-loops for location f11 Self-Loop 2 has the metering function: 1-G, resulting in the new transition 23. Self-Loop 3 has unbounded runtime, resulting in the new transition 24. Self-Loop 4 has the metering function: 1-G, resulting in the new transition 25. Self-Loop 5 has the metering function: 1-G, resulting in the new transition 26. Removing the self-loops: 2 3 4 5. Eliminating 1 self-loops for location f43 Self-Loop 10 has unbounded runtime, resulting in the new transition 27. Removing the self-loops: 10. Eliminating 1 self-loops for location f48 Self-Loop 11 has unbounded runtime, resulting in the new transition 28. Removing the self-loops: 11. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f63 -> f11 : [ A>=1+B ], cost: 1 17: f63 -> f11 : D'=J, [ B>=A ], cost: 1 23: f11 -> [9] : G'=1, [ D>=E && G==0 ], cost: 1-G 24: f11 -> [9] : [ 1+D>=E && E>=2+D && G==0 ], cost: INF 25: f11 -> [9] : E'=1+D, G'=1, [ E==1+D && G==0 ], cost: 1-G 26: f11 -> [9] : E'=1+D, G'=1, H'=free, [ E==1+D && G==0 ], cost: 1-G 1: f0 -> f11 : B'=10, C'=20, D'=1, E'=20, F'=0, G'=0, [], cost: 1 7: f40 -> f59 : [ 0>=1+F ], cost: 1 8: f40 -> f59 : [ F>=1 ], cost: 1 9: f40 -> f43 : F'=0, J'=1+J, [ F==0 ], cost: 1 15: f59 -> f63 : [ B>=1+A ], cost: 1 16: f59 -> f63 : E'=-1+A, [ A>=B ], cost: 1 27: f43 -> [10] : [], cost: INF 28: f48 -> [11] : [], cost: INF 12: f54 -> f40 : [ 0>=1+F ], cost: 1 13: f54 -> f40 : [ F>=1 ], cost: 1 14: f54 -> f40 : F'=0, H'=free_7, [ F==0 ], cost: 1 6: [9] -> f40 : A'=E, G'=0, H'=free_3, Q'=free_4, J'=1+D, K'=free_5, [ E>=2+D && G==0 ], cost: 1 20: [10] -> f48 : A'=-1+A, [], cost: 1 18: [11] -> f54 : [ A>=J ], cost: 1 19: [11] -> f54 : F'=1, [ J>=1+A ], cost: 1 Applied simple chaining: Start location: f0 0: f63 -> f11 : [ A>=1+B ], cost: 1 17: f63 -> f11 : D'=J, [ B>=A ], cost: 1 23: f11 -> [9] : G'=1, [ D>=E && G==0 ], cost: 1-G 24: f11 -> [9] : [ 1+D>=E && E>=2+D && G==0 ], cost: INF 25: f11 -> [9] : E'=1+D, G'=1, [ E==1+D && G==0 ], cost: 1-G 26: f11 -> [9] : E'=1+D, G'=1, H'=free, [ E==1+D && G==0 ], cost: 1-G 1: f0 -> f11 : B'=10, C'=20, D'=1, E'=20, F'=0, G'=0, [], cost: 1 7: f40 -> f59 : [ 0>=1+F ], cost: 1 8: f40 -> f59 : [ F>=1 ], cost: 1 9: f40 -> [11] : A'=-1+A, F'=0, J'=1+J, [ F==0 ], cost: INF 15: f59 -> f63 : [ B>=1+A ], cost: 1 16: f59 -> f63 : E'=-1+A, [ A>=B ], cost: 1 12: f54 -> f40 : [ 0>=1+F ], cost: 1 13: f54 -> f40 : [ F>=1 ], cost: 1 14: f54 -> f40 : F'=0, H'=free_7, [ F==0 ], cost: 1 6: [9] -> f40 : A'=E, G'=0, H'=free_3, Q'=free_4, J'=1+D, K'=free_5, [ E>=2+D && G==0 ], cost: 1 18: [11] -> f54 : [ A>=J ], cost: 1 19: [11] -> f54 : F'=1, [ J>=1+A ], cost: 1 Applied chaining over branches and pruning: Start location: f0 29: f11 -> [12] : G'=1, [ D>=E && G==0 ], cost: 1-G 30: f11 -> [13] : [ 1+D>=E && E>=2+D && G==0 ], cost: INF 31: f11 -> [14] : E'=1+D, G'=1, [ E==1+D && G==0 ], cost: 1-G 32: f11 -> [15] : E'=1+D, G'=1, H'=free, [ E==1+D && G==0 ], cost: 1-G 1: f0 -> f11 : B'=10, C'=20, D'=1, E'=20, F'=0, G'=0, [], cost: 1 Applied chaining over branches and pruning: Start location: f0 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 Computing complexity for remaining 0 transitions. The final runtime is determined by this resulting transition: Final Guard: Final Cost: 1 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)