Trying to load file: main.koat Initial Control flow graph problem: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 17: f2 -> f22 : T'=M, [], cost: 1 10: f3 -> f2 : F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ free_9>=1 && F>=1 && N==0 ], cost: 1 3: f3 -> f3 : B'=1+B, C'=1+C, [ A>=1+B ], cost: 1 4: f3 -> f4 : [ B>=A ], cost: 1 11: f3 -> f25 : F'=free_10, P'=N, Q_1'=0, [ F>=1 && N>=1 && free_10>=1 ], cost: 1 12: f3 -> f25 : F'=free_11, P'=N, Q_1'=0, [ F>=1 && 0>=1+N && free_11>=1 ], cost: 1 5: f4 -> f5 : D'=0, E'=C, [], cost: 1 13: f4 -> f17 : S'=J, T'=0, [ J>=1 ], cost: 1 14: f4 -> f17 : S'=J, T'=0, [ 0>=1+J ], cost: 1 18: f4 -> f21 : J'=0, M'=free_13, S'=0, T'=0, U'=0, [ J==0 ], cost: 1 19: f5 -> f3 : F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ F>=0 && J>=1 && free_26>=0 ], cost: 1 20: f5 -> f3 : F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ F>=0 && 0>=1+J && free_39>=0 ], cost: 1 6: f5 -> f5 : D'=1+D, E'=-1+E, [ E>=1 ], cost: 1 9: f5 -> f16 : F'=1+F, Q'=1+Q, L'=M, [ 0>=E && F>=0 ], cost: 1 15: f5 -> f18 : F'=free_12, J'=0, S'=0, T'=0, [ free_12>=0 && F>=0 && J==0 ], cost: 1 8: f16 -> f1 : F'=free_7, [ Q>=H && F>=0 ], cost: 1 22: f16 -> f16 : F'=1+free_47, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ F>=0 && free_56>=0 && H>=1+Q && free_47>=0 ], cost: 1 16: f12 -> f16 : F'=Q, Q'=1+Q, L'=M, [], cost: 1 21: f23 -> f4 : G'=free_41, H'=free_43, Q'=free_44, J'=free_40, L'=0, Z'=free_42, [ 0>=free_45 ], cost: 1 23: f23 -> f16 : F'=free_58, G'=free_64, H'=free_57, Q'=1+free_58, L'=free_61, M'=free_61, A1'=free_61, B1'=free_61, C1'=free_61, D1'=free_60, E1'=free_63, F1'=free_59, Q1'=free_62, J1'=free_65, [ free_66>=1 ], cost: 1 Simplified the transitions: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 10: f3 -> f2 : F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ F>=1 && N==0 ], cost: 1 3: f3 -> f3 : B'=1+B, C'=1+C, [ A>=1+B ], cost: 1 4: f3 -> f4 : [ B>=A ], cost: 1 5: f4 -> f5 : D'=0, E'=C, [], cost: 1 19: f5 -> f3 : F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ F>=0 && J>=1 ], cost: 1 20: f5 -> f3 : F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ F>=0 && 0>=1+J ], cost: 1 6: f5 -> f5 : D'=1+D, E'=-1+E, [ E>=1 ], cost: 1 9: f5 -> f16 : F'=1+F, Q'=1+Q, L'=M, [ 0>=E && F>=0 ], cost: 1 8: f16 -> f1 : F'=free_7, [ Q>=H && F>=0 ], cost: 1 22: f16 -> f16 : F'=1+free_47, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ F>=0 && H>=1+Q && free_47>=0 ], cost: 1 Eliminating 1 self-loops for location f3 Self-Loop 3 has the metering function: -B+A, resulting in the new transition 24. Removing the self-loops: 3. Eliminating 1 self-loops for location f5 Self-Loop 6 has the metering function: E, resulting in the new transition 25. Removing the self-loops: 6. Eliminating 1 self-loops for location f16 Removing the self-loops: 22. Adding an epsilon transition (to model nonexecution of the loops): 27. Removed all Self-loops using metering functions (where possible): Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 24: f3 -> [14] : B'=A, C'=-B+C+A, [ A>=1+B ], cost: -B+A 5: f4 -> f5 : D'=0, E'=C, [], cost: 1 25: f5 -> [15] : D'=E+D, E'=0, [ E>=1 ], cost: E 26: f16 -> [16] : F'=1+free_47, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ F>=0 && H>=1+Q && free_47>=0 ], cost: 1 27: f16 -> [16] : [], cost: 0 10: [14] -> f2 : F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ F>=1 && N==0 ], cost: 1 4: [14] -> f4 : [ B>=A ], cost: 1 19: [15] -> f3 : F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ F>=0 && J>=1 ], cost: 1 20: [15] -> f3 : F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ F>=0 && 0>=1+J ], cost: 1 9: [15] -> f16 : F'=1+F, Q'=1+Q, L'=M, [ 0>=E && F>=0 ], cost: 1 8: [16] -> f1 : F'=free_7, [ Q>=H && F>=0 ], cost: 1 Applied simple chaining: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 24: f3 -> [14] : B'=A, C'=-B+C+A, [ A>=1+B ], cost: -B+A 25: f5 -> [15] : D'=E+D, E'=0, [ E>=1 ], cost: E 26: f16 -> [16] : F'=1+free_47, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ F>=0 && H>=1+Q && free_47>=0 ], cost: 1 27: f16 -> [16] : [], cost: 0 10: [14] -> f2 : F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ F>=1 && N==0 ], cost: 1 4: [14] -> f5 : D'=0, E'=C, [ B>=A ], cost: 2 19: [15] -> f3 : F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ F>=0 && J>=1 ], cost: 1 20: [15] -> f3 : F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ F>=0 && 0>=1+J ], cost: 1 9: [15] -> f16 : F'=1+F, Q'=1+Q, L'=M, [ 0>=E && F>=0 ], cost: 1 8: [16] -> f1 : F'=free_7, [ Q>=H && F>=0 ], cost: 1 Applied chaining over branches and pruning: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E 32: f5 -> f16 : D'=E+D, E'=0, F'=1+F, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 ], cost: 1+E 33: f16 -> f1 : F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ F>=0 && H>=1+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 2 34: f16 -> f1 : F'=free_7, [ Q>=H && F>=0 ], cost: 1 Applied chaining over branches and pruning: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E Final control flow graph problem, now checking costs for infinitely many models: Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 7: f1 -> f5 : F'=free_2, G'=free_4, H'=free_6, Q'=free_1, J'=free_3, K'=free_5, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E This is only a partial result (probably due to a timeout), trying to find max complexity Removed transitions with const cost Start location: f30 0: f30 -> f1 : [], cost: 1 1: f1 -> f2 : A'=free, [], cost: 1 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E Performed chaining from the start location: Start location: f30 37: f30 -> f2 : A'=free, [], cost: 2 2: f2 -> f3 : B'=0, C'=0, [], cost: 1 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E Performed chaining from the start location: Start location: f30 38: f30 -> f3 : A'=free, B'=0, C'=0, [], cost: 3 28: f3 -> f2 : B'=A, C'=-B+C+A, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ A>=1+B && F>=1 && N==0 ], cost: 1-B+A 29: f3 -> f5 : B'=A, C'=-B+C+A, D'=0, E'=-B+C+A, [ A>=1+B && A>=A ], cost: 2-B+A 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E Performed chaining from the start location: Start location: f30 39: f30 -> f2 : A'=free, B'=free, C'=free, F'=free_8, M'=O, N'=O, P'=0, Q_1'=0, R'=O, [ free>=1 && F>=1 && N==0 ], cost: 4+free 40: f30 -> f5 : A'=free, B'=free, C'=free, D'=0, E'=free, [ free>=1 && free>=free ], cost: 5+free 35: f5 -> f1 : D'=E+D, E'=0, F'=free_7, G'=free_54, H'=free_46, Q'=1+free_50, L'=free_51, M'=free_51, A1'=free_51, B1'=free_51, C1'=free_51, D1'=free_53, E1'=free_48, F1'=free_52, G1'=free_55, H1'=free_49, [ E>=1 && 0>=0 && F>=0 && 1+F>=0 && H>=2+Q && free_47>=0 && 1+free_50>=free_46 && 1+free_47>=0 ], cost: 3+E 36: f5 -> f1 : D'=E+D, E'=0, F'=free_7, Q'=1+Q, L'=M, [ E>=1 && 0>=0 && F>=0 && 1+Q>=H && 1+F>=0 ], cost: 2+E 30: f5 -> f3 : D'=E+D, E'=0, F'=free_15, G'=free_14, H'=free_18, Q'=free_22, J'=free_17, L'=free_23, N'=free_16, O'=free_25, S'=free_19, T'=0, V'=J, W'=free_20, X'=free_21, Y'=free_24, [ E>=1 && F>=0 && J>=1 ], cost: 1+E 31: f5 -> f3 : D'=E+D, E'=0, F'=free_28, G'=free_27, H'=free_31, Q'=free_35, J'=free_30, L'=free_36, N'=free_29, O'=free_38, S'=free_32, T'=0, V'=J, W'=free_33, X'=free_34, Y'=free_37, [ E>=1 && F>=0 && 0>=1+J ], cost: 1+E Found configuration with infinitely models for cost: 4+free and guard: free>=1 && F>=1 && N==0: N: Both, free: Pos, F: Pos Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: free>=1 && F>=1 && N==0 Final Cost: 4+free Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)