Trying to load file: main.koat Initial Control flow graph problem: Start location: f2 0: f2 -> f13 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1 1: f13 -> f13 : J'=1+J, K'=1, L'=0, M'=0, [ C>=J ], cost: 1 2: f13 -> f13 : A'=free_1+A, J'=1+J, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1 3: f13 -> f13 : A'=free_3+A, J'=1+J, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1 46: f13 -> f24 : [ J>=1+C ], cost: 1 4: f24 -> f24 : J'=1+J, [ D>=J ], cost: 1 43: f24 -> f31 : [ 0>=1+P && J>=1+D ], cost: 1 44: f24 -> f31 : [ P>=1 && J>=1+D ], cost: 1 45: f24 -> f37 : P'=0, [ J>=1+D && P==0 ], cost: 1 5: f31 -> f31 : J'=1+J, [ D>=J ], cost: 1 42: f31 -> f37 : [ J>=1+D ], cost: 1 6: f37 -> f40 : [ N>=O ], cost: 1 41: f37 -> f118 : B'=free_34, [ O>=1+N ], cost: 1 7: f40 -> f44 : [ 0>=1+P && 0>=Q_1 ], cost: 1 8: f40 -> f44 : [ P>=1 && 0>=Q_1 ], cost: 1 12: f40 -> f64 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1 40: f40 -> f71 : [ Q_1>=1 ], cost: 1 9: f44 -> f44 : J'=1+J, [ D>=J ], cost: 1 39: f44 -> f50 : [ J>=1+D ], cost: 1 10: f50 -> f50 : J'=1+J, [ D>=J ], cost: 1 38: f50 -> f57 : A1'=Q_1+C, [ J>=1+D ], cost: 1 37: f57 -> f40 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1 11: f57 -> f57 : J'=1+J, [ D>=J ], cost: 1 36: f64 -> f40 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1 13: f64 -> f64 : J'=2+J, [ E>=J ], cost: 1 14: f71 -> f71 : J'=1+J, R'=2*J, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1 33: f71 -> f86 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1 34: f71 -> f86 : L'=free_28, Z'=free_29, [ 0>=1+free_30 && J>=1+C ], cost: 1 35: f71 -> f86 : L'=free_31, Z'=free_32, [ free_33>=1 && J>=1+C ], cost: 1 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1 19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ 0>=1+free_11 && D>=J ], cost: 1 20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ free_14>=1 && D>=J ], cost: 1 21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1 22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1 23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1 24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1 25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1 26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1 27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1 28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1 29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1 30: f118 -> f118 : J'=1+J, [ D>=J ], cost: 1 31: f118 -> f1 : [ J>=1+D ], cost: 1 Simplified the transitions: Start location: f2 0: f2 -> f13 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1 1: f13 -> f13 : J'=1+J, K'=1, L'=0, M'=0, [ C>=J ], cost: 1 2: f13 -> f13 : A'=free_1+A, J'=1+J, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1 3: f13 -> f13 : A'=free_3+A, J'=1+J, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1 46: f13 -> f24 : [ J>=1+C ], cost: 1 4: f24 -> f24 : J'=1+J, [ D>=J ], cost: 1 43: f24 -> f31 : [ 0>=1+P && J>=1+D ], cost: 1 44: f24 -> f31 : [ P>=1 && J>=1+D ], cost: 1 45: f24 -> f37 : P'=0, [ J>=1+D && P==0 ], cost: 1 5: f31 -> f31 : J'=1+J, [ D>=J ], cost: 1 42: f31 -> f37 : [ J>=1+D ], cost: 1 6: f37 -> f40 : [ N>=O ], cost: 1 41: f37 -> f118 : B'=free_34, [ O>=1+N ], cost: 1 7: f40 -> f44 : [ 0>=1+P && 0>=Q_1 ], cost: 1 8: f40 -> f44 : [ P>=1 && 0>=Q_1 ], cost: 1 12: f40 -> f64 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1 40: f40 -> f71 : [ Q_1>=1 ], cost: 1 9: f44 -> f44 : J'=1+J, [ D>=J ], cost: 1 39: f44 -> f50 : [ J>=1+D ], cost: 1 10: f50 -> f50 : J'=1+J, [ D>=J ], cost: 1 38: f50 -> f57 : A1'=Q_1+C, [ J>=1+D ], cost: 1 37: f57 -> f40 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1 11: f57 -> f57 : J'=1+J, [ D>=J ], cost: 1 36: f64 -> f40 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1 13: f64 -> f64 : J'=2+J, [ E>=J ], cost: 1 14: f71 -> f71 : J'=1+J, R'=2*J, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1 33: f71 -> f86 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1 34: f71 -> f86 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1 35: f71 -> f86 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1 19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1 20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1 21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1 22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1 23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1 24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1 25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1 26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1 27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1 28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1 29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1 30: f118 -> f118 : J'=1+J, [ D>=J ], cost: 1 Eliminating 3 self-loops for location f13 Self-Loop 1 has the metering function: 1+C-J, resulting in the new transition 47. Self-Loop 2 has the metering function: 1+C-J, resulting in the new transition 48. Self-Loop 3 has the metering function: 1+C-J, resulting in the new transition 49. Removing the self-loops: 1 2 3. Eliminating 1 self-loops for location f24 Self-Loop 4 has the metering function: 1-J+D, resulting in the new transition 50. Removing the self-loops: 4. Eliminating 1 self-loops for location f31 Self-Loop 5 has the metering function: 1-J+D, resulting in the new transition 51. Removing the self-loops: 5. Eliminating 1 self-loops for location f44 Self-Loop 9 has the metering function: 1-J+D, resulting in the new transition 52. Removing the self-loops: 9. Eliminating 1 self-loops for location f50 Self-Loop 10 has the metering function: 1-J+D, resulting in the new transition 53. Removing the self-loops: 10. Eliminating 1 self-loops for location f57 Self-Loop 11 has the metering function: 1-J+D, resulting in the new transition 54. Removing the self-loops: 11. Eliminating 1 self-loops for location f64 Self-Loop 13 has the metering function: meter, resulting in the new transition 55. Removing the self-loops: 13. Eliminating 1 self-loops for location f71 Self-Loop 14 has the metering function: 1+C-J, resulting in the new transition 56. Removing the self-loops: 14. Eliminating 1 self-loops for location f118 Self-Loop 30 has the metering function: 1-J+D, resulting in the new transition 57. Removing the self-loops: 30. Removed all Self-loops using metering functions (where possible): Start location: f2 0: f2 -> f13 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1 47: f13 -> [18] : J'=1+C, K'=1, L'=0, M'=0, [ C>=J ], cost: 1+C-J 48: f13 -> [18] : A'=free_1*(1+C-J)+A, J'=1+C, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1+C-J 49: f13 -> [18] : A'=free_3*(1+C-J)+A, J'=1+C, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1+C-J 50: f24 -> [19] : J'=1+D, [ D>=J ], cost: 1-J+D 51: f31 -> [20] : J'=1+D, [ D>=J ], cost: 1-J+D 6: f37 -> f40 : [ N>=O ], cost: 1 41: f37 -> f118 : B'=free_34, [ O>=1+N ], cost: 1 7: f40 -> f44 : [ 0>=1+P && 0>=Q_1 ], cost: 1 8: f40 -> f44 : [ P>=1 && 0>=Q_1 ], cost: 1 12: f40 -> f64 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1 40: f40 -> f71 : [ Q_1>=1 ], cost: 1 52: f44 -> [21] : J'=1+D, [ D>=J ], cost: 1-J+D 53: f50 -> [22] : J'=1+D, [ D>=J ], cost: 1-J+D 54: f57 -> [23] : J'=1+D, [ D>=J ], cost: 1-J+D 55: f64 -> [24] : J'=J+2*meter, [ E>=J && 2*meter==E-J ], cost: meter 56: f71 -> [25] : J'=1+C, R'=2*C, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1+C-J 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1 19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1 20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1 21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1 22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1 23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1 24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1 25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1 26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1 27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1 28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1 29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1 57: f118 -> [26] : J'=1+D, [ D>=J ], cost: 1-J+D 46: [18] -> f24 : [ J>=1+C ], cost: 1 43: [19] -> f31 : [ 0>=1+P && J>=1+D ], cost: 1 44: [19] -> f31 : [ P>=1 && J>=1+D ], cost: 1 45: [19] -> f37 : P'=0, [ J>=1+D && P==0 ], cost: 1 42: [20] -> f37 : [ J>=1+D ], cost: 1 39: [21] -> f50 : [ J>=1+D ], cost: 1 38: [22] -> f57 : A1'=Q_1+C, [ J>=1+D ], cost: 1 37: [23] -> f40 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1 36: [24] -> f40 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1 33: [25] -> f86 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1 34: [25] -> f86 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1 35: [25] -> f86 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1 Applied simple chaining: Start location: f2 0: f2 -> f13 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1 47: f13 -> [18] : J'=1+C, K'=1, L'=0, M'=0, [ C>=J ], cost: 1+C-J 48: f13 -> [18] : A'=free_1*(1+C-J)+A, J'=1+C, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1+C-J 49: f13 -> [18] : A'=free_3*(1+C-J)+A, J'=1+C, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1+C-J 51: f31 -> f37 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D 6: f37 -> f40 : [ N>=O ], cost: 1 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 7: f40 -> f44 : [ 0>=1+P && 0>=Q_1 ], cost: 1 8: f40 -> f44 : [ P>=1 && 0>=Q_1 ], cost: 1 12: f40 -> [24] : J'=J+2*meter, P'=0, [ 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 1+meter 40: f40 -> [25] : J'=1+C, R'=2*C, S'=free_5, T'=1-free_5, [ Q_1>=1 && C>=J ], cost: 2+C-J 52: f44 -> f50 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D 53: f50 -> f57 : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D 54: f57 -> f40 : J'=1+D, Q_1'=1+Q_1, [ D>=J && 1+D>=1+D ], cost: 2-J+D 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1 19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1 20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1 21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1 22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1 23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1 24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1 25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1 26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1 27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1 28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1 29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1 46: [18] -> [19] : J'=1+D, [ J>=1+C && D>=J ], cost: 2-J+D 43: [19] -> f31 : [ 0>=1+P && J>=1+D ], cost: 1 44: [19] -> f31 : [ P>=1 && J>=1+D ], cost: 1 45: [19] -> f37 : P'=0, [ J>=1+D && P==0 ], cost: 1 36: [24] -> f40 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1 33: [25] -> f86 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1 34: [25] -> f86 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1 35: [25] -> f86 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1 Applied chaining over branches and pruning: Start location: f2 58: f2 -> [18] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=1, L'=0, M'=0, [ 2*D>=J ], cost: 2-J+2*D 59: f2 -> [18] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J ], cost: 2-J+2*D 60: f2 -> [18] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J ], cost: 2-J+2*D 51: f31 -> f37 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D 6: f37 -> f40 : [ N>=O ], cost: 1 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 64: f40 -> f50 : J'=1+D, [ 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 3-J+D 65: f40 -> f50 : J'=1+D, [ P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 3-J+D 67: f40 -> f86 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J 68: f40 -> f86 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J 69: f40 -> f86 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J 66: f40 -> [27] : J'=J+2*meter, P'=0, [ 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 1+meter 70: f50 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 71: f91 -> f103 : L'=free_15, R'=2*J, V'=0, W'=0, [ D>=J && free_8==0 ], cost: 2 72: f91 -> f103 : L'=free_16, R'=2*J, V'=0, W'=free_17, [ D>=J && 0>=1+free_8 ], cost: 2 74: f91 -> f103 : L'=free_15, R'=2*J, V'=free_10, W'=0, [ D>=J && free_9==0 ], cost: 2 75: f91 -> f103 : L'=free_16, R'=2*J, V'=free_10, W'=free_17, [ D>=J && 0>=1+free_9 ], cost: 2 77: f91 -> f103 : L'=free_15, R'=2*J, V'=free_13, W'=0, [ D>=J && free_12==0 ], cost: 2 80: f103 -> f91 : J'=1+J, L'=0, X'=0, Y'=0, [ L==0 && free_20==0 ], cost: 2 81: f103 -> f91 : J'=1+J, L'=free_20, X'=0, Y'=free_25, [ L==0 && 0>=1+free_20 ], cost: 2 83: f103 -> f91 : J'=1+J, L'=0, X'=free_22, Y'=0, [ 0>=1+L && free_21==0 ], cost: 2 84: f103 -> f91 : J'=1+J, L'=free_21, X'=free_22, Y'=free_25, [ 0>=1+L && 0>=1+free_21 ], cost: 2 86: f103 -> f91 : J'=1+J, L'=0, X'=free_24, Y'=0, [ L>=1 && free_23==0 ], cost: 2 61: [18] -> f31 : J'=1+D, [ J>=1+C && D>=J && 0>=1+P && 1+D>=1+D ], cost: 3-J+D 62: [18] -> f31 : J'=1+D, [ J>=1+C && D>=J && P>=1 && 1+D>=1+D ], cost: 3-J+D 63: [18] -> f37 : J'=1+D, P'=0, [ J>=1+C && D>=J && 1+D>=1+D && P==0 ], cost: 3-J+D Applied chaining over branches and pruning: Start location: f2 89: f2 -> f31 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 92: f2 -> f31 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 93: f2 -> f31 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 95: f2 -> f31 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 96: f2 -> f31 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 91: f2 -> f37 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 94: f2 -> f37 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 97: f2 -> f37 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 51: f31 -> f37 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D 98: f37 -> f50 : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 99: f37 -> f50 : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 100: f37 -> f86 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 101: f37 -> f86 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 102: f37 -> f86 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: f37 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 70: f50 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 32: f91 -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 104: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=0, W'=0, X'=0, Y'=0, [ D>=J && free_8==0 && free_15==0 && free_20==0 ], cost: 4 105: f91 -> f91 : J'=1+J, L'=free_20, R'=2*J, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && free_8==0 && free_15==0 && 0>=1+free_20 ], cost: 4 107: f91 -> f91 : J'=1+J, L'=free_21, R'=2*J, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && free_8==0 && 0>=1+free_15 && 0>=1+free_21 ], cost: 4 111: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J && 0>=1+free_8 && 0>=1+free_16 && free_21==0 ], cost: 4 116: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J && free_9==0 && 0>=1+free_15 && free_21==0 ], cost: 4 Eliminating 5 self-loops for location f91 Self-Loop 104 has the metering function: 1-J+D, resulting in the new transition 129. Self-Loop 105 has the metering function: 1-J+D, resulting in the new transition 130. Self-Loop 107 has the metering function: 1-J+D, resulting in the new transition 131. Self-Loop 111 has the metering function: 1-J+D, resulting in the new transition 132. Self-Loop 116 has the metering function: 1-J+D, resulting in the new transition 133. Removing the self-loops: 104 105 107 111 116. Removed all Self-loops using metering functions (where possible): Start location: f2 89: f2 -> f31 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 92: f2 -> f31 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 93: f2 -> f31 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 95: f2 -> f31 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 96: f2 -> f31 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 91: f2 -> f37 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 94: f2 -> f37 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 97: f2 -> f37 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 51: f31 -> f37 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D 98: f37 -> f50 : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 99: f37 -> f50 : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 100: f37 -> f86 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 101: f37 -> f86 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 102: f37 -> f86 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: f37 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 70: f50 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D 15: f86 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1 16: f86 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1 17: f86 -> f91 : U'=free_7, [ L>=1 ], cost: 1 129: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=0, W'=0, X'=0, Y'=0, [ D>=J ], cost: 4-4*J+4*D 130: f91 -> [29] : J'=1+D, L'=free_20, R'=2*D, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && 0>=1+free_20 ], cost: 4-4*J+4*D 131: f91 -> [29] : J'=1+D, L'=free_21, R'=2*D, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && 0>=1+free_21 ], cost: 4-4*J+4*D 132: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J ], cost: 4-4*J+4*D 133: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J ], cost: 4-4*J+4*D 32: [29] -> f37 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1 Applied chaining over branches and pruning: Start location: f2 91: f2 -> f37 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 94: f2 -> f37 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 97: f2 -> f37 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 141: f37 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_27==0 ], cost: 5+C-J 142: f37 -> f91 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, U'=free_6, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 ], cost: 5+C-J 144: f37 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_28==0 ], cost: 5+C-J 145: f37 -> f91 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, U'=free_6, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_28 ], cost: 5+C-J 147: f37 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_31==0 ], cost: 5+C-J 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: f37 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 139: f37 -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 140: f37 -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 150: f91 -> f37 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=0, W'=0, X'=0, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D 151: f91 -> f37 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && 0>=1+free_20 && 1+D>=1+D ], cost: 5-4*J+4*D 152: f91 -> f37 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && 0>=1+free_21 && 1+D>=1+D ], cost: 5-4*J+4*D 153: f91 -> f37 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D 154: f91 -> f37 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D Applied chaining over branches and pruning: Start location: f2 91: f2 -> f37 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 94: f2 -> f37 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 97: f2 -> f37 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 156: f37 -> f37 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_27==0 && D>=1+C && 0>=1+free_20 && 1+D>=1+D ], cost: 6-3*C-J+4*D 161: f37 -> f37 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 && D>=1+C && 0>=1+free_20 && 1+D>=1+D ], cost: 6-3*C-J+4*D 162: f37 -> f37 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D 167: f37 -> f37 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_28==0 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D 177: f37 -> f37 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_31==0 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D 41: f37 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: f37 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 139: f37 -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 140: f37 -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D Eliminating 5 self-loops for location f37 Removing the self-loops: 156 161 162 167 177. Adding an epsilon transition (to model nonexecution of the loops): 185. Removed all Self-loops using metering functions (where possible): Start location: f2 91: f2 -> f37 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 94: f2 -> f37 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 97: f2 -> f37 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 180: f37 -> [37] : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_20 ], cost: 6-3*C-J+4*D 181: f37 -> [37] : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_20 ], cost: 6-3*C-J+4*D 182: f37 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D 183: f37 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D 184: f37 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D 185: f37 -> [37] : [], cost: 0 41: [37] -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: [37] -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 139: [37] -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 140: [37] -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D Applied chaining over branches and pruning: Start location: f2 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 191: f2 -> [37] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 197: f2 -> [37] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 203: f2 -> [37] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 186: f2 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 187: f2 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 188: f2 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 189: f2 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 190: f2 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 192: f2 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 193: f2 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 194: f2 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 195: f2 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 196: f2 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 198: f2 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 199: f2 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 200: f2 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 201: f2 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 202: f2 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 41: [37] -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D 103: [37] -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter 139: [37] -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D 140: [37] -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D Applied chaining over branches and pruning: Start location: f2 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 186: f2 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 187: f2 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 188: f2 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 189: f2 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 190: f2 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 192: f2 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 193: f2 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 194: f2 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 195: f2 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 196: f2 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 198: f2 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 199: f2 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 200: f2 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 201: f2 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 202: f2 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 204: f2 -> [53] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 205: f2 -> [54] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 206: f2 -> [55] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 207: f2 -> [56] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 208: f2 -> [57] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 209: f2 -> [58] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 210: f2 -> [59] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 211: f2 -> [60] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 212: f2 -> [61] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 213: f2 -> [62] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 214: f2 -> [63] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 215: f2 -> [64] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D Final control flow graph problem, now checking costs for infinitely many models: Start location: f2 134: f2 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 135: f2 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 136: f2 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 137: f2 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D 138: f2 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D 186: f2 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 187: f2 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 188: f2 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 189: f2 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 190: f2 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 192: f2 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 193: f2 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 194: f2 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 195: f2 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 196: f2 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 198: f2 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 199: f2 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 200: f2 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 201: f2 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 202: f2 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 204: f2 -> [53] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 205: f2 -> [54] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 206: f2 -> [55] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 207: f2 -> [56] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 208: f2 -> [57] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 209: f2 -> [58] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 210: f2 -> [59] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 211: f2 -> [60] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 212: f2 -> [61] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 213: f2 -> [62] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 214: f2 -> [63] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D 215: f2 -> [64] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D Computing complexity for remaining 32 transitions. Found configuration with infinitely models for cost: 4-J+D and guard: 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D: P: Neg, J: Neg, D: Neg, where: J > D Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D Final Cost: 4-J+D 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),?)