Trying to load file: main.koat Initial Control flow graph problem: Start location: start 0: f2 -> f2 : B'=1+B, D'=free, [ A>=B && C>=free ], cost: 1 1: f2 -> f2 : B'=1+B, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1 81: f2 -> f15 : [ B>=1+A && C>=1 ], cost: 1 80: f2 -> f1 : [ B>=1+A && 0>=C ], cost: 1 2: f15 -> f15 : B'=1+B, F'=0, G'=0, [ A>=B ], cost: 1 3: f15 -> f15 : B'=1+B, F'=free_4, G'=free_3, H'=H+free_3, [ A>=B && 0>=1+free_4 ], cost: 1 4: f15 -> f15 : B'=1+B, F'=free_6, G'=free_5, H'=H+free_5, [ A>=B && free_6>=1 ], cost: 1 79: f15 -> f26 : Q'=1, [ B>=1+A ], cost: 1 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f81 : Q'=0, [ 200>=J && Q==0 ], cost: 1 78: f26 -> f1 : [ J>=201 ], cost: 1 7: f30 -> f33 : [ A>=B ], cost: 1 77: f30 -> f42 : [ B>=1+A ], cost: 1 76: f33 -> f30 : B'=1+B, [ K>=1+A ], cost: 1 8: f33 -> f33 : K'=1+K, [ A>=K ], cost: 1 14: f42 -> f42 : L'=1+L, M'=0, [ A>=1+L ], cost: 1 9: f42 -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: f42 -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: f42 -> f68 : [ L>=A ], cost: 1 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f51 : H'=0, [ A>=K ], cost: 1 12: f51 -> f51 : B'=1+B, H'=free_9, [ A>=B ], cost: 1 73: f51 -> f58 : H'=free_38, [ B>=1+A ], cost: 1 72: f58 -> f47 : K'=1+K, [ B>=1+A ], cost: 1 13: f58 -> f58 : B'=1+B, [ A>=B ], cost: 1 15: f68 -> f72 : [ A>=B ], cost: 1 71: f68 -> f152 : [ B>=1+A ], cost: 1 70: f72 -> f68 : B'=1+B, [ K>=B ], cost: 1 16: f72 -> f72 : K'=1+K, [ B>=1+K ], cost: 1 18: f81 -> f81 : B'=1+B, [ A>=B ], cost: 1 69: f81 -> f87 : [ B>=1+A ], cost: 1 19: f87 -> f90 : [ A>=B ], cost: 1 68: f87 -> f100 : Z'=1, [ B>=1+A ], cost: 1 67: f90 -> f87 : B'=1+B, [ K>=1+A ], cost: 1 20: f90 -> f90 : H'=free_10, K'=1+K, [ A>=K ], cost: 1 21: f100 -> f103 : [ A>=B ], cost: 1 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 62: f103 -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: f103 -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 22: f103 -> f103 : H'=free_11, K'=1+K, [ A>=K ], cost: 1 23: f119 -> f122 : [ A>=B ], cost: 1 61: f119 -> f131 : [ B>=1+A ], cost: 1 60: f122 -> f119 : B'=1+B, [ K>=1+A ], cost: 1 24: f122 -> f122 : H'=free_12, K'=1+K, [ A>=K ], cost: 1 25: f131 -> f131 : B'=1+B, F'=0, N'=0, [ A>=B ], cost: 1 26: f131 -> f131 : B'=1+B, F'=free_14, N'=free_13, O'=O+free_13, [ A>=B && 0>=1+free_14 ], cost: 1 27: f131 -> f131 : B'=1+B, F'=free_16, N'=free_15, O'=O+free_15, [ A>=B && free_16>=1 ], cost: 1 59: f131 -> f141 : [ B>=1+A ], cost: 1 28: f141 -> f141 : B'=1+B, [ A>=B ], cost: 1 58: f141 -> f147 : [ B>=1+A ], cost: 1 29: f147 -> f147 : B'=1+B, [ A>=B ], cost: 1 57: f147 -> f152 : [ B>=1+A ], cost: 1 30: f152 -> f155 : [ A>=B ], cost: 1 56: f152 -> f164 : [ B>=1+A ], cost: 1 55: f155 -> f152 : B'=1+B, [ K>=1+A ], cost: 1 31: f155 -> f155 : H'=free_17, K'=1+K, [ A>=K ], cost: 1 32: f164 -> f167 : [ B>=1 ], cost: 1 54: f164 -> f176 : [ 0>=B ], cost: 1 53: f167 -> f164 : B'=-1+B, [ K>=1+B ], cost: 1 33: f167 -> f167 : H'=free_18, K'=1+K, [ B>=K ], cost: 1 34: f176 -> f176 : B'=1+B, [ A>=B ], cost: 1 52: f176 -> f184 : Y'=free_31, [ B>=1+A ], cost: 1 35: f184 -> f187 : [ A>=B ], cost: 1 51: f184 -> f199 : C'=0, [ B>=1+A ], cost: 1 50: f187 -> f184 : B'=1+B, [ K>=1+A ], cost: 1 36: f187 -> f187 : H'=free_19, K'=1+K, [ A>=K ], cost: 1 37: f199 -> f199 : B'=1+B, P'=free_20, [ A>=B && C>=free_20 ], cost: 1 38: f199 -> f199 : B'=1+B, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1 47: f199 -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: f199 -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: f199 -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 46: f210 -> f26 : J'=1+J, [ B>=1+A ], cost: 1 39: f210 -> f210 : B'=1+B, [ A>=B ], cost: 1 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 45: f218 -> f1 : [ B>=1+A && 0>=1+C ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 Simplified the transitions: Start location: start 0: f2 -> f2 : B'=1+B, D'=free, [ A>=B && C>=free ], cost: 1 1: f2 -> f2 : B'=1+B, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1 81: f2 -> f15 : [ B>=1+A && C>=1 ], cost: 1 2: f15 -> f15 : B'=1+B, F'=0, G'=0, [ A>=B ], cost: 1 3: f15 -> f15 : B'=1+B, F'=free_4, G'=free_3, H'=H+free_3, [ A>=B && 0>=1+free_4 ], cost: 1 4: f15 -> f15 : B'=1+B, F'=free_6, G'=free_5, H'=H+free_5, [ A>=B && free_6>=1 ], cost: 1 79: f15 -> f26 : Q'=1, [ B>=1+A ], cost: 1 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f81 : Q'=0, [ 200>=J && Q==0 ], cost: 1 7: f30 -> f33 : [ A>=B ], cost: 1 77: f30 -> f42 : [ B>=1+A ], cost: 1 76: f33 -> f30 : B'=1+B, [ K>=1+A ], cost: 1 8: f33 -> f33 : K'=1+K, [ A>=K ], cost: 1 14: f42 -> f42 : L'=1+L, M'=0, [ A>=1+L ], cost: 1 9: f42 -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: f42 -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: f42 -> f68 : [ L>=A ], cost: 1 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f51 : H'=0, [ A>=K ], cost: 1 12: f51 -> f51 : B'=1+B, H'=free_9, [ A>=B ], cost: 1 73: f51 -> f58 : H'=free_38, [ B>=1+A ], cost: 1 72: f58 -> f47 : K'=1+K, [ B>=1+A ], cost: 1 13: f58 -> f58 : B'=1+B, [ A>=B ], cost: 1 15: f68 -> f72 : [ A>=B ], cost: 1 71: f68 -> f152 : [ B>=1+A ], cost: 1 70: f72 -> f68 : B'=1+B, [ K>=B ], cost: 1 16: f72 -> f72 : K'=1+K, [ B>=1+K ], cost: 1 18: f81 -> f81 : B'=1+B, [ A>=B ], cost: 1 69: f81 -> f87 : [ B>=1+A ], cost: 1 19: f87 -> f90 : [ A>=B ], cost: 1 68: f87 -> f100 : Z'=1, [ B>=1+A ], cost: 1 67: f90 -> f87 : B'=1+B, [ K>=1+A ], cost: 1 20: f90 -> f90 : H'=free_10, K'=1+K, [ A>=K ], cost: 1 21: f100 -> f103 : [ A>=B ], cost: 1 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 62: f103 -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: f103 -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 22: f103 -> f103 : H'=free_11, K'=1+K, [ A>=K ], cost: 1 23: f119 -> f122 : [ A>=B ], cost: 1 61: f119 -> f131 : [ B>=1+A ], cost: 1 60: f122 -> f119 : B'=1+B, [ K>=1+A ], cost: 1 24: f122 -> f122 : H'=free_12, K'=1+K, [ A>=K ], cost: 1 25: f131 -> f131 : B'=1+B, F'=0, N'=0, [ A>=B ], cost: 1 26: f131 -> f131 : B'=1+B, F'=free_14, N'=free_13, O'=O+free_13, [ A>=B && 0>=1+free_14 ], cost: 1 27: f131 -> f131 : B'=1+B, F'=free_16, N'=free_15, O'=O+free_15, [ A>=B && free_16>=1 ], cost: 1 59: f131 -> f141 : [ B>=1+A ], cost: 1 28: f141 -> f141 : B'=1+B, [ A>=B ], cost: 1 58: f141 -> f147 : [ B>=1+A ], cost: 1 29: f147 -> f147 : B'=1+B, [ A>=B ], cost: 1 57: f147 -> f152 : [ B>=1+A ], cost: 1 30: f152 -> f155 : [ A>=B ], cost: 1 56: f152 -> f164 : [ B>=1+A ], cost: 1 55: f155 -> f152 : B'=1+B, [ K>=1+A ], cost: 1 31: f155 -> f155 : H'=free_17, K'=1+K, [ A>=K ], cost: 1 32: f164 -> f167 : [ B>=1 ], cost: 1 54: f164 -> f176 : [ 0>=B ], cost: 1 53: f167 -> f164 : B'=-1+B, [ K>=1+B ], cost: 1 33: f167 -> f167 : H'=free_18, K'=1+K, [ B>=K ], cost: 1 34: f176 -> f176 : B'=1+B, [ A>=B ], cost: 1 52: f176 -> f184 : Y'=free_31, [ B>=1+A ], cost: 1 35: f184 -> f187 : [ A>=B ], cost: 1 51: f184 -> f199 : C'=0, [ B>=1+A ], cost: 1 50: f187 -> f184 : B'=1+B, [ K>=1+A ], cost: 1 36: f187 -> f187 : H'=free_19, K'=1+K, [ A>=K ], cost: 1 37: f199 -> f199 : B'=1+B, P'=free_20, [ A>=B && C>=free_20 ], cost: 1 38: f199 -> f199 : B'=1+B, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1 47: f199 -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: f199 -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: f199 -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 46: f210 -> f26 : J'=1+J, [ B>=1+A ], cost: 1 39: f210 -> f210 : B'=1+B, [ A>=B ], cost: 1 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 Eliminating 2 self-loops for location f2 Self-Loop 0 has the metering function: 1-B+A, resulting in the new transition 83. Self-Loop 1 has the metering function: 1-B+A, resulting in the new transition 84. Removing the self-loops: 0 1. Eliminating 3 self-loops for location f15 Self-Loop 2 has the metering function: 1-B+A, resulting in the new transition 85. Self-Loop 3 has the metering function: 1-B+A, resulting in the new transition 86. Self-Loop 4 has the metering function: 1-B+A, resulting in the new transition 87. Removing the self-loops: 2 3 4. Eliminating 1 self-loops for location f33 Self-Loop 8 has the metering function: 1-K+A, resulting in the new transition 88. Removing the self-loops: 8. Eliminating 1 self-loops for location f42 Self-Loop 14 has the metering function: -L+A, resulting in the new transition 89. Removing the self-loops: 14. Eliminating 1 self-loops for location f51 Self-Loop 12 has the metering function: 1-B+A, resulting in the new transition 90. Removing the self-loops: 12. Eliminating 1 self-loops for location f58 Self-Loop 13 has the metering function: 1-B+A, resulting in the new transition 91. Removing the self-loops: 13. Eliminating 1 self-loops for location f72 Self-Loop 16 has the metering function: -K+B, resulting in the new transition 92. Removing the self-loops: 16. Eliminating 1 self-loops for location f81 Self-Loop 18 has the metering function: 1-B+A, resulting in the new transition 93. Removing the self-loops: 18. Eliminating 1 self-loops for location f90 Self-Loop 20 has the metering function: 1-K+A, resulting in the new transition 94. Removing the self-loops: 20. Eliminating 1 self-loops for location f103 Self-Loop 22 has the metering function: 1-K+A, resulting in the new transition 95. Removing the self-loops: 22. Eliminating 1 self-loops for location f122 Self-Loop 24 has the metering function: 1-K+A, resulting in the new transition 96. Removing the self-loops: 24. Eliminating 3 self-loops for location f131 Self-Loop 25 has the metering function: 1-B+A, resulting in the new transition 97. Self-Loop 26 has the metering function: 1-B+A, resulting in the new transition 98. Self-Loop 27 has the metering function: 1-B+A, resulting in the new transition 99. Removing the self-loops: 25 26 27. Eliminating 1 self-loops for location f141 Self-Loop 28 has the metering function: 1-B+A, resulting in the new transition 100. Removing the self-loops: 28. Eliminating 1 self-loops for location f147 Self-Loop 29 has the metering function: 1-B+A, resulting in the new transition 101. Removing the self-loops: 29. Eliminating 1 self-loops for location f155 Self-Loop 31 has the metering function: 1-K+A, resulting in the new transition 102. Removing the self-loops: 31. Eliminating 1 self-loops for location f167 Self-Loop 33 has the metering function: 1-K+B, resulting in the new transition 103. Removing the self-loops: 33. Eliminating 1 self-loops for location f176 Self-Loop 34 has the metering function: 1-B+A, resulting in the new transition 104. Removing the self-loops: 34. Eliminating 1 self-loops for location f187 Self-Loop 36 has the metering function: 1-K+A, resulting in the new transition 105. Removing the self-loops: 36. Eliminating 2 self-loops for location f199 Self-Loop 37 has the metering function: 1-B+A, resulting in the new transition 106. Self-Loop 38 has the metering function: 1-B+A, resulting in the new transition 107. Removing the self-loops: 37 38. Eliminating 1 self-loops for location f210 Self-Loop 39 has the metering function: 1-B+A, resulting in the new transition 108. Removing the self-loops: 39. Removed all Self-loops using metering functions (where possible): Start location: start 83: f2 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f2 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f15 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f15 -> [35] : B'=1+A, F'=free_4, G'=free_3, H'=H-(-1+B-A)*free_3, [ A>=B && 0>=1+free_4 ], cost: 1-B+A 87: f15 -> [35] : B'=1+A, F'=free_6, G'=free_5, H'=H-free_5*(-1+B-A), [ A>=B && free_6>=1 ], cost: 1-B+A 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f81 : Q'=0, [ 200>=J && Q==0 ], cost: 1 7: f30 -> f33 : [ A>=B ], cost: 1 77: f30 -> f42 : [ B>=1+A ], cost: 1 88: f33 -> [36] : K'=1+A, [ A>=K ], cost: 1-K+A 89: f42 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f51 : H'=0, [ A>=K ], cost: 1 90: f51 -> [38] : B'=1+A, H'=free_9, [ A>=B ], cost: 1-B+A 91: f58 -> [39] : B'=1+A, [ A>=B ], cost: 1-B+A 15: f68 -> f72 : [ A>=B ], cost: 1 71: f68 -> f152 : [ B>=1+A ], cost: 1 92: f72 -> [40] : K'=B, [ B>=1+K ], cost: -K+B 93: f81 -> [41] : B'=1+A, [ A>=B ], cost: 1-B+A 19: f87 -> f90 : [ A>=B ], cost: 1 68: f87 -> f100 : Z'=1, [ B>=1+A ], cost: 1 94: f90 -> [42] : H'=free_10, K'=1+A, [ A>=K ], cost: 1-K+A 21: f100 -> f103 : [ A>=B ], cost: 1 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 95: f103 -> [43] : H'=free_11, K'=1+A, [ A>=K ], cost: 1-K+A 23: f119 -> f122 : [ A>=B ], cost: 1 61: f119 -> f131 : [ B>=1+A ], cost: 1 96: f122 -> [44] : H'=free_12, K'=1+A, [ A>=K ], cost: 1-K+A 97: f131 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f131 -> [45] : B'=1+A, F'=free_14, N'=free_13, O'=O-(-1+B-A)*free_13, [ A>=B && 0>=1+free_14 ], cost: 1-B+A 99: f131 -> [45] : B'=1+A, F'=free_16, N'=free_15, O'=-(-1+B-A)*free_15+O, [ A>=B && free_16>=1 ], cost: 1-B+A 100: f141 -> [46] : B'=1+A, [ A>=B ], cost: 1-B+A 101: f147 -> [47] : B'=1+A, [ A>=B ], cost: 1-B+A 30: f152 -> f155 : [ A>=B ], cost: 1 56: f152 -> f164 : [ B>=1+A ], cost: 1 102: f155 -> [48] : H'=free_17, K'=1+A, [ A>=K ], cost: 1-K+A 32: f164 -> f167 : [ B>=1 ], cost: 1 54: f164 -> f176 : [ 0>=B ], cost: 1 103: f167 -> [49] : H'=free_18, K'=1+B, [ B>=K ], cost: 1-K+B 104: f176 -> [50] : B'=1+A, [ A>=B ], cost: 1-B+A 35: f184 -> f187 : [ A>=B ], cost: 1 51: f184 -> f199 : C'=0, [ B>=1+A ], cost: 1 105: f187 -> [51] : H'=free_19, K'=1+A, [ A>=K ], cost: 1-K+A 106: f199 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f199 -> [52] : B'=1+A, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1-B+A 108: f210 -> [53] : B'=1+A, [ A>=B ], cost: 1-B+A 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 81: [34] -> f15 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f26 : Q'=1, [ B>=1+A ], cost: 1 76: [36] -> f30 : B'=1+B, [ K>=1+A ], cost: 1 9: [37] -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f68 : [ L>=A ], cost: 1 73: [38] -> f58 : H'=free_38, [ B>=1+A ], cost: 1 72: [39] -> f47 : K'=1+K, [ B>=1+A ], cost: 1 70: [40] -> f68 : B'=1+B, [ K>=B ], cost: 1 69: [41] -> f87 : [ B>=1+A ], cost: 1 67: [42] -> f87 : B'=1+B, [ K>=1+A ], cost: 1 62: [43] -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 60: [44] -> f119 : B'=1+B, [ K>=1+A ], cost: 1 59: [45] -> f141 : [ B>=1+A ], cost: 1 58: [46] -> f147 : [ B>=1+A ], cost: 1 57: [47] -> f152 : [ B>=1+A ], cost: 1 55: [48] -> f152 : B'=1+B, [ K>=1+A ], cost: 1 53: [49] -> f164 : B'=-1+B, [ K>=1+B ], cost: 1 52: [50] -> f184 : Y'=free_31, [ B>=1+A ], cost: 1 50: [51] -> f184 : B'=1+B, [ K>=1+A ], cost: 1 47: [52] -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: [52] -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 46: [53] -> f26 : J'=1+J, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: start 83: f2 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f2 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f15 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f15 -> [35] : B'=1+A, F'=free_4, G'=free_3, H'=H-(-1+B-A)*free_3, [ A>=B && 0>=1+free_4 ], cost: 1-B+A 87: f15 -> [35] : B'=1+A, F'=free_6, G'=free_5, H'=H-free_5*(-1+B-A), [ A>=B && free_6>=1 ], cost: 1-B+A 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f87 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 7: f30 -> f30 : B'=1+B, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 77: f30 -> f42 : [ B>=1+A ], cost: 1 89: f42 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f58 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f58 -> f47 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 15: f68 -> f68 : B'=1+B, K'=B, [ A>=B && B>=1+K && B>=B ], cost: 2-K+B 71: f68 -> f152 : [ B>=1+A ], cost: 1 19: f87 -> f87 : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 68: f87 -> f100 : Z'=1, [ B>=1+A ], cost: 1 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 21: f100 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 23: f119 -> f119 : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 61: f119 -> f131 : [ B>=1+A ], cost: 1 97: f131 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f131 -> [45] : B'=1+A, F'=free_14, N'=free_13, O'=O-(-1+B-A)*free_13, [ A>=B && 0>=1+free_14 ], cost: 1-B+A 99: f131 -> [45] : B'=1+A, F'=free_16, N'=free_15, O'=-(-1+B-A)*free_15+O, [ A>=B && free_16>=1 ], cost: 1-B+A 100: f141 -> f147 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f147 -> f152 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 30: f152 -> f152 : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 56: f152 -> f164 : [ B>=1+A ], cost: 1 32: f164 -> f164 : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K && 1+B>=1+B ], cost: 3-K+B 54: f164 -> f184 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 35: f184 -> f184 : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 51: f184 -> f199 : C'=0, [ B>=1+A ], cost: 1 106: f199 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f199 -> [52] : B'=1+A, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1-B+A 108: f210 -> f26 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 81: [34] -> f15 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f26 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f68 : [ L>=A ], cost: 1 62: [43] -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f141 : [ B>=1+A ], cost: 1 47: [52] -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: [52] -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 Eliminating 1 self-loops for location f30 Removing the self-loops: 7. Adding an epsilon transition (to model nonexecution of the loops): 110. Eliminating 1 self-loops for location f68 Self-Loop 15 has the metering function: 1-B+A, resulting in the new transition 111. Removing the self-loops: 15. Eliminating 1 self-loops for location f87 Removing the self-loops: 19. Adding an epsilon transition (to model nonexecution of the loops): 113. Eliminating 1 self-loops for location f119 Removing the self-loops: 23. Adding an epsilon transition (to model nonexecution of the loops): 115. Eliminating 1 self-loops for location f152 Removing the self-loops: 30. Adding an epsilon transition (to model nonexecution of the loops): 117. Eliminating 1 self-loops for location f164 Removing the self-loops: 32. Adding an epsilon transition (to model nonexecution of the loops): 119. Eliminating 1 self-loops for location f184 Removing the self-loops: 35. Adding an epsilon transition (to model nonexecution of the loops): 121. Removed all Self-loops using metering functions (where possible): Start location: start 83: f2 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f2 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f15 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f15 -> [35] : B'=1+A, F'=free_4, G'=free_3, H'=H-(-1+B-A)*free_3, [ A>=B && 0>=1+free_4 ], cost: 1-B+A 87: f15 -> [35] : B'=1+A, F'=free_6, G'=free_5, H'=H-free_5*(-1+B-A), [ A>=B && free_6>=1 ], cost: 1-B+A 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f87 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 109: f30 -> [54] : B'=1+B, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 110: f30 -> [54] : [], cost: 0 89: f42 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f58 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f58 -> f47 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 111: f68 -> [55] : B'=1+A, K'=A, [ A>=B && B>=1+K ], cost: 3-3*B+3*A 112: f87 -> [56] : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 113: f87 -> [56] : [], cost: 0 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 21: f100 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 114: f119 -> [57] : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 115: f119 -> [57] : [], cost: 0 97: f131 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f131 -> [45] : B'=1+A, F'=free_14, N'=free_13, O'=O-(-1+B-A)*free_13, [ A>=B && 0>=1+free_14 ], cost: 1-B+A 99: f131 -> [45] : B'=1+A, F'=free_16, N'=free_15, O'=-(-1+B-A)*free_15+O, [ A>=B && free_16>=1 ], cost: 1-B+A 100: f141 -> f147 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f147 -> f152 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 116: f152 -> [58] : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 117: f152 -> [58] : [], cost: 0 118: f164 -> [59] : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K ], cost: 3-K+B 119: f164 -> [59] : [], cost: 0 120: f184 -> [60] : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 121: f184 -> [60] : [], cost: 0 106: f199 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f199 -> [52] : B'=1+A, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1-B+A 108: f210 -> f26 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 81: [34] -> f15 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f26 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f68 : [ L>=A ], cost: 1 62: [43] -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f141 : [ B>=1+A ], cost: 1 47: [52] -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: [52] -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 77: [54] -> f42 : [ B>=1+A ], cost: 1 71: [55] -> f152 : [ B>=1+A ], cost: 1 68: [56] -> f100 : Z'=1, [ B>=1+A ], cost: 1 61: [57] -> f131 : [ B>=1+A ], cost: 1 56: [58] -> f164 : [ B>=1+A ], cost: 1 54: [59] -> f184 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 51: [60] -> f199 : C'=0, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: start 83: f2 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f2 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f15 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f15 -> [35] : B'=1+A, F'=free_4, G'=free_3, H'=H-(-1+B-A)*free_3, [ A>=B && 0>=1+free_4 ], cost: 1-B+A 87: f15 -> [35] : B'=1+A, F'=free_6, G'=free_5, H'=H-free_5*(-1+B-A), [ A>=B && free_6>=1 ], cost: 1-B+A 5: f26 -> f30 : [ 0>=1+Q && 200>=J ], cost: 1 6: f26 -> f30 : [ Q>=1 && 200>=J ], cost: 1 17: f26 -> f87 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 109: f30 -> [54] : B'=1+B, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 110: f30 -> [54] : [], cost: 0 89: f42 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f47 -> f42 : L'=1+L, [ K>=1+A ], cost: 1 11: f47 -> f58 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f58 -> f47 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 112: f87 -> [56] : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 113: f87 -> [56] : [], cost: 0 66: f100 -> f119 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f100 -> f152 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f100 -> f152 : [ B>=1+A && Z>=1 ], cost: 1 21: f100 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 114: f119 -> [57] : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 115: f119 -> [57] : [], cost: 0 97: f131 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f131 -> [45] : B'=1+A, F'=free_14, N'=free_13, O'=O-(-1+B-A)*free_13, [ A>=B && 0>=1+free_14 ], cost: 1-B+A 99: f131 -> [45] : B'=1+A, F'=free_16, N'=free_15, O'=-(-1+B-A)*free_15+O, [ A>=B && free_16>=1 ], cost: 1-B+A 100: f141 -> f147 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f147 -> f152 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 116: f152 -> [58] : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 117: f152 -> [58] : [], cost: 0 118: f164 -> [59] : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K ], cost: 3-K+B 119: f164 -> [59] : [], cost: 0 120: f184 -> [60] : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 121: f184 -> [60] : [], cost: 0 106: f199 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f199 -> [52] : B'=1+A, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1-B+A 108: f210 -> f26 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f26 : J'=1+J, [ B>=1+A && C>=0 ], cost: 1 40: f218 -> f228 : R'=free_25, S'=free_23, T'=free_23, U'=1, V'=free_23, W'=free_24, [ A>=B && free_23>=2 ], cost: 1 41: f218 -> f228 : R'=free_28, S'=free_26, T'=free_26, U'=1, V'=1, W'=free_27, [ A>=B && 1>=free_26 ], cost: 1 42: f228 -> f218 : B'=1+B, [ C>=W ], cost: 1 43: f228 -> f218 : B'=1+B, C'=W, [ W>=1+C ], cost: 1 82: start -> f2 : [], cost: 1 81: [34] -> f15 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f26 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f47 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f47 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f152 : B'=1+A, K'=A, [ L>=A && A>=B && B>=1+K && 1+A>=1+A ], cost: 5-3*B+3*A 62: [43] -> f100 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f100 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f141 : [ B>=1+A ], cost: 1 47: [52] -> f210 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f210 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: [52] -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 77: [54] -> f42 : [ B>=1+A ], cost: 1 68: [56] -> f100 : Z'=1, [ B>=1+A ], cost: 1 61: [57] -> f131 : [ B>=1+A ], cost: 1 56: [58] -> f164 : [ B>=1+A ], cost: 1 54: [59] -> f184 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 51: [60] -> f199 : C'=0, [ B>=1+A ], cost: 1 Applied chaining over branches and pruning: Start location: start 122: start -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 2-B+A 123: start -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 2-B+A Final control flow graph problem, now checking costs for infinitely many models: Start location: start 122: start -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 2-B+A 123: start -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 2-B+A Computing complexity for remaining 2 transitions. Found configuration with infinitely models for cost: 2-B+A and guard: A>=B && C>=free: B: Pos, C: Both, free: Neg, A: Pos, where: A > B Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: A>=B && C>=free Final Cost: 2-B+A Obtained the following complexity w.r.t. the length of the input n: Complexity class: n^1 Complexity value: 1 WORST_CASE(Omega(n^1),?)