Trying to load file: main.koat Initial Control flow graph problem: Start location: f9 0: f12 -> f16 : B'=1, C'=free_2, D'=free, E'=free_1, F'=1+G, H'=free_3, Q'=G, [ A>=0 && free_2>=2 && free_4>=free_2 && B==1 ], cost: 1 2: f16 -> f16 : B'=1+B, C'=free_11, D'=free_9, E'=free_10, G'=-1+G, L'=M, N'=free_12, O'=1+B, P'=-1+G, [ B>=0 && G>=0 && free_11>=2 ], cost: 1 10: f16 -> f8 : B'=1+H1, C'=free_48, M'=0, A1'=H1, B1'=0, C1'=D, D1'=0, E1'=D, F1'=D, G1'=D, [ free_49>=2 && free_48>=2 && B>=0 && G>=0 && M==0 ], cost: 1 1: f13 -> f16 : C'=free_7, D'=free_5, J'=free_6, K'=free_8, [ free_7>=2 && Q>=0 ], cost: 1 9: f13 -> f8 : B'=1+H1, C'=free_46, Q'=0, M'=0, A1'=H1, B1'=0, C1'=D, D1'=0, E1'=D, F1'=D, G1'=D, [ free_47>=2 && free_46>=2 && M==0 && Q==0 && B==1 ], cost: 1 4: f1 -> f16 : A'=G, B'=0, C'=free_21, D'=R, M'=R, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, [ A>=Q_1 && A>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 ], cost: 1 3: f1 -> f1 : A'=1+A, R'=S, S'=free_14, T'=S, U'=free_13, V'=A, [ Q_1>=1+A && A>=0 ], cost: 1 5: f7 -> f8 : C'=free_25, D'=free_24, M'=0, B1'=0, C1'=free_24, D1'=0, E1'=free_24, F1'=G1, [ free_25>=2 && A1>=0 && B1==0 ], cost: 1 6: f7 -> f10 : C'=free_32, D'=free_34, Y'=free_28, B1'=free_26, C1'=free_29, D1'=free_31, E1'=free_33, F1'=free_27, G1'=free_30, [ free_32>=2 && A1>=0 && B1==G1 ], cost: 1 7: f8 -> f8 : C'=free_37, D'=free_35, E'=free_36, M'=0, B1'=0, C1'=free_35, D1'=0, E1'=free_35, F1'=G1, H1'=-1+H1, Q1'=-1+H1, [ free_37>=2 && H1>=0 && B1==0 ], cost: 1 8: f8 -> f10 : C'=free_43, Y'=free_45, B1'=free_38, C1'=free_40, D1'=free_42, E1'=free_44, F1'=free_39, G1'=free_41, [ free_43>=2 && H1>=0 && B1==G1 ], cost: 1 11: f9 -> f1 : A'=2, C'=free_53, Q_1'=free_53, R'=free_52, S'=free_54, T'=free_52, W'=free_52, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 ], cost: 1 12: f9 -> f10 : A'=free_70, C'=free_66, D'=0, M'=0, Q_1'=free_58, R'=free_63, S'=free_62, T'=free_57, W'=free_68, X'=free_67, Y'=free_56, B1'=free_55, C1'=free_60, D1'=free_65, E1'=free_69, F1'=free_61, G1'=free_64, J1'=free_59, [ 0>=free_72 && 0>=free_73 && 0>=free_66 && 0>=free_71 ], cost: 1 13: f9 -> f10 : A'=free_89, C'=1, D'=free_83, M'=0, Q_1'=free_77, R'=free_82, S'=free_81, T'=free_76, W'=free_87, X'=free_86, Y'=free_75, B1'=free_88, C1'=free_85, D1'=free_79, E1'=free_84, F1'=free_80, G1'=free_74, J1'=free_78, [ S==0 ], cost: 1 Simplified the transitions: Start location: f9 2: f16 -> f16 : B'=1+B, C'=free_11, D'=free_9, E'=free_10, G'=-1+G, L'=M, N'=free_12, O'=1+B, P'=-1+G, [ B>=0 && G>=0 && free_11>=2 ], cost: 1 10: f16 -> f8 : B'=1+H1, C'=free_48, M'=0, A1'=H1, B1'=0, C1'=D, D1'=0, E1'=D, F1'=D, G1'=D, [ free_48>=2 && B>=0 && G>=0 && M==0 ], cost: 1 4: f1 -> f16 : A'=G, B'=0, C'=free_21, D'=R, M'=R, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, [ A>=Q_1 && A>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 ], cost: 1 3: f1 -> f1 : A'=1+A, R'=S, S'=free_14, T'=S, U'=free_13, V'=A, [ Q_1>=1+A && A>=0 ], cost: 1 7: f8 -> f8 : C'=free_37, D'=free_35, E'=free_36, M'=0, B1'=0, C1'=free_35, D1'=0, E1'=free_35, F1'=G1, H1'=-1+H1, Q1'=-1+H1, [ free_37>=2 && H1>=0 && B1==0 ], cost: 1 11: f9 -> f1 : A'=2, C'=free_53, Q_1'=free_53, R'=free_52, S'=free_54, T'=free_52, W'=free_52, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 ], cost: 1 Eliminating 1 self-loops for location f16 Self-Loop 2 has the metering function: 1+G, resulting in the new transition 14. Removing the self-loops: 2. Eliminating 1 self-loops for location f1 Self-Loop 3 has the metering function: Q_1-A, resulting in the new transition 15. Removing the self-loops: 3. Eliminating 1 self-loops for location f8 Self-Loop 7 has the metering function: 1+H1, resulting in the new transition 16. Removing the self-loops: 7. Removed all Self-loops using metering functions (where possible): Start location: f9 14: f16 -> [8] : B'=1+B+G, C'=free_11, D'=free_9, E'=free_10, G'=-1, L'=M, N'=free_12, O'=1+B+G, P'=-1, [ B>=0 && G>=0 && free_11>=2 ], cost: 1+G 15: f1 -> [9] : A'=Q_1, R'=free_14, S'=free_14, T'=free_14, U'=free_13, V'=-1+Q_1, [ Q_1>=1+A && A>=0 ], cost: Q_1-A 16: f8 -> [10] : C'=free_37, D'=free_35, E'=free_36, M'=0, B1'=0, C1'=free_35, D1'=0, E1'=free_35, F1'=G1, H1'=-1, Q1'=-1, [ free_37>=2 && H1>=0 && B1==0 ], cost: 1+H1 11: f9 -> f1 : A'=2, C'=free_53, Q_1'=free_53, R'=free_52, S'=free_54, T'=free_52, W'=free_52, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 ], cost: 1 10: [8] -> f8 : B'=1+H1, C'=free_48, M'=0, A1'=H1, B1'=0, C1'=D, D1'=0, E1'=D, F1'=D, G1'=D, [ free_48>=2 && B>=0 && G>=0 && M==0 ], cost: 1 4: [9] -> f16 : A'=G, B'=0, C'=free_21, D'=R, M'=R, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, [ A>=Q_1 && A>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 ], cost: 1 Applied simple chaining: Start location: f9 11: f9 -> [8] : A'=G, B'=1+G, C'=free_11, D'=free_9, E'=free_10, G'=-1, L'=free_14, M'=free_14, N'=free_12, O'=1+G, P'=-1, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, U'=free_13, V'=-1+free_53, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 && free_53>=3 && 2>=0 && free_53>=free_53 && free_53>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 && 0>=0 && G>=0 && free_11>=2 ], cost: 1+free_53+G 10: [8] -> [10] : B'=1+H1, C'=free_37, D'=free_35, E'=free_36, M'=0, A1'=H1, B1'=0, C1'=free_35, D1'=0, E1'=free_35, F1'=D, G1'=D, H1'=-1, Q1'=-1, [ free_48>=2 && B>=0 && G>=0 && M==0 && free_37>=2 && H1>=0 && 0==0 ], cost: 2+H1 Applied chaining over branches and pruning: Start location: f9 17: f9 -> [11] : A'=G, B'=1+G, C'=free_11, D'=free_9, E'=free_10, G'=-1, L'=free_14, M'=free_14, N'=free_12, O'=1+G, P'=-1, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, U'=free_13, V'=-1+free_53, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 && free_53>=3 && 2>=0 && free_53>=free_53 && free_53>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 && 0>=0 && G>=0 && free_11>=2 ], cost: 1+free_53+G Final control flow graph problem, now checking costs for infinitely many models: Start location: f9 17: f9 -> [11] : A'=G, B'=1+G, C'=free_11, D'=free_9, E'=free_10, G'=-1, L'=free_14, M'=free_14, N'=free_12, O'=1+G, P'=-1, Q_1'=free_18, R'=free_20, S'=free_19, T'=free_15, U'=free_13, V'=-1+free_53, W'=free_22, X'=free_23, Y'=free_17, Z'=free_16, J1'=free_51, K1'=free_50, L1'=2, [ free_53>=2 && free_53>=3 && 2>=0 && free_53>=free_53 && free_53>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 && 0>=0 && G>=0 && free_11>=2 ], cost: 1+free_53+G Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: 1+free_53+G and guard: free_53>=2 && free_53>=3 && 2>=0 && free_53>=free_53 && free_53>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 && 0>=0 && G>=0 && free_11>=2: B: Both, free_11: Pos, free_53: Pos, free_21: Const, G: Pos, free_16: Pos Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: free_53>=2 && free_53>=3 && 2>=0 && free_53>=free_53 && free_53>=0 && free_21>=2 && free_16>=free_21 && G>=free_21 && B==0 && 0>=0 && G>=0 && free_11>=2 Final Cost: 1+free_53+G Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)