Trying to load file: main.koat Initial Control flow graph problem: Start location: f2 0: f48 -> f52 : [ A>=1 ], cost: 1 20: f48 -> f52 : [ B>=1 && 0>=A ], cost: 1 19: f48 -> f46 : P'=2, [ 0>=B && 0>=A ], cost: 1 1: f52 -> f46 : [ 0>=B ], cost: 1 21: f52 -> f46 : P'=3, [ B>=1 ], cost: 1 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 3: f10 -> f14 : H'=1, [ D>=1+G && 0>=G ], cost: 1 4: f10 -> f14 : H'=0, [ D>=1+G && G>=1 ], cost: 1 35: f10 -> f1 : [ G>=D ], cost: 1 5: f14 -> f23 : J'=1, K'=L, [ Q>=0 && 1+G>=D && 1>=Q ], cost: 1 6: f14 -> f23 : J'=0, K'=L, [ Q>=0 && D>=2+G && 1>=Q ], cost: 1 7: f23 -> f27 : E'=1+E, [ Q>=1 && 0>=C && 0>=E ], cost: 1 8: f23 -> f27 : E'=1+E, [ Q>=1 && 0>=C && E==1 ], cost: 1 9: f23 -> f27 : E'=0, F'=1+F, [ E>=2 && C==0 ], cost: 1 10: f23 -> f27 : C'=-1+C, [ C>=1 ], cost: 1 32: f27 -> f23 : [ D>=F && Q==0 ], cost: 1 11: f27 -> f42 : A'=H, B'=J, M'=1, N'=K, [ M>=1 && Q>=1 ], cost: 1 12: f27 -> f42 : A'=H, B'=J, M'=1, N'=K, O'=K, [ 0>=M && Q>=1 ], cost: 1 15: f42 -> f48 : A'=0, O'=N, [ A==0 && N==O ], cost: 1 13: f42 -> f44 : O'=N, [ 0>=1+A && N==O ], cost: 1 14: f42 -> f44 : O'=N, [ A>=1 && N==O ], cost: 1 22: f42 -> f59 : [ Q_1>=0 && N>=1+O && 1>=Q_1 ], cost: 1 23: f42 -> f59 : [ Q_1>=0 && O>=1+N && 1>=Q_1 ], cost: 1 17: f44 -> f48 : [ 0>=1+B ], cost: 1 18: f44 -> f48 : [ B>=1 ], cost: 1 16: f44 -> f46 : B'=0, P'=1, [ B==0 ], cost: 1 26: f59 -> f63 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E ], cost: 1 27: f59 -> f63 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 ], cost: 1 28: f59 -> f63 : E'=0, F'=1+F, [ E>=2 && C==0 ], cost: 1 29: f59 -> f63 : C'=-1+C, [ C>=1 ], cost: 1 33: f63 -> f10 : G'=1+G, L'=0, Q_1'=1, [ L>=1 && D>=F && Q_1==1 ], cost: 1 34: f63 -> f10 : G'=1+G, L'=1, Q_1'=1, [ 0>=L && D>=F && Q_1==1 ], cost: 1 30: f63 -> f23 : [ Q>=0 && 1>=Q && 0>=Q_1 && D>=F ], cost: 1 31: f63 -> f23 : [ Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 1 Simplified the transitions: Start location: f2 0: f48 -> f52 : [ A>=1 ], cost: 1 20: f48 -> f52 : [ B>=1 && 0>=A ], cost: 1 19: f48 -> f46 : P'=2, [ 0>=B && 0>=A ], cost: 1 1: f52 -> f46 : [ 0>=B ], cost: 1 21: f52 -> f46 : P'=3, [ B>=1 ], cost: 1 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 3: f10 -> f14 : H'=1, [ D>=1+G && 0>=G ], cost: 1 4: f10 -> f14 : H'=0, [ D>=1+G && G>=1 ], cost: 1 5: f14 -> f23 : J'=1, K'=L, [ Q>=0 && 1+G>=D && 1>=Q ], cost: 1 6: f14 -> f23 : J'=0, K'=L, [ Q>=0 && D>=2+G && 1>=Q ], cost: 1 7: f23 -> f27 : E'=1+E, [ Q>=1 && 0>=C && 0>=E ], cost: 1 8: f23 -> f27 : E'=1+E, [ Q>=1 && 0>=C && E==1 ], cost: 1 9: f23 -> f27 : E'=0, F'=1+F, [ E>=2 && C==0 ], cost: 1 10: f23 -> f27 : C'=-1+C, [ C>=1 ], cost: 1 32: f27 -> f23 : [ D>=F && Q==0 ], cost: 1 11: f27 -> f42 : A'=H, B'=J, M'=1, N'=K, [ M>=1 && Q>=1 ], cost: 1 12: f27 -> f42 : A'=H, B'=J, M'=1, N'=K, O'=K, [ 0>=M && Q>=1 ], cost: 1 15: f42 -> f48 : A'=0, O'=N, [ A==0 && N==O ], cost: 1 13: f42 -> f44 : O'=N, [ 0>=1+A && N==O ], cost: 1 14: f42 -> f44 : O'=N, [ A>=1 && N==O ], cost: 1 22: f42 -> f59 : [ Q_1>=0 && N>=1+O && 1>=Q_1 ], cost: 1 23: f42 -> f59 : [ Q_1>=0 && O>=1+N && 1>=Q_1 ], cost: 1 17: f44 -> f48 : [ 0>=1+B ], cost: 1 18: f44 -> f48 : [ B>=1 ], cost: 1 16: f44 -> f46 : B'=0, P'=1, [ B==0 ], cost: 1 26: f59 -> f63 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E ], cost: 1 27: f59 -> f63 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 ], cost: 1 28: f59 -> f63 : E'=0, F'=1+F, [ E>=2 && C==0 ], cost: 1 29: f59 -> f63 : C'=-1+C, [ C>=1 ], cost: 1 33: f63 -> f10 : G'=1+G, L'=0, Q_1'=1, [ L>=1 && D>=F && Q_1==1 ], cost: 1 34: f63 -> f10 : G'=1+G, L'=1, Q_1'=1, [ 0>=L && D>=F && Q_1==1 ], cost: 1 30: f63 -> f23 : [ Q>=0 && 1>=Q && 0>=Q_1 && D>=F ], cost: 1 31: f63 -> f23 : [ Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 1 Applied chaining over branches and pruning: Start location: f2 19: f48 -> f46 : P'=2, [ 0>=B && 0>=A ], cost: 1 56: f48 -> f46 : [ A>=1 && 0>=B ], cost: 2 57: f48 -> f46 : P'=3, [ A>=1 && B>=1 ], cost: 2 58: f48 -> f46 : P'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 44: f23 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && D>=1+F && Q==0 ], cost: 2 47: f23 -> f23 : C'=-1+C, [ C>=1 && D>=F && Q==0 ], cost: 2 40: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 ], cost: 2 41: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && 0>=E && 0>=M && Q>=1 ], cost: 2 43: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && E==1 && 0>=M && Q>=1 ], cost: 2 45: f23 -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 ], cost: 2 46: f23 -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, O'=K, [ E>=2 && C==0 && 0>=M && Q>=1 ], cost: 2 15: f42 -> f48 : A'=0, O'=N, [ A==0 && N==O ], cost: 1 50: f42 -> f48 : O'=N, [ 0>=1+A && N==O && 0>=1+B ], cost: 2 51: f42 -> f48 : O'=N, [ 0>=1+A && N==O && B>=1 ], cost: 2 53: f42 -> f48 : O'=N, [ A>=1 && N==O && 0>=1+B ], cost: 2 54: f42 -> f48 : O'=N, [ A>=1 && N==O && B>=1 ], cost: 2 52: f42 -> f46 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2 55: f42 -> f46 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2 22: f42 -> f59 : [ Q_1>=0 && N>=1+O && 1>=Q_1 ], cost: 1 23: f42 -> f59 : [ Q_1>=0 && O>=1+N && 1>=Q_1 ], cost: 1 59: f59 -> f10 : E'=1+E, G'=1+G, L'=0, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && L>=1 && D>=F && Q_1==1 ], cost: 2 60: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && 0>=L && D>=F && Q_1==1 ], cost: 2 63: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && E==1 && 0>=L && D>=F && Q_1==1 ], cost: 2 65: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=0, Q_1'=1, [ E>=2 && C==0 && L>=1 && D>=1+F && Q_1==1 ], cost: 2 66: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=1, Q_1'=1, [ E>=2 && C==0 && 0>=L && D>=1+F && Q_1==1 ], cost: 2 61: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 64: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 67: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && 0>=Q_1 && D>=1+F ], cost: 2 68: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && Q_1>=2 && D>=1+F ], cost: 2 72: f59 -> f23 : C'=-1+C, [ C>=1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 Eliminating 2 self-loops for location f23 Self-Loop 47 has the metering function: C, resulting in the new transition 74. Removing the self-loops: 44 47. Adding an epsilon transition (to model nonexecution of the loops): 75. Removed all Self-loops using metering functions (where possible): Start location: f2 19: f48 -> f46 : P'=2, [ 0>=B && 0>=A ], cost: 1 56: f48 -> f46 : [ A>=1 && 0>=B ], cost: 2 57: f48 -> f46 : P'=3, [ A>=1 && B>=1 ], cost: 2 58: f48 -> f46 : P'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 73: f23 -> [13] : E'=0, F'=1+F, [ E>=2 && C==0 && D>=1+F && Q==0 ], cost: 2 74: f23 -> [13] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 75: f23 -> [13] : [], cost: 0 15: f42 -> f48 : A'=0, O'=N, [ A==0 && N==O ], cost: 1 50: f42 -> f48 : O'=N, [ 0>=1+A && N==O && 0>=1+B ], cost: 2 51: f42 -> f48 : O'=N, [ 0>=1+A && N==O && B>=1 ], cost: 2 53: f42 -> f48 : O'=N, [ A>=1 && N==O && 0>=1+B ], cost: 2 54: f42 -> f48 : O'=N, [ A>=1 && N==O && B>=1 ], cost: 2 52: f42 -> f46 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2 55: f42 -> f46 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2 22: f42 -> f59 : [ Q_1>=0 && N>=1+O && 1>=Q_1 ], cost: 1 23: f42 -> f59 : [ Q_1>=0 && O>=1+N && 1>=Q_1 ], cost: 1 59: f59 -> f10 : E'=1+E, G'=1+G, L'=0, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && L>=1 && D>=F && Q_1==1 ], cost: 2 60: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && 0>=L && D>=F && Q_1==1 ], cost: 2 63: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && E==1 && 0>=L && D>=F && Q_1==1 ], cost: 2 65: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=0, Q_1'=1, [ E>=2 && C==0 && L>=1 && D>=1+F && Q_1==1 ], cost: 2 66: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=1, Q_1'=1, [ E>=2 && C==0 && 0>=L && D>=1+F && Q_1==1 ], cost: 2 61: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 64: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 67: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && 0>=Q_1 && D>=1+F ], cost: 2 68: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && Q_1>=2 && D>=1+F ], cost: 2 72: f59 -> f23 : C'=-1+C, [ C>=1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 40: [13] -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 ], cost: 2 41: [13] -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && 0>=E && 0>=M && Q>=1 ], cost: 2 43: [13] -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && E==1 && 0>=M && Q>=1 ], cost: 2 45: [13] -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 ], cost: 2 46: [13] -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, O'=K, [ E>=2 && C==0 && 0>=M && Q>=1 ], cost: 2 Applied chaining over branches and pruning: Start location: f2 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 81: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 ], cost: 2 82: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && 0>=E && 0>=M && Q>=1 ], cost: 2 83: f23 -> f42 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, [ Q>=1 && 0>=C && E==1 && 0>=M && Q>=1 ], cost: 2 84: f23 -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 ], cost: 2 85: f23 -> f42 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, O'=K, [ E>=2 && C==0 && 0>=M && Q>=1 ], cost: 2 76: f23 -> [14] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 77: f23 -> [15] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 78: f23 -> [16] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 79: f23 -> [17] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 80: f23 -> [18] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 52: f42 -> f46 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2 55: f42 -> f46 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2 87: f42 -> f46 : A'=0, O'=N, P'=3, [ A==0 && N==O && B>=1 && 0>=0 && B>=1 ], cost: 3 88: f42 -> f46 : O'=N, P'=2, [ 0>=1+A && N==O && 0>=1+B && 0>=B && 0>=A ], cost: 3 89: f42 -> f46 : O'=N, P'=3, [ 0>=1+A && N==O && B>=1 && B>=1 && 0>=A && B>=1 ], cost: 4 22: f42 -> f59 : [ Q_1>=0 && N>=1+O && 1>=Q_1 ], cost: 1 23: f42 -> f59 : [ Q_1>=0 && O>=1+N && 1>=Q_1 ], cost: 1 59: f59 -> f10 : E'=1+E, G'=1+G, L'=0, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && L>=1 && D>=F && Q_1==1 ], cost: 2 60: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && 0>=L && D>=F && Q_1==1 ], cost: 2 63: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && E==1 && 0>=L && D>=F && Q_1==1 ], cost: 2 65: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=0, Q_1'=1, [ E>=2 && C==0 && L>=1 && D>=1+F && Q_1==1 ], cost: 2 66: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=1, Q_1'=1, [ E>=2 && C==0 && 0>=L && D>=1+F && Q_1==1 ], cost: 2 61: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 64: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 67: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && 0>=Q_1 && D>=1+F ], cost: 2 68: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && Q_1>=2 && D>=1+F ], cost: 2 72: f59 -> f23 : C'=-1+C, [ C>=1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 Applied chaining over branches and pruning: Start location: f2 24: f46 -> f59 : O'=0, [ Q_1>=0 && O>=1 && 1>=Q_1 ], cost: 1 25: f46 -> f59 : O'=1, [ Q_1>=0 && 0>=O && 1>=Q_1 ], cost: 1 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 92: f23 -> f46 : A'=H, B'=0, E'=1+E, M'=1, N'=K, O'=K, P'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && 0>=1+H && K==O && J==0 ], cost: 4 93: f23 -> f46 : A'=H, B'=0, E'=1+E, M'=1, N'=K, O'=K, P'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && H>=1 && K==O && J==0 ], cost: 4 95: f23 -> f46 : A'=H, B'=J, E'=1+E, M'=1, N'=K, O'=K, P'=2, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && 0>=1+H && K==O && 0>=1+J && 0>=J && 0>=H ], cost: 5 101: f23 -> f46 : A'=0, B'=J, E'=1+E, M'=1, N'=K, O'=K, P'=3, [ Q>=1 && 0>=C && 0>=E && 0>=M && Q>=1 && H==0 && K==K && J>=1 && 0>=0 && J>=1 ], cost: 5 106: f23 -> f46 : A'=0, B'=J, E'=1+E, M'=1, N'=K, O'=K, P'=3, [ Q>=1 && 0>=C && E==1 && 0>=M && Q>=1 && H==0 && K==K && J>=1 && 0>=0 && J>=1 ], cost: 5 97: f23 -> f59 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && K>=1+O && 1>=Q_1 ], cost: 3 98: f23 -> f59 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 ], cost: 3 114: f23 -> f59 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && K>=1+O && 1>=Q_1 ], cost: 3 115: f23 -> f59 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 ], cost: 3 76: f23 -> [14] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 77: f23 -> [15] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 78: f23 -> [16] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 79: f23 -> [17] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 80: f23 -> [18] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 59: f59 -> f10 : E'=1+E, G'=1+G, L'=0, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && L>=1 && D>=F && Q_1==1 ], cost: 2 60: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && 0>=L && D>=F && Q_1==1 ], cost: 2 63: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && E==1 && 0>=L && D>=F && Q_1==1 ], cost: 2 65: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=0, Q_1'=1, [ E>=2 && C==0 && L>=1 && D>=1+F && Q_1==1 ], cost: 2 66: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=1, Q_1'=1, [ E>=2 && C==0 && 0>=L && D>=1+F && Q_1==1 ], cost: 2 61: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 64: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 67: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && 0>=Q_1 && D>=1+F ], cost: 2 68: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && Q_1>=2 && D>=1+F ], cost: 2 72: f59 -> f23 : C'=-1+C, [ C>=1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 Applied chaining over branches and pruning: Start location: f2 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 97: f23 -> f59 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && K>=1+O && 1>=Q_1 ], cost: 3 98: f23 -> f59 : A'=H, B'=J, E'=1+E, M'=1, N'=K, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 ], cost: 3 115: f23 -> f59 : A'=H, B'=J, E'=0, F'=1+F, M'=1, N'=K, [ E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 ], cost: 3 123: f23 -> f59 : A'=H, B'=0, E'=1+E, M'=1, N'=K, O'=0, P'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && H>=1 && K==O && J==0 && Q_1>=0 && K>=1 && 1>=Q_1 ], cost: 5 124: f23 -> f59 : A'=H, B'=0, E'=1+E, M'=1, N'=K, O'=1, P'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && H>=1 && K==O && J==0 && Q_1>=0 && 0>=K && 1>=Q_1 ], cost: 5 76: f23 -> [14] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 77: f23 -> [15] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 78: f23 -> [16] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 79: f23 -> [17] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 80: f23 -> [18] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 59: f59 -> f10 : E'=1+E, G'=1+G, L'=0, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && L>=1 && D>=F && Q_1==1 ], cost: 2 60: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && 0>=E && 0>=L && D>=F && Q_1==1 ], cost: 2 63: f59 -> f10 : E'=1+E, G'=1+G, L'=1, Q_1'=1, [ Q_1>=1 && 0>=C && E==1 && 0>=L && D>=F && Q_1==1 ], cost: 2 65: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=0, Q_1'=1, [ E>=2 && C==0 && L>=1 && D>=1+F && Q_1==1 ], cost: 2 66: f59 -> f10 : E'=0, F'=1+F, G'=1+G, L'=1, Q_1'=1, [ E>=2 && C==0 && 0>=L && D>=1+F && Q_1==1 ], cost: 2 61: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && 0>=E && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 64: f59 -> f23 : E'=1+E, [ Q_1>=1 && 0>=C && E==1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 67: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && 0>=Q_1 && D>=1+F ], cost: 2 68: f59 -> f23 : E'=0, F'=1+F, [ E>=2 && C==0 && Q>=0 && 1>=Q && Q_1>=2 && D>=1+F ], cost: 2 72: f59 -> f23 : C'=-1+C, [ C>=1 && Q>=0 && 1>=Q && Q_1>=2 && D>=F ], cost: 2 Applied chaining over branches and pruning: Start location: f2 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 36: f10 -> f23 : H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 37: f10 -> f23 : H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q ], cost: 2 38: f10 -> f23 : H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q ], cost: 2 39: f10 -> f23 : H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q ], cost: 2 131: f23 -> f10 : A'=H, B'=J, E'=2+E, G'=1+G, L'=0, M'=1, N'=K, Q_1'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && K>=1+O && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 5 132: f23 -> f10 : A'=H, B'=J, E'=2+E, G'=1+G, L'=1, M'=1, N'=K, Q_1'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && K>=1+O && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && 0>=L && D>=F && Q_1==1 ], cost: 5 134: f23 -> f10 : A'=H, B'=J, E'=2+E, G'=1+G, L'=0, M'=1, N'=K, Q_1'=1, [ Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 5 137: f23 -> f10 : A'=H, B'=J, E'=1, F'=1+F, G'=1+G, L'=0, M'=1, N'=K, Q_1'=1, [ E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=0 && L>=1 && D>=1+F && Q_1==1 ], cost: 5 138: f23 -> f10 : A'=H, B'=J, E'=1, F'=1+F, G'=1+G, L'=1, M'=1, N'=K, Q_1'=1, [ E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && O>=1+K && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=0 && 0>=L && D>=1+F && Q_1==1 ], cost: 5 76: f23 -> [14] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 77: f23 -> [15] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 78: f23 -> [16] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 79: f23 -> [17] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C 80: f23 -> [18] : C'=0, [ C>=1 && D>=F && Q==0 ], cost: 2*C Applied chaining over branches and pruning: Start location: f2 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 145: f10 -> f10 : A'=1, B'=1, E'=2+E, G'=1+G, H'=1, J'=1, K'=L, L'=0, M'=1, N'=L, Q_1'=1, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && L>=1+O && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 7 146: f10 -> f10 : A'=1, B'=1, E'=2+E, G'=1+G, H'=1, J'=1, K'=L, L'=1, M'=1, N'=L, Q_1'=1, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && L>=1+O && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && 0>=L && D>=F && Q_1==1 ], cost: 7 148: f10 -> f10 : A'=1, B'=1, E'=1, F'=1+F, G'=1+G, H'=1, J'=1, K'=L, L'=0, M'=1, N'=L, Q_1'=1, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && E>=2 && C==0 && M>=1 && Q>=1 && Q_1>=0 && O>=1+L && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=0 && L>=1 && D>=1+F && Q_1==1 ], cost: 7 157: f10 -> f10 : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, J'=0, K'=L, L'=0, M'=1, N'=L, Q_1'=1, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && O>=1+L && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 7 165: f10 -> f10 : A'=0, B'=1, E'=2+E, G'=1+G, H'=0, J'=1, K'=L, L'=0, M'=1, N'=L, Q_1'=1, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && Q>=1 && 0>=C && 0>=E && M>=1 && Q>=1 && Q_1>=0 && L>=1+O && 1>=Q_1 && Q_1>=1 && 0>=C && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 7 150: f10 -> [14] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 160: f10 -> [14] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 170: f10 -> [14] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 180: f10 -> [14] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 151: f10 -> [15] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 161: f10 -> [15] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 171: f10 -> [15] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 181: f10 -> [15] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 152: f10 -> [16] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 162: f10 -> [16] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 172: f10 -> [16] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 182: f10 -> [16] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 153: f10 -> [17] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 163: f10 -> [17] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 173: f10 -> [17] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 183: f10 -> [17] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 154: f10 -> [18] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 164: f10 -> [18] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 174: f10 -> [18] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 184: f10 -> [18] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C Eliminating 5 self-loops for location f10 Self-Loop 145 has the metering function: -1-G+D, resulting in the new transition 185. Self-Loop 146 has the metering function: -1-G+D, resulting in the new transition 186. Self-Loop 148 has the metering function: -1-G+D, resulting in the new transition 187. Self-Loop 165 has the metering function: -1-G+D, resulting in the new transition 191. Found this metering function when nesting loops: -1/2-G+D, Found this metering function when nesting loops: -1/2-G+D, Removing the self-loops: 145 146 148 157 165 188 189. Adding an epsilon transition (to model nonexecution of the loops): 192. Removed all Self-loops using metering functions (where possible): Start location: f2 2: f2 -> f10 : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 185: f10 -> [19] : A'=1, B'=1, E'=-2+E-2*G+2*D, G'=-1+D, H'=1, J'=1, K'=0, L'=0, M'=1, N'=0, Q_1'=1, [ 1+G-D==0 && 0>=G && -1+Q==0 && 0>=C && M>=1 && L>=1+O && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: -7-7*G+7*D 186: f10 -> [19] : A'=1, B'=1, E'=-2+E-2*G+2*D, G'=-1+D, H'=1, J'=1, K'=1, L'=1, M'=1, N'=1, Q_1'=1, [ 1+G-D==0 && 0>=G && -1+Q==0 && 0>=C && M>=1 && L>=1+O && 0>=1+E && 0>=L && D>=F && Q_1==1 ], cost: -7-7*G+7*D 187: f10 -> [19] : A'=1, B'=1, E'=1, F'=-1+F-G+D, G'=-1+D, H'=1, J'=1, K'=0, L'=0, M'=1, N'=0, Q_1'=1, [ 1+G-D==0 && 0>=G && -1+Q==0 && E>=2 && C==0 && M>=1 && O>=1+L && L>=1 && D>=1+F && Q_1==1 ], cost: -7-7*G+7*D 190: f10 -> [19] : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, J'=0, K'=L, L'=0, M'=1, N'=L, Q_1'=1, [ 0>=G && D>=2+G && -1+Q==0 && 0>=C && M>=1 && O>=1+L && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: 7 191: f10 -> [19] : A'=0, B'=1, E'=-2+E-2*G+2*D, G'=-1+D, H'=0, J'=1, K'=0, L'=0, M'=1, N'=0, Q_1'=1, [ 1+G-D==0 && G>=1 && -1+Q==0 && 0>=C && M>=1 && L>=1+O && 0>=1+E && L>=1 && D>=F && Q_1==1 ], cost: -7-7*G+7*D 192: f10 -> [19] : [], cost: 0 150: [19] -> [14] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 160: [19] -> [14] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 170: [19] -> [14] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 180: [19] -> [14] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 151: [19] -> [15] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 161: [19] -> [15] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 171: [19] -> [15] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 181: [19] -> [15] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 152: [19] -> [16] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 162: [19] -> [16] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 172: [19] -> [16] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 182: [19] -> [16] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 153: [19] -> [17] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 163: [19] -> [17] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 173: [19] -> [17] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 183: [19] -> [17] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 154: [19] -> [18] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 164: [19] -> [18] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 174: [19] -> [18] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 184: [19] -> [18] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C Applied chaining over branches and pruning: Start location: f2 193: f2 -> [19] : E'=0, F'=1, G'=0, [ C>=0 && D>=1 ], cost: 1 150: [19] -> [14] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 160: [19] -> [14] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 170: [19] -> [14] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 180: [19] -> [14] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 151: [19] -> [15] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 161: [19] -> [15] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 171: [19] -> [15] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 181: [19] -> [15] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 152: [19] -> [16] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 162: [19] -> [16] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 172: [19] -> [16] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 182: [19] -> [16] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 153: [19] -> [17] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 163: [19] -> [17] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 173: [19] -> [17] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 183: [19] -> [17] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 154: [19] -> [18] : C'=0, H'=1, J'=1, K'=L, [ D>=1+G && 0>=G && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 164: [19] -> [18] : C'=0, H'=1, J'=0, K'=L, [ D>=1+G && 0>=G && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 174: [19] -> [18] : C'=0, H'=0, J'=1, K'=L, [ D>=1+G && G>=1 && Q>=0 && 1+G>=D && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C 184: [19] -> [18] : C'=0, H'=0, J'=0, K'=L, [ D>=1+G && G>=1 && Q>=0 && D>=2+G && 1>=Q && C>=1 && D>=F && Q==0 ], cost: 2+2*C Applied chaining over branches and pruning: Start location: f2 194: f2 -> [14] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 195: f2 -> [14] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 196: f2 -> [15] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 197: f2 -> [15] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 198: f2 -> [16] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 199: f2 -> [16] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 200: f2 -> [17] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 201: f2 -> [17] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 202: f2 -> [18] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 203: f2 -> [18] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C Final control flow graph problem, now checking costs for infinitely many models: Start location: f2 194: f2 -> [14] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 195: f2 -> [14] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 196: f2 -> [15] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 197: f2 -> [15] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 198: f2 -> [16] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 199: f2 -> [16] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 200: f2 -> [17] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 201: f2 -> [17] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 202: f2 -> [18] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=1, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C 203: f2 -> [18] : C'=0, E'=0, F'=1, G'=0, H'=1, J'=0, K'=L, [ C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && D>=2 && 1>=Q && C>=1 && D>=1 && Q==0 ], cost: 3+2*C Computing complexity for remaining 10 transitions. Found configuration with infinitely models for cost: 3+2*C and guard: C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0: Q: Both, C: Pos, D: Const Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: C>=0 && D>=1 && D>=1 && 0>=0 && Q>=0 && 1>=D && 1>=Q && C>=1 && D>=1 && Q==0 Final Cost: 3+2*C 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),?)