Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f274 -> f283 : [ A>=1+B ], cost: 1 1: f274 -> f283 : [ B>=1+A ], cost: 1 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f277 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f283 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ 29>=R ], cost: 1 58: f283 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ R>=31 ], cost: 1 59: f283 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ R==30 ], cost: 1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 3: f41 -> f49 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f41 -> f156 : [ G>=1+F ], cost: 1 4: f49 -> f49 : A'=1+A, D'=free+D, J'=free, [ H>=A ], cost: 1 108: f49 -> f56 : [ 0>=1+D && A>=1+H ], cost: 1 109: f49 -> f56 : [ D>=1 && A>=1+H ], cost: 1 110: f49 -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 5: f56 -> f56 : A'=1+A, Q'=free_1, [ H>=A ], cost: 1 106: f56 -> f73 : E'=-free_99, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ free_101>=0 && A>=1+H ], cost: 1 107: f56 -> f73 : E'=free_103, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ 0>=1+free_105 && A>=1+H ], cost: 1 6: f73 -> f75 : [ F>=K ], cost: 1 105: f73 -> f88 : [ K>=1+F ], cost: 1 7: f75 -> f75 : A'=1+A, Q'=free_2, [ H>=A ], cost: 1 104: f75 -> f81 : X'=free_98, [ A>=1+H ], cost: 1 103: f81 -> f73 : K'=1+K, [ A>=1+H ], cost: 1 8: f81 -> f81 : A'=1+A, [ H>=A ], cost: 1 9: f88 -> f88 : A'=1+A, [ H>=A ], cost: 1 102: f88 -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 11: f97 -> f99 : [ F>=1+G && H>=G ], cost: 1 12: f97 -> f99 : [ G>=1+F && H>=G ], cost: 1 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 13: f99 -> f99 : A'=1+A, D'=free_3+D, L'=free_3, [ F>=A ], cost: 1 99: f99 -> f106 : [ 0>=1+D && A>=1+F ], cost: 1 100: f99 -> f106 : [ D>=1 && A>=1+F ], cost: 1 101: f99 -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 14: f106 -> f106 : A'=1+A, Q'=free_4, [ F>=A ], cost: 1 97: f106 -> f123 : E'=-free_88, X'=free_90, Y'=free_89, H1'=free_91, Q1'=free_88, J1'=free_88, [ free_90>=0 && A>=1+F ], cost: 1 98: f106 -> f123 : E'=free_92, X'=free_94, Y'=free_93, J1'=-free_92, K1'=free_95, L1'=free_92, [ 0>=1+free_94 && A>=1+F ], cost: 1 15: f123 -> f123 : A'=1+A, [ F>=A ], cost: 1 96: f123 -> f128 : [ A>=1+F ], cost: 1 16: f128 -> f130 : [ H>=K ], cost: 1 95: f128 -> f142 : [ K>=1+H ], cost: 1 17: f130 -> f130 : A'=1+A, Q'=free_5, [ F>=A ], cost: 1 94: f130 -> f135 : [ A>=1+F ], cost: 1 93: f135 -> f128 : K'=1+K, [ A>=1+F ], cost: 1 18: f135 -> f135 : A'=1+A, [ F>=A ], cost: 1 19: f142 -> f142 : A'=1+A, [ F>=A ], cost: 1 92: f142 -> f151 : M'=C, N'=free_86, O'=free_87, P'=free_87+free_86, [ A>=1+F ], cost: 1 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 32: f156 -> f156 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F ], cost: 1 24: f156 -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: f156 -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: f156 -> f191 : [ 0>=G ], cost: 1 26: f160 -> f160 : K'=1+K, [ F>=K ], cost: 1 90: f160 -> f165 : [ K>=1+F ], cost: 1 27: f165 -> f167 : [ F>=K ], cost: 1 89: f165 -> f179 : [ K>=1+F ], cost: 1 28: f167 -> f167 : A'=1+A, Q'=free_10, [ F>=A ], cost: 1 88: f167 -> f172 : [ A>=1+F ], cost: 1 87: f172 -> f165 : K'=1+K, [ A>=1+F ], cost: 1 29: f172 -> f172 : A'=1+A, [ F>=A ], cost: 1 86: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, [ K>=1+F ], cost: 1 31: f179 -> f179 : K'=1+K, Q_1'=0, [ F>=K ], cost: 1 33: f191 -> f195 : B'=1+G, E'=free_12, [ G>=1 ], cost: 1 85: f191 -> f230 : [ 0>=G ], cost: 1 34: f195 -> f195 : K'=1+K, [ F>=K ], cost: 1 82: f195 -> f202 : E'=free_83, [ K>=1+F && 0>=1+E ], cost: 1 83: f195 -> f202 : E'=free_84, [ K>=1+F && E>=1 ], cost: 1 84: f195 -> f223 : E'=0, [ K>=1+F && E==0 ], cost: 1 35: f202 -> f204 : [ F>=K ], cost: 1 81: f202 -> f217 : [ K>=1+F ], cost: 1 36: f204 -> f204 : A'=1+A, Q'=free_13, [ H>=A ], cost: 1 80: f204 -> f210 : X'=free_82, [ A>=1+H ], cost: 1 79: f210 -> f202 : K'=1+K, [ A>=1+H ], cost: 1 37: f210 -> f210 : A'=1+A, [ H>=A ], cost: 1 78: f217 -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 38: f217 -> f217 : K'=1+K, [ H>=K ], cost: 1 77: f223 -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 39: f223 -> f223 : K'=1+K, [ H>=K ], cost: 1 40: f230 -> f232 : [ A>=1 ], cost: 1 76: f230 -> f350 : [ 0>=A ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 42: f235 -> f247 : [ 0>=B ], cost: 1 43: f235 -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 44: f235 -> f243 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 1 45: f235 -> f243 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 1 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f243 -> f235 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f243 -> f235 : B'=-1+B, [ V>=1 ], cost: 1 46: f243 -> f247 : [], cost: 1 74: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: f250 -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 51: f250 -> f263 : E'=free_19, Q'=free_21, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, [ 0>=1+free_24 && A>=G ], cost: 1 52: f250 -> f263 : E'=free_25, Q'=free_27, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, [ free_30>=1 && A>=G ], cost: 1 73: f263 -> f250 : G'=1+G, [ K>=1+H ], cost: 1 53: f263 -> f263 : K'=1+K, A1'=free_31, B1'=free_32, [ H>=K ], cost: 1 72: f277 -> f230 : A'=-1+A, [ K>=1+F ], cost: 1 56: f277 -> f277 : K'=1+K, [ F>=K ], cost: 1 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 62: f300 -> f315 : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_55, Y'=free_57, A1'=free_59, B1'=free_53, [ T>=K ], cost: 1 63: f315 -> f315 : B1'=free_60, C1'=free_61, G1'=1+G1, [ F>=G1 ], cost: 1 66: f315 -> f331 : X'=free_64, B1'=0, C1'=free_65, [ G1>=1+F ], cost: 1 67: f315 -> f331 : Q'=free_66, W'=free_67, X'=free_68, B1'=free_69, C1'=free_70, [ G1>=1+F && 0>=1+free_71 ], cost: 1 68: f315 -> f331 : Q'=free_72, W'=free_73, X'=free_74, B1'=free_75, C1'=free_76, [ G1>=1+F && free_77>=1 ], cost: 1 65: f331 -> f300 : K'=1+K, [ G1>=1+H ], cost: 1 64: f331 -> f331 : A1'=free_62, B1'=free_63, G1'=1+G1, [ H>=G1 ], cost: 1 Simplified the transitions: Start location: f0 0: f274 -> f283 : [ A>=1+B ], cost: 1 1: f274 -> f283 : [ B>=1+A ], cost: 1 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f277 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f283 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ 29>=R ], cost: 1 58: f283 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ R>=31 ], cost: 1 59: f283 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ R==30 ], cost: 1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 3: f41 -> f49 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f41 -> f156 : [ G>=1+F ], cost: 1 4: f49 -> f49 : A'=1+A, D'=free+D, J'=free, [ H>=A ], cost: 1 108: f49 -> f56 : [ 0>=1+D && A>=1+H ], cost: 1 109: f49 -> f56 : [ D>=1 && A>=1+H ], cost: 1 110: f49 -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 5: f56 -> f56 : A'=1+A, Q'=free_1, [ H>=A ], cost: 1 106: f56 -> f73 : E'=-free_99, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ free_101>=0 && A>=1+H ], cost: 1 107: f56 -> f73 : E'=free_103, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ 0>=1+free_105 && A>=1+H ], cost: 1 6: f73 -> f75 : [ F>=K ], cost: 1 105: f73 -> f88 : [ K>=1+F ], cost: 1 7: f75 -> f75 : A'=1+A, Q'=free_2, [ H>=A ], cost: 1 104: f75 -> f81 : X'=free_98, [ A>=1+H ], cost: 1 103: f81 -> f73 : K'=1+K, [ A>=1+H ], cost: 1 8: f81 -> f81 : A'=1+A, [ H>=A ], cost: 1 9: f88 -> f88 : A'=1+A, [ H>=A ], cost: 1 102: f88 -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 11: f97 -> f99 : [ F>=1+G && H>=G ], cost: 1 12: f97 -> f99 : [ G>=1+F && H>=G ], cost: 1 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 13: f99 -> f99 : A'=1+A, D'=free_3+D, L'=free_3, [ F>=A ], cost: 1 99: f99 -> f106 : [ 0>=1+D && A>=1+F ], cost: 1 100: f99 -> f106 : [ D>=1 && A>=1+F ], cost: 1 101: f99 -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 14: f106 -> f106 : A'=1+A, Q'=free_4, [ F>=A ], cost: 1 97: f106 -> f123 : E'=-free_88, X'=free_90, Y'=free_89, H1'=free_91, Q1'=free_88, J1'=free_88, [ free_90>=0 && A>=1+F ], cost: 1 98: f106 -> f123 : E'=free_92, X'=free_94, Y'=free_93, J1'=-free_92, K1'=free_95, L1'=free_92, [ 0>=1+free_94 && A>=1+F ], cost: 1 15: f123 -> f123 : A'=1+A, [ F>=A ], cost: 1 96: f123 -> f128 : [ A>=1+F ], cost: 1 16: f128 -> f130 : [ H>=K ], cost: 1 95: f128 -> f142 : [ K>=1+H ], cost: 1 17: f130 -> f130 : A'=1+A, Q'=free_5, [ F>=A ], cost: 1 94: f130 -> f135 : [ A>=1+F ], cost: 1 93: f135 -> f128 : K'=1+K, [ A>=1+F ], cost: 1 18: f135 -> f135 : A'=1+A, [ F>=A ], cost: 1 19: f142 -> f142 : A'=1+A, [ F>=A ], cost: 1 92: f142 -> f151 : M'=C, N'=free_86, O'=free_87, P'=free_87+free_86, [ A>=1+F ], cost: 1 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 32: f156 -> f156 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F ], cost: 1 24: f156 -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: f156 -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: f156 -> f191 : [ 0>=G ], cost: 1 26: f160 -> f160 : K'=1+K, [ F>=K ], cost: 1 90: f160 -> f165 : [ K>=1+F ], cost: 1 27: f165 -> f167 : [ F>=K ], cost: 1 89: f165 -> f179 : [ K>=1+F ], cost: 1 28: f167 -> f167 : A'=1+A, Q'=free_10, [ F>=A ], cost: 1 88: f167 -> f172 : [ A>=1+F ], cost: 1 87: f172 -> f165 : K'=1+K, [ A>=1+F ], cost: 1 29: f172 -> f172 : A'=1+A, [ F>=A ], cost: 1 86: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, [ K>=1+F ], cost: 1 31: f179 -> f179 : K'=1+K, Q_1'=0, [ F>=K ], cost: 1 33: f191 -> f195 : B'=1+G, E'=free_12, [ G>=1 ], cost: 1 85: f191 -> f230 : [ 0>=G ], cost: 1 34: f195 -> f195 : K'=1+K, [ F>=K ], cost: 1 82: f195 -> f202 : E'=free_83, [ K>=1+F && 0>=1+E ], cost: 1 83: f195 -> f202 : E'=free_84, [ K>=1+F && E>=1 ], cost: 1 84: f195 -> f223 : E'=0, [ K>=1+F && E==0 ], cost: 1 35: f202 -> f204 : [ F>=K ], cost: 1 81: f202 -> f217 : [ K>=1+F ], cost: 1 36: f204 -> f204 : A'=1+A, Q'=free_13, [ H>=A ], cost: 1 80: f204 -> f210 : X'=free_82, [ A>=1+H ], cost: 1 79: f210 -> f202 : K'=1+K, [ A>=1+H ], cost: 1 37: f210 -> f210 : A'=1+A, [ H>=A ], cost: 1 78: f217 -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 38: f217 -> f217 : K'=1+K, [ H>=K ], cost: 1 77: f223 -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 39: f223 -> f223 : K'=1+K, [ H>=K ], cost: 1 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 42: f235 -> f247 : [ 0>=B ], cost: 1 43: f235 -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 44: f235 -> f243 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 1 45: f235 -> f243 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 1 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f243 -> f235 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f243 -> f235 : B'=-1+B, [ V>=1 ], cost: 1 46: f243 -> f247 : [], cost: 1 74: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: f250 -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 51: f250 -> f263 : E'=free_19, Q'=free_21, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, [ 0>=1+free_24 && A>=G ], cost: 1 52: f250 -> f263 : E'=free_25, Q'=free_27, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, [ free_30>=1 && A>=G ], cost: 1 73: f263 -> f250 : G'=1+G, [ K>=1+H ], cost: 1 53: f263 -> f263 : K'=1+K, A1'=free_31, B1'=free_32, [ H>=K ], cost: 1 72: f277 -> f230 : A'=-1+A, [ K>=1+F ], cost: 1 56: f277 -> f277 : K'=1+K, [ F>=K ], cost: 1 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 62: f300 -> f315 : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_55, Y'=free_57, A1'=free_59, B1'=free_53, [ T>=K ], cost: 1 63: f315 -> f315 : B1'=free_60, C1'=free_61, G1'=1+G1, [ F>=G1 ], cost: 1 66: f315 -> f331 : X'=free_64, B1'=0, C1'=free_65, [ G1>=1+F ], cost: 1 67: f315 -> f331 : Q'=free_66, W'=free_67, X'=free_68, B1'=free_69, C1'=free_70, [ G1>=1+F ], cost: 1 68: f315 -> f331 : Q'=free_72, W'=free_73, X'=free_74, B1'=free_75, C1'=free_76, [ G1>=1+F ], cost: 1 65: f331 -> f300 : K'=1+K, [ G1>=1+H ], cost: 1 64: f331 -> f331 : A1'=free_62, B1'=free_63, G1'=1+G1, [ H>=G1 ], cost: 1 Eliminating 1 self-loops for location f49 Self-Loop 4 has the metering function: 1+H-A, resulting in the new transition 112. Removing the self-loops: 4. Eliminating 1 self-loops for location f56 Self-Loop 5 has the metering function: 1+H-A, resulting in the new transition 113. Removing the self-loops: 5. Eliminating 1 self-loops for location f75 Self-Loop 7 has the metering function: 1+H-A, resulting in the new transition 114. Removing the self-loops: 7. Eliminating 1 self-loops for location f81 Self-Loop 8 has the metering function: 1+H-A, resulting in the new transition 115. Removing the self-loops: 8. Eliminating 1 self-loops for location f88 Self-Loop 9 has the metering function: 1+H-A, resulting in the new transition 116. Removing the self-loops: 9. Eliminating 1 self-loops for location f99 Self-Loop 13 has the metering function: 1+F-A, resulting in the new transition 117. Removing the self-loops: 13. Eliminating 1 self-loops for location f106 Self-Loop 14 has the metering function: 1+F-A, resulting in the new transition 118. Removing the self-loops: 14. Eliminating 1 self-loops for location f123 Self-Loop 15 has the metering function: 1+F-A, resulting in the new transition 119. Removing the self-loops: 15. Eliminating 1 self-loops for location f130 Self-Loop 17 has the metering function: 1+F-A, resulting in the new transition 120. Removing the self-loops: 17. Eliminating 1 self-loops for location f135 Self-Loop 18 has the metering function: 1+F-A, resulting in the new transition 121. Removing the self-loops: 18. Eliminating 1 self-loops for location f142 Self-Loop 19 has the metering function: 1+F-A, resulting in the new transition 122. Removing the self-loops: 19. Eliminating 1 self-loops for location f156 Removing the self-loops: 32. Adding an epsilon transition (to model nonexecution of the loops): 124. Eliminating 1 self-loops for location f160 Self-Loop 26 has the metering function: 1-K+F, resulting in the new transition 125. Removing the self-loops: 26. Eliminating 1 self-loops for location f167 Self-Loop 28 has the metering function: 1+F-A, resulting in the new transition 126. Removing the self-loops: 28. Eliminating 1 self-loops for location f172 Self-Loop 29 has the metering function: 1+F-A, resulting in the new transition 127. Removing the self-loops: 29. Eliminating 1 self-loops for location f179 Self-Loop 31 has the metering function: 1-K+F, resulting in the new transition 128. Removing the self-loops: 31. Eliminating 1 self-loops for location f195 Self-Loop 34 has the metering function: 1-K+F, resulting in the new transition 129. Removing the self-loops: 34. Eliminating 1 self-loops for location f204 Self-Loop 36 has the metering function: 1+H-A, resulting in the new transition 130. Removing the self-loops: 36. Eliminating 1 self-loops for location f210 Self-Loop 37 has the metering function: 1+H-A, resulting in the new transition 131. Removing the self-loops: 37. Eliminating 1 self-loops for location f217 Self-Loop 38 has the metering function: 1-K+H, resulting in the new transition 132. Removing the self-loops: 38. Eliminating 1 self-loops for location f223 Self-Loop 39 has the metering function: 1-K+H, resulting in the new transition 133. Removing the self-loops: 39. Eliminating 1 self-loops for location f263 Self-Loop 53 has the metering function: 1-K+H, resulting in the new transition 134. Removing the self-loops: 53. Eliminating 1 self-loops for location f277 Self-Loop 56 has the metering function: 1-K+F, resulting in the new transition 135. Removing the self-loops: 56. Eliminating 1 self-loops for location f315 Self-Loop 63 has the metering function: 1+F-G1, resulting in the new transition 136. Removing the self-loops: 63. Eliminating 1 self-loops for location f331 Self-Loop 64 has the metering function: 1+H-G1, resulting in the new transition 137. Removing the self-loops: 64. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f274 -> f283 : [ A>=1+B ], cost: 1 1: f274 -> f283 : [ B>=1+A ], cost: 1 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f277 : A'=B, [ 0>=1+B1 && B==A ], cost: 1 57: f283 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ 29>=R ], cost: 1 58: f283 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ R>=31 ], cost: 1 59: f283 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ R==30 ], cost: 1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 3: f41 -> f49 : B'=1+G, D'=0, E'=0, Q'=0, [ F>=G && H>=G ], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f41 -> f156 : [ G>=1+F ], cost: 1 112: f49 -> [45] : A'=1+H, D'=(1+H-A)*free+D, J'=free, [ H>=A ], cost: 1+H-A 113: f56 -> [46] : A'=1+H, Q'=free_1, [ H>=A ], cost: 1+H-A 6: f73 -> f75 : [ F>=K ], cost: 1 105: f73 -> f88 : [ K>=1+F ], cost: 1 114: f75 -> [47] : A'=1+H, Q'=free_2, [ H>=A ], cost: 1+H-A 115: f81 -> [48] : A'=1+H, [ H>=A ], cost: 1+H-A 116: f88 -> [49] : A'=1+H, [ H>=A ], cost: 1+H-A 11: f97 -> f99 : [ F>=1+G && H>=G ], cost: 1 12: f97 -> f99 : [ G>=1+F && H>=G ], cost: 1 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 117: f99 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ F>=A ], cost: 1+F-A 118: f106 -> [51] : A'=1+F, Q'=free_4, [ F>=A ], cost: 1+F-A 119: f123 -> [52] : A'=1+F, [ F>=A ], cost: 1+F-A 16: f128 -> f130 : [ H>=K ], cost: 1 95: f128 -> f142 : [ K>=1+H ], cost: 1 120: f130 -> [53] : A'=1+F, Q'=free_5, [ F>=A ], cost: 1+F-A 121: f135 -> [54] : A'=1+F, [ F>=A ], cost: 1+F-A 122: f142 -> [55] : A'=1+F, [ F>=A ], cost: 1+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 123: f156 -> [56] : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F ], cost: 1 124: f156 -> [56] : [], cost: 0 125: f160 -> [57] : K'=1+F, [ F>=K ], cost: 1-K+F 27: f165 -> f167 : [ F>=K ], cost: 1 89: f165 -> f179 : [ K>=1+F ], cost: 1 126: f167 -> [58] : A'=1+F, Q'=free_10, [ F>=A ], cost: 1+F-A 127: f172 -> [59] : A'=1+F, [ F>=A ], cost: 1+F-A 128: f179 -> [60] : K'=1+F, Q_1'=0, [ F>=K ], cost: 1-K+F 33: f191 -> f195 : B'=1+G, E'=free_12, [ G>=1 ], cost: 1 85: f191 -> f230 : [ 0>=G ], cost: 1 129: f195 -> [61] : K'=1+F, [ F>=K ], cost: 1-K+F 35: f202 -> f204 : [ F>=K ], cost: 1 81: f202 -> f217 : [ K>=1+F ], cost: 1 130: f204 -> [62] : A'=1+H, Q'=free_13, [ H>=A ], cost: 1+H-A 131: f210 -> [63] : A'=1+H, [ H>=A ], cost: 1+H-A 132: f217 -> [64] : K'=1+H, [ H>=K ], cost: 1-K+H 133: f223 -> [65] : K'=1+H, [ H>=K ], cost: 1-K+H 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 42: f235 -> f247 : [ 0>=B ], cost: 1 43: f235 -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 44: f235 -> f243 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 1 45: f235 -> f243 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 1 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f243 -> f235 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f243 -> f235 : B'=-1+B, [ V>=1 ], cost: 1 46: f243 -> f247 : [], cost: 1 74: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: f250 -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 51: f250 -> f263 : E'=free_19, Q'=free_21, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, [ 0>=1+free_24 && A>=G ], cost: 1 52: f250 -> f263 : E'=free_25, Q'=free_27, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, [ free_30>=1 && A>=G ], cost: 1 134: f263 -> [66] : K'=1+H, A1'=free_31, B1'=free_32, [ H>=K ], cost: 1-K+H 135: f277 -> [67] : K'=1+F, [ F>=K ], cost: 1-K+F 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 62: f300 -> f315 : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_55, Y'=free_57, A1'=free_59, B1'=free_53, [ T>=K ], cost: 1 136: f315 -> [68] : B1'=free_60, C1'=free_61, G1'=1+F, [ F>=G1 ], cost: 1+F-G1 137: f331 -> [69] : A1'=free_62, B1'=free_63, G1'=1+H, [ H>=G1 ], cost: 1+H-G1 108: [45] -> f56 : [ 0>=1+D && A>=1+H ], cost: 1 109: [45] -> f56 : [ D>=1 && A>=1+H ], cost: 1 110: [45] -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 106: [46] -> f73 : E'=-free_99, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ free_101>=0 && A>=1+H ], cost: 1 107: [46] -> f73 : E'=free_103, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ 0>=1+free_105 && A>=1+H ], cost: 1 104: [47] -> f81 : X'=free_98, [ A>=1+H ], cost: 1 103: [48] -> f73 : K'=1+K, [ A>=1+H ], cost: 1 102: [49] -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H ], cost: 1 99: [50] -> f106 : [ 0>=1+D && A>=1+F ], cost: 1 100: [50] -> f106 : [ D>=1 && A>=1+F ], cost: 1 101: [50] -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 97: [51] -> f123 : E'=-free_88, X'=free_90, Y'=free_89, H1'=free_91, Q1'=free_88, J1'=free_88, [ free_90>=0 && A>=1+F ], cost: 1 98: [51] -> f123 : E'=free_92, X'=free_94, Y'=free_93, J1'=-free_92, K1'=free_95, L1'=free_92, [ 0>=1+free_94 && A>=1+F ], cost: 1 96: [52] -> f128 : [ A>=1+F ], cost: 1 94: [53] -> f135 : [ A>=1+F ], cost: 1 93: [54] -> f128 : K'=1+K, [ A>=1+F ], cost: 1 92: [55] -> f151 : M'=C, N'=free_86, O'=free_87, P'=free_87+free_86, [ A>=1+F ], cost: 1 24: [56] -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: [56] -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: [56] -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: [56] -> f191 : [ 0>=G ], cost: 1 90: [57] -> f165 : [ K>=1+F ], cost: 1 88: [58] -> f172 : [ A>=1+F ], cost: 1 87: [59] -> f165 : K'=1+K, [ A>=1+F ], cost: 1 86: [60] -> f156 : B'=G, E'=free_85, G'=-1+G, [ K>=1+F ], cost: 1 82: [61] -> f202 : E'=free_83, [ K>=1+F && 0>=1+E ], cost: 1 83: [61] -> f202 : E'=free_84, [ K>=1+F && E>=1 ], cost: 1 84: [61] -> f223 : E'=0, [ K>=1+F && E==0 ], cost: 1 80: [62] -> f210 : X'=free_82, [ A>=1+H ], cost: 1 79: [63] -> f202 : K'=1+K, [ A>=1+H ], cost: 1 78: [64] -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 77: [65] -> f191 : G'=-1+G, [ K>=1+H ], cost: 1 73: [66] -> f250 : G'=1+G, [ K>=1+H ], cost: 1 72: [67] -> f230 : A'=-1+A, [ K>=1+F ], cost: 1 66: [68] -> f331 : X'=free_64, B1'=0, C1'=free_65, [ G1>=1+F ], cost: 1 67: [68] -> f331 : Q'=free_66, W'=free_67, X'=free_68, B1'=free_69, C1'=free_70, [ G1>=1+F ], cost: 1 68: [68] -> f331 : Q'=free_72, W'=free_73, X'=free_74, B1'=free_75, C1'=free_76, [ G1>=1+F ], cost: 1 65: [69] -> f300 : K'=1+K, [ G1>=1+H ], cost: 1 Applied simple chaining: Start location: f0 0: f274 -> f283 : [ A>=1+B ], cost: 1 1: f274 -> f283 : [ B>=1+A ], cost: 1 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 57: f283 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ 29>=R ], cost: 1 58: f283 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ R>=31 ], cost: 1 59: f283 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ R==30 ], cost: 1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 111: f41 -> f156 : [ G>=1+F ], cost: 1 3: f41 -> [45] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A ], cost: 2+H-A 113: f56 -> [46] : A'=1+H, Q'=free_1, [ H>=A ], cost: 1+H-A 6: f73 -> f81 : A'=1+H, Q'=free_2, X'=free_98, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 105: f73 -> f97 : A'=1+H, D'=0, E'=0, Q'=0, [ K>=1+F && H>=A && 1+H>=1+H ], cost: 3+H-A 115: f81 -> f73 : A'=1+H, K'=1+K, [ H>=A && 1+H>=1+H ], cost: 2+H-A 11: f97 -> f99 : [ F>=1+G && H>=G ], cost: 1 12: f97 -> f99 : [ G>=1+F && H>=G ], cost: 1 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 117: f99 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ F>=A ], cost: 1+F-A 118: f106 -> [51] : A'=1+F, Q'=free_4, [ F>=A ], cost: 1+F-A 119: f123 -> f128 : A'=1+F, [ F>=A && 1+F>=1+F ], cost: 2+F-A 16: f128 -> f135 : A'=1+F, Q'=free_5, [ H>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 95: f128 -> f151 : A'=1+F, M'=C, N'=free_86, O'=free_87, P'=free_87+free_86, [ K>=1+H && F>=A && 1+F>=1+F ], cost: 3+F-A 121: f135 -> f128 : A'=1+F, K'=1+K, [ F>=A && 1+F>=1+F ], cost: 2+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 123: f156 -> [56] : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F ], cost: 1 124: f156 -> [56] : [], cost: 0 125: f160 -> f165 : K'=1+F, [ F>=K && 1+F>=1+F ], cost: 2-K+F 27: f165 -> f172 : A'=1+F, Q'=free_10, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 89: f165 -> f179 : [ K>=1+F ], cost: 1 127: f172 -> f165 : A'=1+F, K'=1+K, [ F>=A && 1+F>=1+F ], cost: 2+F-A 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 85: f191 -> f230 : [ 0>=G ], cost: 1 33: f191 -> [61] : B'=1+G, E'=free_12, K'=1+F, [ G>=1 && F>=K ], cost: 2-K+F 81: f202 -> f191 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 35: f202 -> f210 : A'=1+H, Q'=free_13, X'=free_82, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 131: f210 -> f202 : A'=1+H, K'=1+K, [ H>=A && 1+H>=1+H ], cost: 2+H-A 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 42: f235 -> f247 : [ 0>=B ], cost: 1 43: f235 -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 44: f235 -> f243 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 1 45: f235 -> f243 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 1 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 47: f243 -> f235 : B'=-1+B, [ 0>=1+V ], cost: 1 48: f243 -> f235 : B'=-1+B, [ V>=1 ], cost: 1 46: f243 -> f247 : [], cost: 1 74: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: f250 -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 51: f250 -> f263 : E'=free_19, Q'=free_21, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, [ 0>=1+free_24 && A>=G ], cost: 1 52: f250 -> f263 : E'=free_25, Q'=free_27, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, [ free_30>=1 && A>=G ], cost: 1 134: f263 -> f250 : G'=1+G, K'=1+H, A1'=free_31, B1'=free_32, [ H>=K && 1+H>=1+H ], cost: 2-K+H 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 62: f300 -> [68] : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_55, Y'=free_57, A1'=free_59, B1'=free_60, C1'=free_61, G1'=1+F, [ T>=K && F>=G1 ], cost: 2+F-G1 137: f331 -> f300 : K'=1+K, A1'=free_62, B1'=free_63, G1'=1+H, [ H>=G1 && 1+H>=1+H ], cost: 2+H-G1 108: [45] -> f56 : [ 0>=1+D && A>=1+H ], cost: 1 109: [45] -> f56 : [ D>=1 && A>=1+H ], cost: 1 110: [45] -> f97 : D'=0, E'=0, Q'=0, [ A>=1+H && D==0 ], cost: 1 106: [46] -> f73 : E'=-free_99, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ free_101>=0 && A>=1+H ], cost: 1 107: [46] -> f73 : E'=free_103, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ 0>=1+free_105 && A>=1+H ], cost: 1 99: [50] -> f106 : [ 0>=1+D && A>=1+F ], cost: 1 100: [50] -> f106 : [ D>=1 && A>=1+F ], cost: 1 101: [50] -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 97: [51] -> f123 : E'=-free_88, X'=free_90, Y'=free_89, H1'=free_91, Q1'=free_88, J1'=free_88, [ free_90>=0 && A>=1+F ], cost: 1 98: [51] -> f123 : E'=free_92, X'=free_94, Y'=free_93, J1'=-free_92, K1'=free_95, L1'=free_92, [ 0>=1+free_94 && A>=1+F ], cost: 1 24: [56] -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 25: [56] -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 30: [56] -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 91: [56] -> f191 : [ 0>=G ], cost: 1 84: [61] -> f191 : E'=0, G'=-1+G, K'=1+H, [ K>=1+F && E==0 && H>=K && 1+H>=1+H ], cost: 3-K+H 82: [61] -> f202 : E'=free_83, [ K>=1+F && 0>=1+E ], cost: 1 83: [61] -> f202 : E'=free_84, [ K>=1+F && E>=1 ], cost: 1 66: [68] -> f331 : X'=free_64, B1'=0, C1'=free_65, [ G1>=1+F ], cost: 1 67: [68] -> f331 : Q'=free_66, W'=free_67, X'=free_68, B1'=free_69, C1'=free_70, [ G1>=1+F ], cost: 1 68: [68] -> f331 : Q'=free_72, W'=free_73, X'=free_74, B1'=free_75, C1'=free_76, [ G1>=1+F ], cost: 1 Applied chaining over branches and pruning: Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 165: f274 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ A>=1+B && 29>=R ], cost: 2 166: f274 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ A>=1+B && R>=31 ], cost: 2 167: f274 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ A>=1+B && R==30 ], cost: 2 168: f274 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ B>=1+A && 29>=R ], cost: 2 170: f274 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ B>=1+A && R==30 ], cost: 2 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 138: f41 -> f56 : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 139: f41 -> f56 : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 140: f41 -> f97 : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 141: f56 -> f73 : A'=1+H, E'=-free_99, Q'=free_1, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ H>=A && free_101>=0 && 1+H>=1+H ], cost: 2+H-A 142: f56 -> f73 : A'=1+H, E'=free_103, Q'=free_1, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ H>=A && 0>=1+free_105 && 1+H>=1+H ], cost: 2+H-A 105: f73 -> f97 : A'=1+H, D'=0, E'=0, Q'=0, [ K>=1+F && H>=A && 1+H>=1+H ], cost: 3+H-A 143: f73 -> [70] : A'=1+H, Q'=free_2, X'=free_98, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 144: f97 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ F>=1+G && H>=G && F>=A ], cost: 2+F-A 145: f97 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ G>=1+F && H>=G && F>=A ], cost: 2+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 146: f156 -> f160 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 ], cost: 2 147: f156 -> f160 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 ], cost: 2 150: f156 -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 151: f156 -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 152: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 125: f160 -> f165 : K'=1+F, [ F>=K && 1+F>=1+F ], cost: 2-K+F 89: f165 -> f179 : [ K>=1+F ], cost: 1 154: f165 -> [71] : A'=1+F, Q'=free_10, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 155: f191 -> f191 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && 1+F>=1+F && free_12==0 && H>=1+F && 1+H>=1+H ], cost: 4-K+H 156: f191 -> f202 : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 157: f191 -> f202 : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 85: f191 -> f230 : [ 0>=G ], cost: 1 81: f202 -> f191 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 158: f202 -> [72] : A'=1+H, Q'=free_13, X'=free_82, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 159: f235 -> f235 : B'=-1+B, T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 2 160: f235 -> f235 : B'=-1+B, T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 2 162: f235 -> f235 : B'=-1+B, T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 2 163: f235 -> f235 : B'=-1+B, T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 && free_18>=1 ], cost: 2 42: f235 -> f247 : [ 0>=B ], cost: 1 43: f235 -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 161: f235 -> f247 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 2 164: f235 -> f247 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 2 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 74: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: f250 -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 174: f250 -> f250 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_32, [ 0>=1+free_24 && A>=G && H>=K && 1+H>=1+H ], cost: 3-K+H 175: f250 -> f250 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_32, [ free_30>=1 && A>=G && H>=K && 1+H>=1+H ], cost: 3-K+H 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 171: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_64, Y'=free_57, A1'=free_59, B1'=0, C1'=free_65, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 172: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_66, W'=free_67, X'=free_68, Y'=free_57, A1'=free_59, B1'=free_69, C1'=free_70, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 173: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_72, W'=free_73, X'=free_74, Y'=free_57, A1'=free_59, B1'=free_75, C1'=free_76, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 137: f331 -> f300 : K'=1+K, A1'=free_62, B1'=free_63, G1'=1+H, [ H>=G1 && 1+H>=1+H ], cost: 2+H-G1 101: [50] -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 Eliminating 1 self-loops for location f191 Removing the self-loops: 155. Adding an epsilon transition (to model nonexecution of the loops): 177. Eliminating 4 self-loops for location f235 Self-Loop 159 has the metering function: B, resulting in the new transition 178. Self-Loop 160 has the metering function: B, resulting in the new transition 179. Self-Loop 162 has the metering function: B, resulting in the new transition 180. Self-Loop 163 has the metering function: B, resulting in the new transition 181. Removing the self-loops: 159 160 162 163. Eliminating 2 self-loops for location f250 Removing the self-loops: 174 175. Adding an epsilon transition (to model nonexecution of the loops): 184. Removed all Self-loops using metering functions (where possible): Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 165: f274 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ A>=1+B && 29>=R ], cost: 2 166: f274 -> f292 : E'=free_39, T'=-1+A, X'=free_41, Y'=free_40, A1'=free_42, C1'=free_43, [ A>=1+B && R>=31 ], cost: 2 167: f274 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ A>=1+B && R==30 ], cost: 2 168: f274 -> f292 : E'=free_34, T'=-1+A, X'=free_36, Y'=free_35, A1'=free_37, C1'=free_38, [ B>=1+A && 29>=R ], cost: 2 170: f274 -> f292 : E'=free_44, R'=30, T'=-1+A, X'=free_46, Y'=free_45, A1'=free_47, C1'=free_48, [ B>=1+A && R==30 ], cost: 2 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 138: f41 -> f56 : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 139: f41 -> f56 : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 140: f41 -> f97 : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 141: f56 -> f73 : A'=1+H, E'=-free_99, Q'=free_1, X'=free_101, Y'=free_102, M1'=free_100, N1'=free_99, O1'=free_99, [ H>=A && free_101>=0 && 1+H>=1+H ], cost: 2+H-A 142: f56 -> f73 : A'=1+H, E'=free_103, Q'=free_1, X'=free_105, Y'=free_106, O1'=-free_103, P1'=free_104, Q1_1'=free_103, [ H>=A && 0>=1+free_105 && 1+H>=1+H ], cost: 2+H-A 105: f73 -> f97 : A'=1+H, D'=0, E'=0, Q'=0, [ K>=1+F && H>=A && 1+H>=1+H ], cost: 3+H-A 143: f73 -> [70] : A'=1+H, Q'=free_2, X'=free_98, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 144: f97 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ F>=1+G && H>=G && F>=A ], cost: 2+F-A 145: f97 -> [50] : A'=1+F, D'=(1+F-A)*free_3+D, L'=free_3, [ G>=1+F && H>=G && F>=A ], cost: 2+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 146: f156 -> f160 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 ], cost: 2 147: f156 -> f160 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 ], cost: 2 150: f156 -> f160 : [ F>=1+G && 0>=1+E && G>=1 ], cost: 1 151: f156 -> f160 : [ F>=1+G && E>=1 && G>=1 ], cost: 1 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 152: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 125: f160 -> f165 : K'=1+F, [ F>=K && 1+F>=1+F ], cost: 2-K+F 89: f165 -> f179 : [ K>=1+F ], cost: 1 154: f165 -> [71] : A'=1+F, Q'=free_10, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 176: f191 -> [73] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 177: f191 -> [73] : [], cost: 0 81: f202 -> f191 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 158: f202 -> [72] : A'=1+H, Q'=free_13, X'=free_82, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 41: f232 -> f235 : S'=1, [ 30>=R ], cost: 1 178: f235 -> [74] : B'=0, T'=0, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 2*B 179: f235 -> [74] : B'=0, T'=0, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 2*B 180: f235 -> [74] : B'=0, T'=0, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 2*B 181: f235 -> [74] : B'=0, T'=0, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 && free_18>=1 ], cost: 2*B 54: f247 -> f274 : S'=0, B1'=free_33, [ S==0 ], cost: 1 49: f247 -> f250 : Q'=1, W'=0, [ 0>=1+S ], cost: 1 50: f247 -> f250 : Q'=1, W'=0, [ S>=1 ], cost: 1 182: f250 -> [75] : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_32, [ 0>=1+free_24 && A>=G && H>=K ], cost: 3-K+H 183: f250 -> [75] : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_32, [ free_30>=1 && A>=G && H>=K ], cost: 3-K+H 184: f250 -> [75] : [], cost: 0 60: f292 -> f300 : Q'=1, W'=1, X'=free_49, D1'=free_50, E1'=free_50, [ X>=0 ], cost: 1 61: f292 -> f300 : Q'=1, W'=1, X'=free_51, E1'=-free_52, F1'=free_52, [ 0>=1+X ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 171: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_56, W'=free_58, X'=free_64, Y'=free_57, A1'=free_59, B1'=0, C1'=free_65, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 172: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_66, W'=free_67, X'=free_68, Y'=free_57, A1'=free_59, B1'=free_69, C1'=free_70, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 173: f300 -> f331 : E'=free_54, G'=1+K, Q'=free_72, W'=free_73, X'=free_74, Y'=free_57, A1'=free_59, B1'=free_75, C1'=free_76, G1'=1+F, [ T>=K && F>=G1 && 1+F>=1+F ], cost: 3+F-G1 137: f331 -> f300 : K'=1+K, A1'=free_62, B1'=free_63, G1'=1+H, [ H>=G1 && 1+H>=1+H ], cost: 2+H-G1 101: [50] -> f151 : D'=0, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ A>=1+F && D==0 ], cost: 1 156: [73] -> f202 : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 157: [73] -> f202 : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 85: [73] -> f230 : [ 0>=G ], cost: 1 42: [74] -> f247 : [ 0>=B ], cost: 1 43: [74] -> f247 : S'=0, T'=-1+B, U'=-free_14+C, [ B>=1 ], cost: 1 161: [74] -> f247 : T'=-1+B, U'=free_15, V'=free_16, [ 0>=1+free_15 && B>=1 ], cost: 2 164: [74] -> f247 : T'=-1+B, U'=free_17, V'=free_18, [ free_17>=1 && B>=1 ], cost: 2 74: [75] -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 75: [75] -> f274 : X'=free_81, Z'=C-free_79, B1'=free_80, [ A>=G ], cost: 1 Applied chaining over branches and pruning: Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 215: f274 -> f300 : E'=free_34, Q'=1, T'=-1+A, W'=1, X'=free_49, Y'=free_35, A1'=free_37, C1'=free_38, D1'=free_50, E1'=free_50, [ A>=1+B && 29>=R && free_36>=0 ], cost: 3 216: f274 -> f300 : E'=free_34, Q'=1, T'=-1+A, W'=1, X'=free_51, Y'=free_35, A1'=free_37, C1'=free_38, E1'=-free_52, F1'=free_52, [ A>=1+B && 29>=R && 0>=1+free_36 ], cost: 3 218: f274 -> f300 : E'=free_39, Q'=1, T'=-1+A, W'=1, X'=free_51, Y'=free_40, A1'=free_42, C1'=free_43, E1'=-free_52, F1'=free_52, [ A>=1+B && R>=31 && 0>=1+free_41 ], cost: 3 219: f274 -> f300 : E'=free_44, Q'=1, R'=30, T'=-1+A, W'=1, X'=free_49, Y'=free_45, A1'=free_47, C1'=free_48, D1'=free_50, E1'=free_50, [ A>=1+B && R==30 && free_46>=0 ], cost: 3 220: f274 -> f300 : E'=free_44, Q'=1, R'=30, T'=-1+A, W'=1, X'=free_51, Y'=free_45, A1'=free_47, C1'=free_48, E1'=-free_52, F1'=free_52, [ A>=1+B && R==30 && 0>=1+free_46 ], cost: 3 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 140: f41 -> f97 : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 185: f41 -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: f41 -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: f41 -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: f41 -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 189: f97 -> f151 : A'=1+F, D'=0, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ F>=1+G && H>=G && F>=A && 1+F>=1+F && (1+F-A)*free_3+D==0 ], cost: 3+F-A 190: f97 -> f151 : A'=1+F, D'=0, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ G>=1+F && H>=G && F>=A && 1+F>=1+F && (1+F-A)*free_3+D==0 ], cost: 3+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 191: f156 -> f165 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 192: f156 -> f165 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 193: f156 -> f165 : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 194: f156 -> f165 : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 152: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 89: f165 -> f179 : [ K>=1+F ], cost: 1 154: f165 -> [71] : A'=1+F, Q'=free_10, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 198: f191 -> f202 : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 199: f191 -> f202 : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 197: f191 -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: f191 -> f230 : [ 0>=G ], cost: 1 195: f191 -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: f191 -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 81: f202 -> f191 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 158: f202 -> [72] : A'=1+H, Q'=free_13, X'=free_82, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 201: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 202: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 203: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 204: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 228: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_78, [ 0>=1+free_24 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 229: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 230: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_78, [ free_30>=1 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 231: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 232: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 69: f300 -> f232 : R'=1+R, [ K>=1+T ], cost: 1 225: f300 -> f300 : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, G1'=1+H, [ T>=K && F>=G1 && 1+F>=1+F && H>=1+F && 1+H>=1+H ], cost: 4+H-G1 226: f300 -> f300 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, G1'=1+H, [ T>=K && F>=G1 && 1+F>=1+F && H>=1+F && 1+H>=1+H ], cost: 4+H-G1 227: f300 -> f300 : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, G1'=1+H, [ T>=K && F>=G1 && 1+F>=1+F && H>=1+F && 1+H>=1+H ], cost: 4+H-G1 205: [74] -> f274 : S'=0, B1'=free_33, [ 0>=B && S==0 ], cost: 2 208: [74] -> f274 : S'=0, T'=-1+B, U'=-free_14+C, B1'=free_33, [ B>=1 && 0==0 ], cost: 2 209: [74] -> f274 : S'=0, T'=-1+B, U'=free_15, V'=free_16, B1'=free_33, [ 0>=1+free_15 && B>=1 && S==0 ], cost: 3 212: [74] -> f274 : S'=0, T'=-1+B, U'=free_17, V'=free_18, B1'=free_33, [ free_17>=1 && B>=1 && S==0 ], cost: 3 206: [74] -> f250 : Q'=1, W'=0, [ 0>=B && 0>=1+S ], cost: 2 207: [74] -> f250 : Q'=1, W'=0, [ 0>=B && S>=1 ], cost: 2 210: [74] -> f250 : Q'=1, T'=-1+B, U'=free_15, V'=free_16, W'=0, [ 0>=1+free_15 && B>=1 && 0>=1+S ], cost: 3 211: [74] -> f250 : Q'=1, T'=-1+B, U'=free_15, V'=free_16, W'=0, [ 0>=1+free_15 && B>=1 && S>=1 ], cost: 3 214: [74] -> f250 : Q'=1, T'=-1+B, U'=free_17, V'=free_18, W'=0, [ free_17>=1 && B>=1 && S>=1 ], cost: 3 Eliminating 3 self-loops for location f300 Removing the self-loops: 225 226 227. Adding an epsilon transition (to model nonexecution of the loops): 237. Removed all Self-loops using metering functions (where possible): Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 215: f274 -> f300 : E'=free_34, Q'=1, T'=-1+A, W'=1, X'=free_49, Y'=free_35, A1'=free_37, C1'=free_38, D1'=free_50, E1'=free_50, [ A>=1+B && 29>=R && free_36>=0 ], cost: 3 216: f274 -> f300 : E'=free_34, Q'=1, T'=-1+A, W'=1, X'=free_51, Y'=free_35, A1'=free_37, C1'=free_38, E1'=-free_52, F1'=free_52, [ A>=1+B && 29>=R && 0>=1+free_36 ], cost: 3 218: f274 -> f300 : E'=free_39, Q'=1, T'=-1+A, W'=1, X'=free_51, Y'=free_40, A1'=free_42, C1'=free_43, E1'=-free_52, F1'=free_52, [ A>=1+B && R>=31 && 0>=1+free_41 ], cost: 3 219: f274 -> f300 : E'=free_44, Q'=1, R'=30, T'=-1+A, W'=1, X'=free_49, Y'=free_45, A1'=free_47, C1'=free_48, D1'=free_50, E1'=free_50, [ A>=1+B && R==30 && free_46>=0 ], cost: 3 220: f274 -> f300 : E'=free_44, Q'=1, R'=30, T'=-1+A, W'=1, X'=free_51, Y'=free_45, A1'=free_47, C1'=free_48, E1'=-free_52, F1'=free_52, [ A>=1+B && R==30 && 0>=1+free_46 ], cost: 3 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 10: f41 -> f97 : B'=1+G, D'=0, E'=0, Q'=0, [ G>=1+H && F>=G ], cost: 1 140: f41 -> f97 : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 185: f41 -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: f41 -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: f41 -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: f41 -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 20: f97 -> f151 : M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H ], cost: 1 21: f97 -> f151 : F'=G, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=F && G==F ], cost: 1 189: f97 -> f151 : A'=1+F, D'=0, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ F>=1+G && H>=G && F>=A && 1+F>=1+F && (1+F-A)*free_3+D==0 ], cost: 3+F-A 190: f97 -> f151 : A'=1+F, D'=0, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ G>=1+F && H>=G && F>=A && 1+F>=1+F && (1+F-A)*free_3+D==0 ], cost: 3+F-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 191: f156 -> f165 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 192: f156 -> f165 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 193: f156 -> f165 : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 194: f156 -> f165 : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 152: f156 -> f179 : E'=0, [ G>=1 && F>=1+G && E==0 ], cost: 1 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 89: f165 -> f179 : [ K>=1+F ], cost: 1 154: f165 -> [71] : A'=1+F, Q'=free_10, [ F>=K && F>=A && 1+F>=1+F ], cost: 3+F-A 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 198: f191 -> f202 : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 199: f191 -> f202 : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 197: f191 -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: f191 -> f230 : [ 0>=G ], cost: 1 195: f191 -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: f191 -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 81: f202 -> f191 : G'=-1+G, K'=1+H, [ K>=1+F && H>=K && 1+H>=1+H ], cost: 3-K+H 158: f202 -> [72] : A'=1+H, Q'=free_13, X'=free_82, [ F>=K && H>=A && 1+H>=1+H ], cost: 3+H-A 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 201: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 202: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 203: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 204: f232 -> [74] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 228: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_78, [ 0>=1+free_24 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 229: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 230: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_78, [ free_30>=1 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 231: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 232: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 234: f300 -> [82] : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, G1'=1+H, [ T>=K && F>=G1 && H>=1+F ], cost: 4+H-G1 235: f300 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, G1'=1+H, [ T>=K && F>=G1 && H>=1+F ], cost: 4+H-G1 236: f300 -> [82] : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, G1'=1+H, [ T>=K && F>=G1 && H>=1+F ], cost: 4+H-G1 237: f300 -> [82] : [], cost: 0 205: [74] -> f274 : S'=0, B1'=free_33, [ 0>=B && S==0 ], cost: 2 208: [74] -> f274 : S'=0, T'=-1+B, U'=-free_14+C, B1'=free_33, [ B>=1 && 0==0 ], cost: 2 209: [74] -> f274 : S'=0, T'=-1+B, U'=free_15, V'=free_16, B1'=free_33, [ 0>=1+free_15 && B>=1 && S==0 ], cost: 3 212: [74] -> f274 : S'=0, T'=-1+B, U'=free_17, V'=free_18, B1'=free_33, [ free_17>=1 && B>=1 && S==0 ], cost: 3 206: [74] -> f250 : Q'=1, W'=0, [ 0>=B && 0>=1+S ], cost: 2 207: [74] -> f250 : Q'=1, W'=0, [ 0>=B && S>=1 ], cost: 2 210: [74] -> f250 : Q'=1, T'=-1+B, U'=free_15, V'=free_16, W'=0, [ 0>=1+free_15 && B>=1 && 0>=1+S ], cost: 3 211: [74] -> f250 : Q'=1, T'=-1+B, U'=free_15, V'=free_16, W'=0, [ 0>=1+free_15 && B>=1 && S>=1 ], cost: 3 214: [74] -> f250 : Q'=1, T'=-1+B, U'=free_17, V'=free_18, W'=0, [ free_17>=1 && B>=1 && S>=1 ], cost: 3 69: [82] -> f232 : R'=1+R, [ K>=1+T ], cost: 1 Applied chaining over branches and pruning: Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 291: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, T'=-1+A, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 292: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 297: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, T'=-1+A, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && 29>=R && 0>=1+free_36 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 304: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=30, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && R==30 && free_46>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 308: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=30, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && R==30 && 0>=1+free_46 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 238: f41 -> f151 : B'=1+G, D'=0, E'=0, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && G>=1+H ], cost: 2 240: f41 -> f151 : A'=1+H, B'=1+G, D'=0, E'=0, F'=G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && H>=F && G==F ], cost: 4+H-A 241: f41 -> f151 : A'=1+F, B'=1+G, D'=0, E'=0, Q'=0, J'=free, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && F>=1+G && H>=G && F>=1+H && 1+F>=1+F && -free_3*(H-F)==0 ], cost: 5+F-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 185: f41 -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: f41 -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: f41 -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: f41 -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 239: f41 -> [83] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 242: f41 -> [84] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 243: f156 -> f179 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 245: f156 -> f179 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 247: f156 -> f179 : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 249: f156 -> f179 : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 244: f156 -> [85] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 246: f156 -> [86] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 248: f156 -> [87] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 250: f156 -> [88] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 251: f191 -> f191 : B'=1+G, E'=free_83, G'=-1+G, K'=1+H, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 && 1+F>=1+F && H>=1+F && 1+H>=1+H ], cost: 5-K+H 253: f191 -> f191 : B'=1+G, E'=free_84, G'=-1+G, K'=1+H, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 && 1+F>=1+F && H>=1+F && 1+H>=1+H ], cost: 5-K+H 197: f191 -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: f191 -> f230 : [ 0>=G ], cost: 1 195: f191 -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: f191 -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 252: f191 -> [89] : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 254: f191 -> [90] : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 260: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_15, V'=free_16, W'=0, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 ], cost: 3+2*B 269: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_15, V'=free_16, W'=0, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 && 0>=0 && 1>=1 ], cost: 3+2*B 278: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_17, V'=free_18, W'=0, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 && 0>=0 && 1>=1 ], cost: 3+2*B 287: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_17, V'=free_18, W'=0, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 && 0>=0 && 1>=1 ], cost: 3+2*B 255: f232 -> [91] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 256: f232 -> [92] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 257: f232 -> [93] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 258: f232 -> [94] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 259: f232 -> [95] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 261: f232 -> [96] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 262: f232 -> [97] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 263: f232 -> [98] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 264: f232 -> [99] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 265: f232 -> [100] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 266: f232 -> [101] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 267: f232 -> [102] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 268: f232 -> [103] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 270: f232 -> [104] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 271: f232 -> [105] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 272: f232 -> [106] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 273: f232 -> [107] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 274: f232 -> [108] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 275: f232 -> [109] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 276: f232 -> [110] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 277: f232 -> [111] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 279: f232 -> [112] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 280: f232 -> [113] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 281: f232 -> [114] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 282: f232 -> [115] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 283: f232 -> [116] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 284: f232 -> [117] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 285: f232 -> [118] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 286: f232 -> [119] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 288: f232 -> [120] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 289: f232 -> [121] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 290: f232 -> [122] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 228: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_78, [ 0>=1+free_24 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 229: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 230: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_78, [ free_30>=1 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 231: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 232: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 69: [82] -> f232 : R'=1+R, [ K>=1+T ], cost: 1 Eliminating 2 self-loops for location f191 Removing the self-loops: 251 253. Adding an epsilon transition (to model nonexecution of the loops): 313. Removed all Self-loops using metering functions (where possible): Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 291: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, T'=-1+A, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 292: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 297: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, T'=-1+A, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && 29>=R && 0>=1+free_36 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 304: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=30, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && R==30 && free_46>=0 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 308: f274 -> [82] : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=30, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && R==30 && 0>=1+free_46 && -1+A>=K && F>=G1 && H>=1+F ], cost: 7+H-G1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 238: f41 -> f151 : B'=1+G, D'=0, E'=0, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && G>=1+H ], cost: 2 240: f41 -> f151 : A'=1+H, B'=1+G, D'=0, E'=0, F'=G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && H>=F && G==F ], cost: 4+H-A 241: f41 -> f151 : A'=1+F, B'=1+G, D'=0, E'=0, Q'=0, J'=free, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && F>=1+G && H>=G && F>=1+H && 1+F>=1+F && -free_3*(H-F)==0 ], cost: 5+F-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 185: f41 -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: f41 -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: f41 -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: f41 -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 239: f41 -> [83] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 242: f41 -> [84] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 22: f151 -> f41 : C'=M, G'=1+G, [ M>=1+P ], cost: 1 23: f151 -> f41 : C'=P, G'=1+G, [ P>=M ], cost: 1 148: f156 -> f179 : B'=G, E'=0, G'=-1+G, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 ], cost: 2 243: f156 -> f179 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 245: f156 -> f179 : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 247: f156 -> f179 : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 249: f156 -> f179 : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 149: f156 -> f191 : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 153: f156 -> f191 : [ 0>=G ], cost: 1 244: f156 -> [85] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 246: f156 -> [86] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 248: f156 -> [87] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 250: f156 -> [88] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 128: f179 -> f156 : B'=G, E'=free_85, G'=-1+G, K'=1+F, Q_1'=0, [ F>=K && 1+F>=1+F ], cost: 2-K+F 311: f191 -> [123] : B'=1+G, E'=free_83, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 5-K+H 312: f191 -> [123] : B'=1+G, E'=free_84, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 5-K+H 313: f191 -> [123] : [], cost: 0 40: f230 -> f232 : [ A>=1 ], cost: 1 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 260: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_15, V'=free_16, W'=0, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 ], cost: 3+2*B 269: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_15, V'=free_16, W'=0, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 && 0>=0 && 1>=1 ], cost: 3+2*B 278: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_17, V'=free_18, W'=0, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 && 0>=0 && 1>=1 ], cost: 3+2*B 287: f232 -> f250 : B'=0, Q'=1, S'=1, T'=0, U'=free_17, V'=free_18, W'=0, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 && 0>=0 && 1>=1 ], cost: 3+2*B 255: f232 -> [91] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 256: f232 -> [92] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 257: f232 -> [93] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 258: f232 -> [94] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 259: f232 -> [95] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 261: f232 -> [96] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 262: f232 -> [97] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 263: f232 -> [98] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 264: f232 -> [99] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 265: f232 -> [100] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 266: f232 -> [101] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 267: f232 -> [102] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 268: f232 -> [103] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 270: f232 -> [104] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 271: f232 -> [105] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 272: f232 -> [106] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 273: f232 -> [107] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 274: f232 -> [108] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 275: f232 -> [109] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 276: f232 -> [110] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 277: f232 -> [111] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 279: f232 -> [112] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 280: f232 -> [113] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 281: f232 -> [114] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 282: f232 -> [115] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 283: f232 -> [116] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 284: f232 -> [117] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 285: f232 -> [118] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 286: f232 -> [119] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 288: f232 -> [120] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 289: f232 -> [121] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 290: f232 -> [122] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 228: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_20, Y'=free_22, Z'=free_24, A1'=free_31, B1'=free_78, [ 0>=1+free_24 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 229: f250 -> f274 : E'=free_19, G'=1+G, Q'=free_21, K'=1+H, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 230: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_26, Y'=free_28, Z'=free_30, A1'=free_31, B1'=free_78, [ free_30>=1 && A>=G && H>=K && 1+G>=1+A ], cost: 4-K+H 231: f250 -> f274 : E'=free_25, G'=1+G, Q'=free_27, K'=1+H, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 4-K+H 232: f250 -> f274 : B1'=free_78, [ G>=1+A ], cost: 1 69: [82] -> f232 : R'=1+R, [ K>=1+T ], cost: 1 197: [123] -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: [123] -> f230 : [ 0>=G ], cost: 1 195: [123] -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: [123] -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 252: [123] -> [89] : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 254: [123] -> [90] : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F Applied chaining over branches and pruning: Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 347: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, R'=1+R, T'=-1+A, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 348: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=1+R, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 349: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, R'=1+R, T'=-1+A, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && 29>=R && 0>=1+free_36 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 350: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=31, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && R==30 && free_46>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 351: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=31, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && R==30 && 0>=1+free_46 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 314: f41 -> f41 : B'=1+G, C'=C, D'=0, E'=0, G'=1+G, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && G>=1+H && C>=1+free_6+free_7 ], cost: 3 315: f41 -> f41 : B'=1+G, C'=free_6+free_7, D'=0, E'=0, G'=1+G, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && G>=1+H && free_6+free_7>=C ], cost: 3 316: f41 -> f41 : A'=1+H, B'=1+G, C'=C, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && H>=F && G==F && C>=1+free_9+free_8 ], cost: 5+H-A 317: f41 -> f41 : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=C ], cost: 5+H-A 319: f41 -> f41 : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 && F>=1+G && H>=G && F>=1+H && 1+F>=1+F && -free_3*(H-F)==0 && free_96+free_97>=C ], cost: 6+F-A 111: f41 -> f156 : [ G>=1+F ], cost: 1 185: f41 -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: f41 -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: f41 -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: f41 -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 239: f41 -> [83] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 242: f41 -> [84] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 320: f156 -> f156 : B'=-1+G, E'=free_85, G'=-2+G, K'=1+F, Q_1'=0, [ G>=1 && G>=F && -1+G>=1 && F>=G && free_11==0 && F>=K && 1+F>=1+F ], cost: 4-K+F 244: f156 -> [85] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 246: f156 -> [86] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 248: f156 -> [87] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 250: f156 -> [88] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 325: f156 -> [123] : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 326: f156 -> [123] : [ 0>=G ], cost: 1 321: f156 -> [124] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 322: f156 -> [125] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 323: f156 -> [126] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 324: f156 -> [127] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 40: f230 -> f232 : [ A>=1 ], cost: 1 328: f232 -> f274 : B'=0, E'=free_19, G'=1+G, Q'=free_21, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 && 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 330: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 333: f232 -> f274 : B'=0, E'=free_19, G'=1+G, Q'=free_21, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 && 0>=0 && 1>=1 && 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 340: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_17, V'=free_18, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 345: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_17, V'=free_18, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 255: f232 -> [91] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 256: f232 -> [92] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 257: f232 -> [93] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 258: f232 -> [94] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 259: f232 -> [95] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 261: f232 -> [96] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 262: f232 -> [97] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 263: f232 -> [98] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 264: f232 -> [99] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 265: f232 -> [100] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 266: f232 -> [101] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 267: f232 -> [102] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 268: f232 -> [103] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 270: f232 -> [104] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 271: f232 -> [105] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 272: f232 -> [106] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 273: f232 -> [107] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 274: f232 -> [108] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 275: f232 -> [109] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 276: f232 -> [110] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 277: f232 -> [111] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 279: f232 -> [112] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 280: f232 -> [113] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 281: f232 -> [114] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 282: f232 -> [115] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 283: f232 -> [116] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 284: f232 -> [117] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 285: f232 -> [118] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 286: f232 -> [119] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 288: f232 -> [120] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 289: f232 -> [121] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 290: f232 -> [122] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 197: [123] -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: [123] -> f230 : [ 0>=G ], cost: 1 195: [123] -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: [123] -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 252: [123] -> [89] : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 254: [123] -> [90] : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F Eliminating 5 self-loops for location f41 Self-Loop 314 has the metering function: 1+F-G, resulting in the new transition 352. Removing the self-loops: 314 315 316 317 319. Adding an epsilon transition (to model nonexecution of the loops): 357. Eliminating 1 self-loops for location f156 Self-Loop 320 has the metering function: meter, resulting in the new transition 358. Removing the self-loops: 320. Removed all Self-loops using metering functions (where possible): Start location: f0 71: f274 -> f230 : A'=-1+B, [ B1>=0 && B==A ], cost: 1 55: f274 -> f230 : A'=-1+B, K'=1+F, [ 0>=1+B1 && B==A && F>=K && 1+F>=1+F ], cost: 3-K+F 347: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_56, K'=1+K, R'=1+R, T'=-1+A, W'=free_58, X'=free_64, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_65, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 348: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=1+R, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && 29>=R && free_36>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 349: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_72, K'=1+K, R'=1+R, T'=-1+A, W'=free_73, X'=free_74, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_76, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && 29>=R && 0>=1+free_36 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 350: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=31, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, D1'=free_50, E1'=free_50, G1'=1+H, [ A>=1+B && R==30 && free_46>=0 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 351: f274 -> f232 : E'=free_54, G'=1+K, Q'=free_66, K'=1+K, R'=31, T'=-1+A, W'=free_67, X'=free_68, Y'=free_57, A1'=free_62, B1'=free_63, C1'=free_70, E1'=-free_52, F1'=free_52, G1'=1+H, [ A>=1+B && R==30 && 0>=1+free_46 && -1+A>=K && F>=G1 && H>=1+F && 1+K>=A ], cost: 8+H-G1 2: f0 -> f41 : C'=0, D'=0, E'=0, [], cost: 1 352: f41 -> [128] : B'=1+F, D'=0, E'=0, G'=1+F, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && C>=1+free_6+free_7 ], cost: 3+3*F-3*G 353: f41 -> [128] : B'=1+G, C'=free_6+free_7, D'=0, E'=0, G'=1+G, Q'=0, M'=C, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && free_6+free_7>=C ], cost: 3 354: f41 -> [128] : A'=1+H, B'=1+G, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && C>=1+free_9+free_8 ], cost: 5+H-A 355: f41 -> [128] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=C, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=C ], cost: 5+H-A 356: f41 -> [128] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=C, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=C ], cost: 6+F-A 357: f41 -> [128] : [], cost: 0 358: f156 -> [129] : B'=1-2*meter+G, E'=free_85, G'=-2*meter+G, K'=1+F, Q_1'=0, [ F-G==0 && -1+G>=1 && F>=K && 2*meter==-F+G ], cost: 3*meter 40: f230 -> f232 : [ A>=1 ], cost: 1 328: f232 -> f274 : B'=0, E'=free_19, G'=1+G, Q'=free_21, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 && 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 330: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 333: f232 -> f274 : B'=0, E'=free_19, G'=1+G, Q'=free_21, K'=1+H, S'=1, T'=0, U'=free_15, V'=free_16, W'=free_23, X'=free_81, Y'=free_22, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 && 0>=0 && 1>=1 && 0>=1+free_24 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 340: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_17, V'=free_18, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 345: f232 -> f274 : B'=0, E'=free_25, G'=1+G, Q'=free_27, K'=1+H, S'=1, T'=0, U'=free_17, V'=free_18, W'=free_29, X'=free_81, Y'=free_28, Z'=C-free_79, A1'=free_31, B1'=free_80, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 && 0>=0 && 1>=1 && free_30>=1 && A>=G && H>=K && A>=1+G ], cost: 7-K+H+2*B 70: f232 -> f230 : A'=-1+A, [ R>=31 ], cost: 1 255: f232 -> [91] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 256: f232 -> [92] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 257: f232 -> [93] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 258: f232 -> [94] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 259: f232 -> [95] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 261: f232 -> [96] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 262: f232 -> [97] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 263: f232 -> [98] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && 0>=1+free_16 ], cost: 1+2*B 264: f232 -> [99] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 265: f232 -> [100] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 266: f232 -> [101] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 267: f232 -> [102] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 268: f232 -> [103] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 270: f232 -> [104] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 271: f232 -> [105] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 272: f232 -> [106] : B'=0, S'=1, T'=0, U'=free_15, V'=free_16, [ 30>=R && 0>=1+free_15 && B>=1 && free_16>=1 ], cost: 1+2*B 273: f232 -> [107] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 274: f232 -> [108] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 275: f232 -> [109] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 276: f232 -> [110] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 277: f232 -> [111] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 279: f232 -> [112] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 280: f232 -> [113] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 281: f232 -> [114] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && 0>=1+free_18 ], cost: 1+2*B 282: f232 -> [115] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 283: f232 -> [116] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 284: f232 -> [117] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 285: f232 -> [118] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 286: f232 -> [119] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 288: f232 -> [120] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 289: f232 -> [121] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 290: f232 -> [122] : B'=0, S'=1, T'=0, U'=free_17, V'=free_18, [ 30>=R && free_17>=1 && B>=1 && free_18>=1 ], cost: 1+2*B 197: [123] -> f230 : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F && 0>=-1+G ], cost: 5-K+H 200: [123] -> f230 : [ 0>=G ], cost: 1 195: [123] -> [80] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 196: [123] -> [81] : B'=1+G, E'=0, G'=-1+G, K'=1+H, [ G>=1 && F>=K && H>=1+F ], cost: 4-K+H 252: [123] -> [89] : B'=1+G, E'=free_83, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && 0>=1+free_12 ], cost: 3-K+F 254: [123] -> [90] : B'=1+G, E'=free_84, K'=1+F, [ G>=1 && F>=K && 1+F>=1+F && free_12>=1 ], cost: 3-K+F 111: [128] -> f156 : [ G>=1+F ], cost: 1 185: [128] -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: [128] -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: [128] -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: [128] -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 239: [128] -> [83] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 242: [128] -> [84] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 244: [129] -> [85] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 246: [129] -> [86] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F ], cost: 4-K+F 248: [129] -> [87] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 250: [129] -> [88] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F ], cost: 3-K+F 325: [129] -> [123] : B'=G, E'=free_11, G'=-1+G, [ G>=1 && G>=F && 0>=-1+G ], cost: 2 326: [129] -> [123] : [ 0>=G ], cost: 1 321: [129] -> [124] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && 0>=1+free_11 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 322: [129] -> [125] : B'=G, E'=free_11, G'=-1+G, K'=1+F, [ G>=1 && G>=F && F>=G && free_11>=1 && -1+G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 5-K+F 323: [129] -> [126] : K'=1+F, [ F>=1+G && 0>=1+E && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F 324: [129] -> [127] : K'=1+F, [ F>=1+G && E>=1 && G>=1 && F>=K && 1+F>=1+F && 1+F>=1+F ], cost: 4-K+F Applied chaining over branches and pruning: Start location: f0 359: f0 -> [128] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 360: f0 -> [128] : B'=1+G, C'=free_6+free_7, D'=0, E'=0, G'=1+G, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && free_6+free_7>=0 ], cost: 4 362: f0 -> [128] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 363: f0 -> [128] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 364: f0 -> [128] : C'=0, D'=0, E'=0, [], cost: 1 185: [128] -> [76] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 186: [128] -> [77] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 3+H-A 187: [128] -> [78] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 188: [128] -> [79] : A'=1+H, B'=1+G, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 3+H-A 239: [128] -> [83] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A 242: [128] -> [84] : A'=1+H, B'=1+G, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 3+H-A Applied chaining over branches and pruning: Start location: f0 383: f0 -> [76] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 4+H-A 384: f0 -> [77] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 4+H-A 385: f0 -> [78] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 4+H-A 386: f0 -> [79] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 4+H-A 387: f0 -> [83] : A'=1+H, B'=1+G, C'=0, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 4+H-A 388: f0 -> [84] : A'=1+H, B'=1+G, C'=0, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 4+H-A 365: f0 -> [130] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 366: f0 -> [131] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 367: f0 -> [132] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 368: f0 -> [133] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 369: f0 -> [134] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 370: f0 -> [135] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 371: f0 -> [136] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 372: f0 -> [137] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 373: f0 -> [138] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 374: f0 -> [139] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 375: f0 -> [140] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 376: f0 -> [141] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 377: f0 -> [142] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 378: f0 -> [143] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 379: f0 -> [144] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 380: f0 -> [145] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 381: f0 -> [146] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 382: f0 -> [147] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 383: f0 -> [76] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 4+H-A 384: f0 -> [77] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H ], cost: 4+H-A 385: f0 -> [78] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 4+H-A 386: f0 -> [79] : A'=1+H, B'=1+G, C'=0, D'=(1+H-A)*free, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && (1+H-A)*free>=1 && 1+H>=1+H ], cost: 4+H-A 387: f0 -> [83] : A'=1+H, B'=1+G, C'=0, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 4+H-A 388: f0 -> [84] : A'=1+H, B'=1+G, C'=0, D'=0, E'=0, Q'=0, J'=free, [ F>=G && H>=G && H>=A && 1+H>=1+H && (1+H-A)*free==0 ], cost: 4+H-A 365: f0 -> [130] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 366: f0 -> [131] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 367: f0 -> [132] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 368: f0 -> [133] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 369: f0 -> [134] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 370: f0 -> [135] : B'=1+F, C'=0, D'=0, E'=0, G'=1+F, Q'=0, M'=0, N'=free_6, O'=free_7, P'=free_6+free_7, [ G>=1+H && F>=G && 0>=1+free_6+free_7 ], cost: 4+3*F-3*G 371: f0 -> [136] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 372: f0 -> [137] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 373: f0 -> [138] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 374: f0 -> [139] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 375: f0 -> [140] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 376: f0 -> [141] : A'=1+H, B'=1+G, C'=free_9+free_8, D'=0, E'=0, F'=G, G'=1+G, Q'=0, J'=free, M'=0, N'=free_8, O'=free_9, P'=free_9+free_8, [ H>=G && H>=A && (1+H-A)*free==0 && H>=F && G==F && free_9+free_8>=0 ], cost: 6+H-A 377: f0 -> [142] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 378: f0 -> [143] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 379: f0 -> [144] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 380: f0 -> [145] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 381: f0 -> [146] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A 382: f0 -> [147] : A'=1+F, B'=1+G, C'=free_96+free_97, D'=0, E'=0, G'=1+G, Q'=0, J'=free, L'=free_3, M'=0, N'=free_96, O'=free_97, P'=free_96+free_97, [ H>=G && H>=A && (1+H-A)*free==0 && F>=1+G && F>=1+H && -free_3*(H-F)==0 && free_96+free_97>=0 ], cost: 7+F-A Computing complexity for remaining 24 transitions. Found configuration with infinitely models for cost: 4+H-A and guard: F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H: H: Pos, F: Pos, free: Neg, G: Pos, A: Neg, where: H > G F > G Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: F>=G && H>=G && H>=A && 0>=1+(1+H-A)*free && 1+H>=1+H Final Cost: 4+H-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),?)