Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f135 -> f136 : [ 0>=1+A ], cost: 1 1: f135 -> f136 : [ A>=1 ], cost: 1 45: f135 -> f146 : A'=0, W'=1, [ A==0 ], cost: 1 2: f136 -> f137 : [ 0>=1+B ], cost: 1 3: f136 -> f137 : [ B>=1 ], cost: 1 44: f136 -> f146 : B'=0, W'=1, [ B==0 ], cost: 1 41: f137 -> f146 : W'=0, [ 0>=1+F ], cost: 1 42: f137 -> f146 : W'=0, [ F>=1 ], cost: 1 43: f137 -> f146 : F'=0, W'=1, [ F==0 ], cost: 1 4: f0 -> f26 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, [], cost: 1 5: f26 -> f29 : Q'=0, [ D>=1+H ], cost: 1 63: f26 -> f38 : H'=0, [ H>=D ], cost: 1 62: f29 -> f26 : H'=1+H, [ Q>=D ], cost: 1 6: f29 -> f29 : Q'=1+Q, J'=free_2, [ D>=1+Q ], cost: 1 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 60: f41 -> f38 : H'=1+H, [ Q>=D ], cost: 1 12: f41 -> f41 : E'=0, Q'=1+Q, K'=0, [ D>=1+Q && E==0 ], cost: 1 8: f41 -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: f41 -> f44 : [ E>=1 && D>=1+Q ], cost: 1 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 57: f62 -> f59 : L'=1+L, [ M>=D ], cost: 1 20: f62 -> f62 : A'=0, M'=1+M, N'=0, [ D>=1+M && A==0 ], cost: 1 15: f62 -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: f62 -> f65 : [ D>=1+M && A>=1 ], cost: 1 17: f65 -> f62 : A'=1, M'=1+M, N'=1, [ free_3>=1+free_4 ], cost: 1 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 54: f83 -> f80 : O'=1+O, [ P>=D ], cost: 1 28: f83 -> f83 : B'=0, P'=1+P, Q_1'=0, [ D>=1+P && B==0 ], cost: 1 23: f83 -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: f83 -> f86 : [ D>=1+P && B>=1 ], cost: 1 25: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [ free_5>=1+free_6 ], cost: 1 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 51: f98 -> f135 : [ 0>=1+E && H>=C ], cost: 1 52: f98 -> f135 : [ E>=1 && H>=C ], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 53: f98 -> f146 : E'=0, W'=1, [ H>=C && E==0 ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 46: f113 -> f110 : T'=1+T, [ U>=C ], cost: 1 36: f113 -> f113 : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 40: f113 -> f113 : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 34: f113 -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: f113 -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 37: f117 -> f113 : F'=1, U'=1+U, V'=1, [ free_7>=1+free_8 ], cost: 1 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 Removing duplicate transition: 17. Removing duplicate transition: 25. Removing duplicate transition: 37. Simplified the transitions: Start location: f0 4: f0 -> f26 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, [], cost: 1 5: f26 -> f29 : Q'=0, [ D>=1+H ], cost: 1 63: f26 -> f38 : H'=0, [ H>=D ], cost: 1 62: f29 -> f26 : H'=1+H, [ Q>=D ], cost: 1 6: f29 -> f29 : Q'=1+Q, J'=free_2, [ D>=1+Q ], cost: 1 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 60: f41 -> f38 : H'=1+H, [ Q>=D ], cost: 1 12: f41 -> f41 : E'=0, Q'=1+Q, K'=0, [ D>=1+Q && E==0 ], cost: 1 8: f41 -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: f41 -> f44 : [ E>=1 && D>=1+Q ], cost: 1 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 57: f62 -> f59 : L'=1+L, [ M>=D ], cost: 1 20: f62 -> f62 : A'=0, M'=1+M, N'=0, [ D>=1+M && A==0 ], cost: 1 15: f62 -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: f62 -> f65 : [ D>=1+M && A>=1 ], cost: 1 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 54: f83 -> f80 : O'=1+O, [ P>=D ], cost: 1 28: f83 -> f83 : B'=0, P'=1+P, Q_1'=0, [ D>=1+P && B==0 ], cost: 1 23: f83 -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: f83 -> f86 : [ D>=1+P && B>=1 ], cost: 1 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 46: f113 -> f110 : T'=1+T, [ U>=C ], cost: 1 36: f113 -> f113 : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 40: f113 -> f113 : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 34: f113 -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: f113 -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 Eliminating 1 self-loops for location f29 Self-Loop 6 has the metering function: -Q+D, resulting in the new transition 64. Removing the self-loops: 6. Eliminating 1 self-loops for location f41 Self-Loop 12 has the metering function: -Q+D, resulting in the new transition 65. Removing the self-loops: 12. Eliminating 1 self-loops for location f62 Self-Loop 20 has the metering function: -M+D, resulting in the new transition 66. Removing the self-loops: 20. Eliminating 1 self-loops for location f83 Self-Loop 28 has the metering function: -P+D, resulting in the new transition 67. Removing the self-loops: 28. Eliminating 2 self-loops for location f113 Removing the self-loops: 36 40. Adding an epsilon transition (to model nonexecution of the loops): 70. Removed all Self-loops using metering functions (where possible): Start location: f0 4: f0 -> f26 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, [], cost: 1 5: f26 -> f29 : Q'=0, [ D>=1+H ], cost: 1 63: f26 -> f38 : H'=0, [ H>=D ], cost: 1 64: f29 -> [25] : Q'=D, J'=free_2, [ D>=1+Q ], cost: -Q+D 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 65: f41 -> [26] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 66: f62 -> [27] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 67: f83 -> [28] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 68: f113 -> [29] : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 69: f113 -> [29] : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 70: f113 -> [29] : [], cost: 0 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 62: [25] -> f26 : H'=1+H, [ Q>=D ], cost: 1 60: [26] -> f38 : H'=1+H, [ Q>=D ], cost: 1 8: [26] -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: [26] -> f44 : [ E>=1 && D>=1+Q ], cost: 1 57: [27] -> f59 : L'=1+L, [ M>=D ], cost: 1 15: [27] -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: [27] -> f65 : [ D>=1+M && A>=1 ], cost: 1 54: [28] -> f80 : O'=1+O, [ P>=D ], cost: 1 23: [28] -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: [28] -> f86 : [ D>=1+P && B>=1 ], cost: 1 46: [29] -> f110 : T'=1+T, [ U>=C ], cost: 1 34: [29] -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: [29] -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 Applied simple chaining: Start location: f0 4: f0 -> f26 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, [], cost: 1 5: f26 -> f26 : H'=1+H, Q'=D, J'=free_2, [ D>=1+H && D>=1 && D>=D ], cost: 2+D 63: f26 -> f38 : H'=0, [ H>=D ], cost: 1 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 65: f41 -> [26] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 66: f62 -> [27] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 67: f83 -> [28] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 68: f113 -> [29] : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 69: f113 -> [29] : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 70: f113 -> [29] : [], cost: 0 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 60: [26] -> f38 : H'=1+H, [ Q>=D ], cost: 1 8: [26] -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: [26] -> f44 : [ E>=1 && D>=1+Q ], cost: 1 57: [27] -> f59 : L'=1+L, [ M>=D ], cost: 1 15: [27] -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: [27] -> f65 : [ D>=1+M && A>=1 ], cost: 1 54: [28] -> f80 : O'=1+O, [ P>=D ], cost: 1 23: [28] -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: [28] -> f86 : [ D>=1+P && B>=1 ], cost: 1 46: [29] -> f110 : T'=1+T, [ U>=C ], cost: 1 34: [29] -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: [29] -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 Eliminating 1 self-loops for location f26 Self-Loop 5 has the metering function: -H+D, resulting in the new transition 71. Removing the self-loops: 5. Removed all Self-loops using metering functions (where possible): Start location: f0 4: f0 -> f26 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, [], cost: 1 71: f26 -> [30] : H'=D, Q'=D, J'=free_2, [ D>=1+H && D>=1 ], cost: -2*H-(H-D)*D+2*D 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 65: f41 -> [26] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 66: f62 -> [27] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 67: f83 -> [28] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 68: f113 -> [29] : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 69: f113 -> [29] : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 70: f113 -> [29] : [], cost: 0 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 60: [26] -> f38 : H'=1+H, [ Q>=D ], cost: 1 8: [26] -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: [26] -> f44 : [ E>=1 && D>=1+Q ], cost: 1 57: [27] -> f59 : L'=1+L, [ M>=D ], cost: 1 15: [27] -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: [27] -> f65 : [ D>=1+M && A>=1 ], cost: 1 54: [28] -> f80 : O'=1+O, [ P>=D ], cost: 1 23: [28] -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: [28] -> f86 : [ D>=1+P && B>=1 ], cost: 1 46: [29] -> f110 : T'=1+T, [ U>=C ], cost: 1 34: [29] -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: [29] -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 63: [30] -> f38 : H'=0, [ H>=D ], cost: 1 Applied simple chaining: Start location: f0 4: f0 -> f38 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 65: f41 -> [26] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 10: f44 -> f41 : E'=1, Q'=1+Q, K'=1, [], cost: 1 11: f44 -> f41 : E'=0, Q'=1+Q, K'=0, [], cost: 1 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 66: f62 -> [27] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 18: f65 -> f62 : A'=1, M'=1+M, N'=1, [], cost: 1 19: f65 -> f62 : A'=0, M'=1+M, N'=0, [], cost: 1 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 67: f83 -> [28] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 26: f86 -> f83 : B'=1, P'=1+P, Q_1'=1, [], cost: 1 27: f86 -> f83 : B'=0, P'=1+P, Q_1'=0, [], cost: 1 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 68: f113 -> [29] : U'=1+U, [ R*C+S>=U+C*T && C>=1+U ], cost: 1 69: f113 -> [29] : F'=0, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 ], cost: 1 70: f113 -> [29] : [], cost: 0 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 60: [26] -> f38 : H'=1+H, [ Q>=D ], cost: 1 8: [26] -> f44 : [ 0>=1+E && D>=1+Q ], cost: 1 9: [26] -> f44 : [ E>=1 && D>=1+Q ], cost: 1 57: [27] -> f59 : L'=1+L, [ M>=D ], cost: 1 15: [27] -> f65 : [ D>=1+M && 0>=1+A ], cost: 1 16: [27] -> f65 : [ D>=1+M && A>=1 ], cost: 1 54: [28] -> f80 : O'=1+O, [ P>=D ], cost: 1 23: [28] -> f86 : [ D>=1+P && 0>=1+B ], cost: 1 24: [28] -> f86 : [ D>=1+P && B>=1 ], cost: 1 46: [29] -> f110 : T'=1+T, [ U>=C ], cost: 1 34: [29] -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 35: [29] -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 Applied chaining over branches and pruning: Start location: f0 4: f0 -> f38 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free 7: f38 -> f41 : Q'=0, [ D>=1+H ], cost: 1 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 72: f41 -> f38 : E'=0, H'=1+H, Q'=D, K'=0, [ D>=1+Q && E==0 && D>=D ], cost: 1-Q+D 73: f41 -> [31] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 74: f41 -> [32] : E'=0, Q'=D, K'=0, [ D>=1+Q && E==0 ], cost: -Q+D 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 14: f59 -> f62 : M'=1+L, [ D>=2+L ], cost: 1 75: f62 -> f59 : A'=0, L'=1+L, M'=D, N'=0, [ D>=1+M && A==0 && D>=D ], cost: 1-M+D 76: f62 -> [33] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 77: f62 -> [34] : A'=0, M'=D, N'=0, [ D>=1+M && A==0 ], cost: -M+D 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 22: f80 -> f83 : P'=1+O, [ D>=2+O ], cost: 1 78: f83 -> f80 : B'=0, O'=1+O, P'=D, Q_1'=0, [ D>=1+P && B==0 && D>=D ], cost: 1-P+D 79: f83 -> [35] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 80: f83 -> [36] : B'=0, P'=D, Q_1'=0, [ D>=1+P && B==0 ], cost: -P+D 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 81: f113 -> f110 : T'=1+T, U'=1+U, [ R*C+S>=U+C*T && C>=1+U && 1+U>=C ], cost: 2 84: f113 -> f110 : F'=0, T'=1+T, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 && 1+U>=C ], cost: 2 85: f113 -> f110 : T'=1+T, [ U>=C ], cost: 1 82: f113 -> f117 : U'=1+U, [ R*C+S>=U+C*T && C>=1+U && 0>=1+F && 1+U+C*T>=1+R*C+S && C>=2+U ], cost: 2 83: f113 -> f117 : U'=1+U, [ R*C+S>=U+C*T && C>=1+U && F>=1 && 1+U+C*T>=1+R*C+S && C>=2+U ], cost: 2 86: f113 -> f117 : [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 87: f113 -> f117 : [ F>=1 && U+C*T>=1+R*C+S && C>=1+U ], cost: 1 38: f117 -> f113 : F'=1, U'=1+U, V'=1, [], cost: 1 39: f117 -> f113 : F'=0, U'=1+U, V'=0, [], cost: 1 Applied chaining over branches and pruning: Start location: f0 4: f0 -> f38 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free 88: f38 -> f38 : E'=0, H'=1+H, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 && D>=D ], cost: 2+D 61: f38 -> f56 : H'=0, [ H>=D ], cost: 1 89: f38 -> [31] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 90: f38 -> [32] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 58: f59 -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 91: f59 -> f59 : A'=0, L'=1+L, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 && D>=D ], cost: 1-L+D 92: f59 -> [33] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 93: f59 -> [34] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 55: f80 -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 94: f80 -> f80 : B'=0, O'=1+O, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 && D>=D ], cost: 1-O+D 95: f80 -> [35] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 96: f80 -> [36] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 81: f113 -> f110 : T'=1+T, U'=1+U, [ R*C+S>=U+C*T && C>=1+U && 1+U>=C ], cost: 2 84: f113 -> f110 : F'=0, T'=1+T, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 && 1+U>=C ], cost: 2 85: f113 -> f110 : T'=1+T, [ U>=C ], cost: 1 97: f113 -> f113 : F'=1, U'=2+U, V'=1, [ R*C+S>=U+C*T && C>=1+U && 0>=1+F && 1+U+C*T>=1+R*C+S && C>=2+U ], cost: 3 98: f113 -> f113 : F'=0, U'=2+U, V'=0, [ R*C+S>=U+C*T && C>=1+U && 0>=1+F && 1+U+C*T>=1+R*C+S && C>=2+U ], cost: 3 100: f113 -> f113 : F'=0, U'=2+U, V'=0, [ R*C+S>=U+C*T && C>=1+U && F>=1 && 1+U+C*T>=1+R*C+S && C>=2+U ], cost: 3 101: f113 -> f113 : F'=1, U'=1+U, V'=1, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 102: f113 -> f113 : F'=0, U'=1+U, V'=0, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 Eliminating 1 self-loops for location f38 Self-Loop 88 has the metering function: -H+D, resulting in the new transition 105. Removing the self-loops: 88. Eliminating 1 self-loops for location f59 Self-Loop 91 has the metering function: -1-L+D, resulting in the new transition 106. Removing the self-loops: 91. Eliminating 1 self-loops for location f80 Self-Loop 94 has the metering function: -1-O+D, resulting in the new transition 107. Removing the self-loops: 94. Eliminating 5 self-loops for location f113 Removing the self-loops: 97 98 100 101 102. Adding an epsilon transition (to model nonexecution of the loops): 113. Removed all Self-loops using metering functions (where possible): Start location: f0 4: f0 -> f38 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free 105: f38 -> [37] : E'=0, H'=D, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: -2*H-(H-D)*D+2*D 13: f56 -> f59 : L'=0, [ D>=1+H ], cost: 1 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 106: f59 -> [38] : A'=0, L'=-1+D, M'=D, N'=0, [ D>=2+L && A==0 ], cost: -3/2-3/2*L-(1+L-D)*D-1/2*(1+L-D)^2+3/2*D+(1+L-D)*L 21: f77 -> f80 : O'=0, [ D>=1+Q ], cost: 1 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 107: f80 -> [39] : B'=0, O'=-1+D, P'=D, Q_1'=0, [ D>=2+O && B==0 ], cost: -3/2-1/2*(1+O-D)^2+O*(1+O-D)-D*(1+O-D)-3/2*O+3/2*D 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 108: f113 -> [40] : F'=1, U'=2+U, V'=1, [ -R*C+U-S+C*T==0 && 0>=1+F && C>=2+U ], cost: 3 109: f113 -> [40] : F'=0, U'=2+U, V'=0, [ -R*C+U-S+C*T==0 && 0>=1+F && C>=2+U ], cost: 3 110: f113 -> [40] : F'=0, U'=2+U, V'=0, [ -R*C+U-S+C*T==0 && F>=1 && C>=2+U ], cost: 3 111: f113 -> [40] : F'=1, U'=1+U, V'=1, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 112: f113 -> [40] : F'=0, U'=1+U, V'=0, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 113: f113 -> [40] : [], cost: 0 61: [37] -> f56 : H'=0, [ H>=D ], cost: 1 89: [37] -> [31] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 90: [37] -> [32] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 58: [38] -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 92: [38] -> [33] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 93: [38] -> [34] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 55: [39] -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 95: [39] -> [35] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 96: [39] -> [36] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 81: [40] -> f110 : T'=1+T, U'=1+U, [ R*C+S>=U+C*T && C>=1+U && 1+U>=C ], cost: 2 84: [40] -> f110 : F'=0, T'=1+T, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 && 1+U>=C ], cost: 2 85: [40] -> f110 : T'=1+T, [ U>=C ], cost: 1 Applied simple chaining: Start location: f0 4: f0 -> f38 : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free 105: f38 -> [37] : E'=0, H'=D, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: -2*H-(H-D)*D+2*D 59: f56 -> f77 : Q'=0, [ H>=D ], cost: 1 13: f56 -> [38] : A'=0, L'=-1+D, M'=D, N'=0, [ D>=1+H && D>=2 && A==0 ], cost: -1/2+(-1+D)*D-1/2*(-1+D)^2+3/2*D 56: f77 -> f98 : H'=0, [ Q>=D ], cost: 1 21: f77 -> [39] : B'=0, O'=-1+D, P'=D, Q_1'=0, [ D>=1+Q && D>=2 && B==0 ], cost: -1/2+(-1+D)*D-1/2*(-1+D)^2+3/2*D 29: f98 -> f101 : Q'=0, [ C>=1+H ], cost: 1 50: f101 -> f98 : H'=1+H, [ Q>=C ], cost: 1 30: f101 -> f104 : R'=0, [ C>=1+Q ], cost: 1 49: f104 -> f101 : Q'=1+Q, [ R>=C ], cost: 1 31: f104 -> f107 : S'=0, [ C>=1+R ], cost: 1 48: f107 -> f104 : R'=1+R, [ S>=C ], cost: 1 32: f107 -> f110 : T'=0, [ C>=1+S ], cost: 1 47: f110 -> f107 : S'=1+S, [ T>=C ], cost: 1 33: f110 -> f113 : U'=0, [ C>=1+T ], cost: 1 108: f113 -> [40] : F'=1, U'=2+U, V'=1, [ -R*C+U-S+C*T==0 && 0>=1+F && C>=2+U ], cost: 3 109: f113 -> [40] : F'=0, U'=2+U, V'=0, [ -R*C+U-S+C*T==0 && 0>=1+F && C>=2+U ], cost: 3 110: f113 -> [40] : F'=0, U'=2+U, V'=0, [ -R*C+U-S+C*T==0 && F>=1 && C>=2+U ], cost: 3 111: f113 -> [40] : F'=1, U'=1+U, V'=1, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 112: f113 -> [40] : F'=0, U'=1+U, V'=0, [ 0>=1+F && U+C*T>=1+R*C+S && C>=1+U ], cost: 2 113: f113 -> [40] : [], cost: 0 61: [37] -> f56 : H'=0, [ H>=D ], cost: 1 89: [37] -> [31] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 90: [37] -> [32] : E'=0, Q'=D, K'=0, [ D>=1+H && D>=1 && E==0 ], cost: 1+D 58: [38] -> f56 : H'=1+H, [ 1+L>=D ], cost: 1 92: [38] -> [33] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 93: [38] -> [34] : A'=0, M'=D, N'=0, [ D>=2+L && D>=2+L && A==0 ], cost: -L+D 55: [39] -> f77 : Q'=1+Q, [ 1+O>=D ], cost: 1 95: [39] -> [35] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 96: [39] -> [36] : B'=0, P'=D, Q_1'=0, [ D>=2+O && D>=2+O && B==0 ], cost: -O+D 81: [40] -> f110 : T'=1+T, U'=1+U, [ R*C+S>=U+C*T && C>=1+U && 1+U>=C ], cost: 2 84: [40] -> f110 : F'=0, T'=1+T, U'=1+U, V'=0, [ U+C*T>=1+R*C+S && C>=1+U && F==0 && 1+U>=C ], cost: 2 85: [40] -> f110 : T'=1+T, [ U>=C ], cost: 1 Applied chaining over branches and pruning: Start location: f0 114: f0 -> [41] : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 114: f0 -> [41] : A'=1, B'=1, C'=3, D'=free, E'=1, F'=1, G'=free_1, H'=0, Q'=free, J'=free_2, [ free>=1 && free>=1 && free>=free ], cost: 2+free^2+2*free Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: 2+free^2+2*free and guard: free>=1 && free>=1 && free>=free: free: Pos Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: free>=1 && free>=1 && free>=free Final Cost: 2+free^2+2*free Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)