Trying to load file: main.koat Initial Control flow graph problem: Start location: start 0: f0 -> f0 : B'=1+B, D'=free, [ A>=B && C>=free ], cost: 1 1: f0 -> f0 : B'=1+B, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1 81: f0 -> f44 : [ B>=1+A && C>=1 ], cost: 1 80: f0 -> f43 : [ B>=1+A && 0>=C ], cost: 1 2: f44 -> f44 : B'=1+B, F'=0, G'=0, [ A>=B ], cost: 1 3: f44 -> f44 : B'=1+B, F'=free_4, G'=free_3, H'=H+free_3, [ A>=B && 0>=1+free_4 ], cost: 1 4: f44 -> f44 : B'=1+B, F'=free_6, G'=free_5, H'=H+free_5, [ A>=B && free_6>=1 ], cost: 1 79: f44 -> f54 : Q'=1, [ B>=1+A ], cost: 1 5: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f99 : Q'=0, [ 200>=J && Q==0 ], cost: 1 78: f54 -> f43 : [ J>=201 ], cost: 1 7: f57 -> f59 : [ A>=B ], cost: 1 77: f57 -> f67 : [ B>=1+A ], cost: 1 76: f59 -> f57 : B'=1+B, [ K>=1+A ], cost: 1 8: f59 -> f59 : K'=1+K, [ A>=K ], cost: 1 14: f67 -> f67 : L'=1+L, M'=0, [ A>=1+L ], cost: 1 9: f67 -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: f67 -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: f67 -> f89 : [ L>=A ], cost: 1 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f74 : H'=0, [ A>=K ], cost: 1 12: f74 -> f74 : B'=1+B, H'=free_9, [ A>=B ], cost: 1 73: f74 -> f80 : H'=free_38, [ B>=1+A ], cost: 1 72: f80 -> f71 : K'=1+K, [ B>=1+A ], cost: 1 13: f80 -> f80 : B'=1+B, [ A>=B ], cost: 1 15: f89 -> f92 : [ A>=B ], cost: 1 71: f89 -> f161 : [ B>=1+A ], cost: 1 70: f92 -> f89 : B'=1+B, [ K>=B ], cost: 1 16: f92 -> f92 : K'=1+K, [ B>=1+K ], cost: 1 18: f99 -> f99 : B'=1+B, [ A>=B ], cost: 1 69: f99 -> f104 : [ B>=1+A ], cost: 1 19: f104 -> f106 : [ A>=B ], cost: 1 68: f104 -> f115 : Z'=1, [ B>=1+A ], cost: 1 67: f106 -> f104 : B'=1+B, [ K>=1+A ], cost: 1 20: f106 -> f106 : H'=free_10, K'=1+K, [ A>=K ], cost: 1 21: f115 -> f117 : [ A>=B ], cost: 1 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 62: f117 -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: f117 -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 22: f117 -> f117 : H'=free_11, K'=1+K, [ A>=K ], cost: 1 23: f132 -> f134 : [ A>=B ], cost: 1 61: f132 -> f142 : [ B>=1+A ], cost: 1 60: f134 -> f132 : B'=1+B, [ K>=1+A ], cost: 1 24: f134 -> f134 : H'=free_12, K'=1+K, [ A>=K ], cost: 1 25: f142 -> f142 : B'=1+B, F'=0, N'=0, [ A>=B ], cost: 1 26: f142 -> f142 : B'=1+B, F'=free_14, N'=free_13, O'=O+free_13, [ A>=B && 0>=1+free_14 ], cost: 1 27: f142 -> f142 : B'=1+B, F'=free_16, N'=free_15, O'=O+free_15, [ A>=B && free_16>=1 ], cost: 1 59: f142 -> f151 : [ B>=1+A ], cost: 1 28: f151 -> f151 : B'=1+B, [ A>=B ], cost: 1 58: f151 -> f156 : [ B>=1+A ], cost: 1 29: f156 -> f156 : B'=1+B, [ A>=B ], cost: 1 57: f156 -> f161 : [ B>=1+A ], cost: 1 30: f161 -> f163 : [ A>=B ], cost: 1 56: f161 -> f171 : [ B>=1+A ], cost: 1 55: f163 -> f161 : B'=1+B, [ K>=1+A ], cost: 1 31: f163 -> f163 : H'=free_17, K'=1+K, [ A>=K ], cost: 1 32: f171 -> f173 : [ B>=1 ], cost: 1 54: f171 -> f181 : [ 0>=B ], cost: 1 53: f173 -> f171 : B'=-1+B, [ K>=1+B ], cost: 1 33: f173 -> f173 : H'=free_18, K'=1+K, [ B>=K ], cost: 1 34: f181 -> f181 : B'=1+B, [ A>=B ], cost: 1 52: f181 -> f188 : Y'=free_31, [ B>=1+A ], cost: 1 35: f188 -> f190 : [ A>=B ], cost: 1 51: f188 -> f201 : C'=0, [ B>=1+A ], cost: 1 50: f190 -> f188 : B'=1+B, [ K>=1+A ], cost: 1 36: f190 -> f190 : H'=free_19, K'=1+K, [ A>=K ], cost: 1 37: f201 -> f201 : B'=1+B, P'=free_20, [ A>=B && C>=free_20 ], cost: 1 38: f201 -> f201 : B'=1+B, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1 47: f201 -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: f201 -> f211 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: f201 -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 46: f211 -> f54 : J'=1+J, [ B>=1+A ], cost: 1 39: f211 -> f211 : B'=1+B, [ A>=B ], cost: 1 44: f218 -> f54 : 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 -> f43 : [ 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 -> f0 : [], cost: 1 Simplified the transitions: Start location: start 0: f0 -> f0 : B'=1+B, D'=free, [ A>=B && C>=free ], cost: 1 1: f0 -> f0 : B'=1+B, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1 81: f0 -> f44 : [ B>=1+A && C>=1 ], cost: 1 2: f44 -> f44 : B'=1+B, F'=0, G'=0, [ A>=B ], cost: 1 3: f44 -> f44 : B'=1+B, F'=free_4, G'=free_3, H'=H+free_3, [ A>=B && 0>=1+free_4 ], cost: 1 4: f44 -> f44 : B'=1+B, F'=free_6, G'=free_5, H'=H+free_5, [ A>=B && free_6>=1 ], cost: 1 79: f44 -> f54 : Q'=1, [ B>=1+A ], cost: 1 5: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f99 : Q'=0, [ 200>=J && Q==0 ], cost: 1 7: f57 -> f59 : [ A>=B ], cost: 1 77: f57 -> f67 : [ B>=1+A ], cost: 1 76: f59 -> f57 : B'=1+B, [ K>=1+A ], cost: 1 8: f59 -> f59 : K'=1+K, [ A>=K ], cost: 1 14: f67 -> f67 : L'=1+L, M'=0, [ A>=1+L ], cost: 1 9: f67 -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: f67 -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: f67 -> f89 : [ L>=A ], cost: 1 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f74 : H'=0, [ A>=K ], cost: 1 12: f74 -> f74 : B'=1+B, H'=free_9, [ A>=B ], cost: 1 73: f74 -> f80 : H'=free_38, [ B>=1+A ], cost: 1 72: f80 -> f71 : K'=1+K, [ B>=1+A ], cost: 1 13: f80 -> f80 : B'=1+B, [ A>=B ], cost: 1 15: f89 -> f92 : [ A>=B ], cost: 1 71: f89 -> f161 : [ B>=1+A ], cost: 1 70: f92 -> f89 : B'=1+B, [ K>=B ], cost: 1 16: f92 -> f92 : K'=1+K, [ B>=1+K ], cost: 1 18: f99 -> f99 : B'=1+B, [ A>=B ], cost: 1 69: f99 -> f104 : [ B>=1+A ], cost: 1 19: f104 -> f106 : [ A>=B ], cost: 1 68: f104 -> f115 : Z'=1, [ B>=1+A ], cost: 1 67: f106 -> f104 : B'=1+B, [ K>=1+A ], cost: 1 20: f106 -> f106 : H'=free_10, K'=1+K, [ A>=K ], cost: 1 21: f115 -> f117 : [ A>=B ], cost: 1 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 62: f117 -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: f117 -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 22: f117 -> f117 : H'=free_11, K'=1+K, [ A>=K ], cost: 1 23: f132 -> f134 : [ A>=B ], cost: 1 61: f132 -> f142 : [ B>=1+A ], cost: 1 60: f134 -> f132 : B'=1+B, [ K>=1+A ], cost: 1 24: f134 -> f134 : H'=free_12, K'=1+K, [ A>=K ], cost: 1 25: f142 -> f142 : B'=1+B, F'=0, N'=0, [ A>=B ], cost: 1 26: f142 -> f142 : B'=1+B, F'=free_14, N'=free_13, O'=O+free_13, [ A>=B && 0>=1+free_14 ], cost: 1 27: f142 -> f142 : B'=1+B, F'=free_16, N'=free_15, O'=O+free_15, [ A>=B && free_16>=1 ], cost: 1 59: f142 -> f151 : [ B>=1+A ], cost: 1 28: f151 -> f151 : B'=1+B, [ A>=B ], cost: 1 58: f151 -> f156 : [ B>=1+A ], cost: 1 29: f156 -> f156 : B'=1+B, [ A>=B ], cost: 1 57: f156 -> f161 : [ B>=1+A ], cost: 1 30: f161 -> f163 : [ A>=B ], cost: 1 56: f161 -> f171 : [ B>=1+A ], cost: 1 55: f163 -> f161 : B'=1+B, [ K>=1+A ], cost: 1 31: f163 -> f163 : H'=free_17, K'=1+K, [ A>=K ], cost: 1 32: f171 -> f173 : [ B>=1 ], cost: 1 54: f171 -> f181 : [ 0>=B ], cost: 1 53: f173 -> f171 : B'=-1+B, [ K>=1+B ], cost: 1 33: f173 -> f173 : H'=free_18, K'=1+K, [ B>=K ], cost: 1 34: f181 -> f181 : B'=1+B, [ A>=B ], cost: 1 52: f181 -> f188 : Y'=free_31, [ B>=1+A ], cost: 1 35: f188 -> f190 : [ A>=B ], cost: 1 51: f188 -> f201 : C'=0, [ B>=1+A ], cost: 1 50: f190 -> f188 : B'=1+B, [ K>=1+A ], cost: 1 36: f190 -> f190 : H'=free_19, K'=1+K, [ A>=K ], cost: 1 37: f201 -> f201 : B'=1+B, P'=free_20, [ A>=B && C>=free_20 ], cost: 1 38: f201 -> f201 : B'=1+B, C'=free_22, P'=free_21, Q_1'=free_22, [ A>=B && free_21>=1+C ], cost: 1 47: f201 -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: f201 -> f211 : X'=free_30, [ B>=1+A && free_30>=1 ], cost: 1 49: f201 -> f218 : C'=0, Q'=0, X'=0, [ B>=1+A ], cost: 1 46: f211 -> f54 : J'=1+J, [ B>=1+A ], cost: 1 39: f211 -> f211 : B'=1+B, [ A>=B ], cost: 1 44: f218 -> f54 : 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 -> f0 : [], cost: 1 Eliminating 2 self-loops for location f0 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 f44 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 f59 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 f67 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 f74 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 f80 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 f92 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 f99 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 f106 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 f117 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 f134 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 f142 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 f151 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 f156 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 f163 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 f173 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 f181 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 f190 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 f201 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 f211 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: f0 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f0 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f44 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f44 -> [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: f44 -> [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: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f99 : Q'=0, [ 200>=J && Q==0 ], cost: 1 7: f57 -> f59 : [ A>=B ], cost: 1 77: f57 -> f67 : [ B>=1+A ], cost: 1 88: f59 -> [36] : K'=1+A, [ A>=K ], cost: 1-K+A 89: f67 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f74 : H'=0, [ A>=K ], cost: 1 90: f74 -> [38] : B'=1+A, H'=free_9, [ A>=B ], cost: 1-B+A 91: f80 -> [39] : B'=1+A, [ A>=B ], cost: 1-B+A 15: f89 -> f92 : [ A>=B ], cost: 1 71: f89 -> f161 : [ B>=1+A ], cost: 1 92: f92 -> [40] : K'=B, [ B>=1+K ], cost: -K+B 93: f99 -> [41] : B'=1+A, [ A>=B ], cost: 1-B+A 19: f104 -> f106 : [ A>=B ], cost: 1 68: f104 -> f115 : Z'=1, [ B>=1+A ], cost: 1 94: f106 -> [42] : H'=free_10, K'=1+A, [ A>=K ], cost: 1-K+A 21: f115 -> f117 : [ A>=B ], cost: 1 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 95: f117 -> [43] : H'=free_11, K'=1+A, [ A>=K ], cost: 1-K+A 23: f132 -> f134 : [ A>=B ], cost: 1 61: f132 -> f142 : [ B>=1+A ], cost: 1 96: f134 -> [44] : H'=free_12, K'=1+A, [ A>=K ], cost: 1-K+A 97: f142 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f142 -> [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: f142 -> [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: f151 -> [46] : B'=1+A, [ A>=B ], cost: 1-B+A 101: f156 -> [47] : B'=1+A, [ A>=B ], cost: 1-B+A 30: f161 -> f163 : [ A>=B ], cost: 1 56: f161 -> f171 : [ B>=1+A ], cost: 1 102: f163 -> [48] : H'=free_17, K'=1+A, [ A>=K ], cost: 1-K+A 32: f171 -> f173 : [ B>=1 ], cost: 1 54: f171 -> f181 : [ 0>=B ], cost: 1 103: f173 -> [49] : H'=free_18, K'=1+B, [ B>=K ], cost: 1-K+B 104: f181 -> [50] : B'=1+A, [ A>=B ], cost: 1-B+A 35: f188 -> f190 : [ A>=B ], cost: 1 51: f188 -> f201 : C'=0, [ B>=1+A ], cost: 1 105: f190 -> [51] : H'=free_19, K'=1+A, [ A>=K ], cost: 1-K+A 106: f201 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f201 -> [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: f211 -> [53] : B'=1+A, [ A>=B ], cost: 1-B+A 44: f218 -> f54 : 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 -> f0 : [], cost: 1 81: [34] -> f44 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f54 : Q'=1, [ B>=1+A ], cost: 1 76: [36] -> f57 : B'=1+B, [ K>=1+A ], cost: 1 9: [37] -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f89 : [ L>=A ], cost: 1 73: [38] -> f80 : H'=free_38, [ B>=1+A ], cost: 1 72: [39] -> f71 : K'=1+K, [ B>=1+A ], cost: 1 70: [40] -> f89 : B'=1+B, [ K>=B ], cost: 1 69: [41] -> f104 : [ B>=1+A ], cost: 1 67: [42] -> f104 : B'=1+B, [ K>=1+A ], cost: 1 62: [43] -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 60: [44] -> f132 : B'=1+B, [ K>=1+A ], cost: 1 59: [45] -> f151 : [ B>=1+A ], cost: 1 58: [46] -> f156 : [ B>=1+A ], cost: 1 57: [47] -> f161 : [ B>=1+A ], cost: 1 55: [48] -> f161 : B'=1+B, [ K>=1+A ], cost: 1 53: [49] -> f171 : B'=-1+B, [ K>=1+B ], cost: 1 52: [50] -> f188 : Y'=free_31, [ B>=1+A ], cost: 1 50: [51] -> f188 : B'=1+B, [ K>=1+A ], cost: 1 47: [52] -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f211 : 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] -> f54 : J'=1+J, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: start 83: f0 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f0 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f44 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f44 -> [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: f44 -> [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: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f104 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 7: f57 -> f57 : B'=1+B, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 77: f57 -> f67 : [ B>=1+A ], cost: 1 89: f67 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f80 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f80 -> f71 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 15: f89 -> f89 : B'=1+B, K'=B, [ A>=B && B>=1+K && B>=B ], cost: 2-K+B 71: f89 -> f161 : [ B>=1+A ], cost: 1 19: f104 -> f104 : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 68: f104 -> f115 : Z'=1, [ B>=1+A ], cost: 1 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 21: f115 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 23: f132 -> f132 : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 61: f132 -> f142 : [ B>=1+A ], cost: 1 97: f142 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f142 -> [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: f142 -> [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: f151 -> f156 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f156 -> f161 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 30: f161 -> f161 : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 56: f161 -> f171 : [ B>=1+A ], cost: 1 32: f171 -> f171 : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K && 1+B>=1+B ], cost: 3-K+B 54: f171 -> f188 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 35: f188 -> f188 : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K && 1+A>=1+A ], cost: 3-K+A 51: f188 -> f201 : C'=0, [ B>=1+A ], cost: 1 106: f201 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f201 -> [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: f211 -> f54 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f54 : 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 -> f0 : [], cost: 1 81: [34] -> f44 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f54 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f89 : [ L>=A ], cost: 1 62: [43] -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f151 : [ B>=1+A ], cost: 1 47: [52] -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f211 : 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 f57 Removing the self-loops: 7. Adding an epsilon transition (to model nonexecution of the loops): 110. Eliminating 1 self-loops for location f89 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 f104 Removing the self-loops: 19. Adding an epsilon transition (to model nonexecution of the loops): 113. Eliminating 1 self-loops for location f132 Removing the self-loops: 23. Adding an epsilon transition (to model nonexecution of the loops): 115. Eliminating 1 self-loops for location f161 Removing the self-loops: 30. Adding an epsilon transition (to model nonexecution of the loops): 117. Eliminating 1 self-loops for location f171 Removing the self-loops: 32. Adding an epsilon transition (to model nonexecution of the loops): 119. Eliminating 1 self-loops for location f188 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: f0 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f0 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f44 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f44 -> [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: f44 -> [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: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f104 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 109: f57 -> [54] : B'=1+B, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 110: f57 -> [54] : [], cost: 0 89: f67 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f80 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f80 -> f71 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 111: f89 -> [55] : B'=1+A, K'=A, [ A>=B && B>=1+K ], cost: 3-3*B+3*A 112: f104 -> [56] : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 113: f104 -> [56] : [], cost: 0 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 21: f115 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 114: f132 -> [57] : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 115: f132 -> [57] : [], cost: 0 97: f142 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f142 -> [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: f142 -> [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: f151 -> f156 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f156 -> f161 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 116: f161 -> [58] : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 117: f161 -> [58] : [], cost: 0 118: f171 -> [59] : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K ], cost: 3-K+B 119: f171 -> [59] : [], cost: 0 120: f188 -> [60] : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 121: f188 -> [60] : [], cost: 0 106: f201 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f201 -> [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: f211 -> f54 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f54 : 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 -> f0 : [], cost: 1 81: [34] -> f44 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f54 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f89 : [ L>=A ], cost: 1 62: [43] -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f151 : [ B>=1+A ], cost: 1 47: [52] -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f211 : 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] -> f67 : [ B>=1+A ], cost: 1 71: [55] -> f161 : [ B>=1+A ], cost: 1 68: [56] -> f115 : Z'=1, [ B>=1+A ], cost: 1 61: [57] -> f142 : [ B>=1+A ], cost: 1 56: [58] -> f171 : [ B>=1+A ], cost: 1 54: [59] -> f188 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 51: [60] -> f201 : C'=0, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: start 83: f0 -> [34] : B'=1+A, D'=free, [ A>=B && C>=free ], cost: 1-B+A 84: f0 -> [34] : B'=1+A, C'=free_1, D'=free_2, E'=free_1, [ A>=B && free_2>=1+C ], cost: 1-B+A 85: f44 -> [35] : B'=1+A, F'=0, G'=0, [ A>=B ], cost: 1-B+A 86: f44 -> [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: f44 -> [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: f54 -> f57 : [ 0>=1+Q && 200>=J ], cost: 1 6: f54 -> f57 : [ Q>=1 && 200>=J ], cost: 1 17: f54 -> f104 : B'=1+A, Q'=0, [ 200>=J && Q==0 && A>=B && 1+A>=1+A ], cost: 3-B+A 109: f57 -> [54] : B'=1+B, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 110: f57 -> [54] : [], cost: 0 89: f67 -> [37] : L'=A, M'=0, [ A>=1+L ], cost: -L+A 74: f71 -> f67 : L'=1+L, [ K>=1+A ], cost: 1 11: f71 -> f80 : B'=1+A, H'=free_38, [ A>=K && A>=B && 1+A>=1+A ], cost: 3-B+A 91: f80 -> f71 : B'=1+A, K'=1+K, [ A>=B && 1+A>=1+A ], cost: 2-B+A 112: f104 -> [56] : B'=1+B, H'=free_10, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 113: f104 -> [56] : [], cost: 0 66: f115 -> f132 : Z'=0, [ B>=1+A && Z==0 ], cost: 1 64: f115 -> f161 : [ B>=1+A && 0>=1+Z ], cost: 1 65: f115 -> f161 : [ B>=1+A && Z>=1 ], cost: 1 21: f115 -> [43] : H'=free_11, K'=1+A, [ A>=B && A>=K ], cost: 2-K+A 114: f132 -> [57] : B'=1+B, H'=free_12, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 115: f132 -> [57] : [], cost: 0 97: f142 -> [45] : B'=1+A, F'=0, N'=0, [ A>=B ], cost: 1-B+A 98: f142 -> [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: f142 -> [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: f151 -> f156 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 101: f156 -> f161 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 2-B+A 116: f161 -> [58] : B'=1+B, H'=free_17, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 117: f161 -> [58] : [], cost: 0 118: f171 -> [59] : B'=-1+B, H'=free_18, K'=1+B, [ B>=1 && B>=K ], cost: 3-K+B 119: f171 -> [59] : [], cost: 0 120: f188 -> [60] : B'=1+B, H'=free_19, K'=1+A, [ A>=B && A>=K ], cost: 3-K+A 121: f188 -> [60] : [], cost: 0 106: f201 -> [52] : B'=1+A, P'=free_20, [ A>=B && C>=free_20 ], cost: 1-B+A 107: f201 -> [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: f211 -> f54 : B'=1+A, J'=1+J, [ A>=B && 1+A>=1+A ], cost: 2-B+A 44: f218 -> f54 : 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 -> f0 : [], cost: 1 81: [34] -> f44 : [ B>=1+A && C>=1 ], cost: 1 79: [35] -> f54 : Q'=1, [ B>=1+A ], cost: 1 9: [37] -> f71 : M'=free_7, [ A>=1+L && 0>=1+free_7 ], cost: 1 10: [37] -> f71 : M'=free_8, [ A>=1+L && free_8>=1 ], cost: 1 75: [37] -> f161 : B'=1+A, K'=A, [ L>=A && A>=B && B>=1+K && 1+A>=1+A ], cost: 5-3*B+3*A 62: [43] -> f115 : B'=1+B, Z'=0, A1'=free_34, B1'=free_32, C1'=free_33, [ K>=1+A && free_34>=0 ], cost: 1 63: [43] -> f115 : B'=1+B, A1'=free_37, B1'=free_35, C1'=free_36, [ K>=1+A && 0>=1+free_37 ], cost: 1 59: [45] -> f151 : [ B>=1+A ], cost: 1 47: [52] -> f211 : X'=free_29, [ B>=1+A && 0>=1+free_29 ], cost: 1 48: [52] -> f211 : 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] -> f67 : [ B>=1+A ], cost: 1 68: [56] -> f115 : Z'=1, [ B>=1+A ], cost: 1 61: [57] -> f142 : [ B>=1+A ], cost: 1 56: [58] -> f171 : [ B>=1+A ], cost: 1 54: [59] -> f188 : B'=1+A, Y'=free_31, [ 0>=B && A>=B && 1+A>=1+A ], cost: 3-B+A 51: [60] -> f201 : 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),?)