YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 101 && B = C && D = E && F = A && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [E >= 1 + C && B = C && D = E && F = A && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [C >= E && 100 >= A && B = C && D = E && F = A && G = H] (?,1) 3. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [F >= 101 (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 4. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A + C + E >= 1 + 2*B + F (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [2*B + F >= A + C + E (?,1) && 100 >= F && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 6. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,A,H,H) True (1,1) Signature: {(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{},2->{3,4,5},3->{},4->{},5->{3,4,5},6->{0,1,2}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 101 && B = C && D = E && F = A && G = H] (1,1) 1. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [E >= 1 + C && B = C && D = E && F = A && G = H] (1,1) 2. start(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [C >= E && 100 >= A && B = C && D = E && F = A && G = H] (1,1) 3. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [F >= 101 (1,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 4. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A + C + E >= 1 + 2*B + F (1,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [2*B + F >= A + C + E (?,1) && 100 >= F && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 6. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,A,H,H) True (1,1) Signature: {(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{},2->{3,4,5},3->{},4->{},5->{3,4,5},6->{0,1,2}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 101 && B = C && D = E && F = A && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [E >= 1 + C && B = C && D = E && F = A && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [C >= E && 100 >= A && B = C && D = E && F = A && G = H] (?,1) 3. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [F >= 101 (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 4. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A + C + E >= 1 + 2*B + F (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [2*B + F >= A + C + E (?,1) && 100 >= F && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 6. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,A,H,H) True (1,1) 7. lbl72(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True (?,1) 8. start(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True (?,1) Signature: {(exitus616,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{},2->{3,4,5,7},3->{},4->{},5->{3,4,5,7},6->{0,1,2,8},7->{},8->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | `- p:[5] c: [5] * Step 4: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A >= 101 && B = C && D = E && F = A && G = H] (?,1) 1. start(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [E >= 1 + C && B = C && D = E && F = A && G = H] (?,1) 2. start(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [C >= E && 100 >= A && B = C && D = E && F = A && G = H] (?,1) 3. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [F >= 101 (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 4. lbl72(A,B,C,D,E,F,G,H) -> stop(A,B,C,D,E,F,G,H) [A + C + E >= 1 + 2*B + F (?,1) && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 5. lbl72(A,B,C,D,E,F,G,H) -> lbl72(A,-1 + B,C,1 + F,E,D,F,H) [2*B + F >= A + C + E (?,1) && 100 >= F && 100 >= A && 101 + B + F >= A + C + E && 1 + B >= F && C >= 1 + B && C >= E && 1 + B + F + G = A + C + E && B + D + F = A + C + E] 6. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,A,H,H) True (1,1) 7. lbl72(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True (?,1) 8. start(A,B,C,D,E,F,G,H) -> exitus616(A,B,C,D,E,F,G,H) True (?,1) Signature: {(exitus616,8);(lbl72,8);(start,8);(start0,8);(stop,8)} Flow Graph: [0->{},1->{},2->{3,4,5,7},3->{},4->{},5->{3,4,5,7},6->{0,1,2,8},7->{},8->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | `- p:[5] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,0.0] start ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start ~> lbl72 [A <= A, B <= K + C, C <= C, D <= K + F, E <= E, F <= D, G <= F, H <= H] lbl72 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] lbl72 ~> lbl72 [A <= A, B <= C + G, C <= C, D <= K + F, E <= E, F <= D, G <= F, H <= H] start0 ~> start [A <= A, B <= C, C <= C, D <= E, E <= E, F <= A, G <= H, H <= H] lbl72 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] start ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H] + Loop: [0.0 <= 101*K + A + 2*B + C + E] lbl72 ~> lbl72 [A <= A, B <= C + G, C <= C, D <= K + F, E <= E, F <= D, G <= F, H <= H] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,0.0] start ~> stop [] start ~> stop [] start ~> lbl72 [D ~=> F,F ~=> G,C ~+> B,F ~+> D,K ~+> B,K ~+> D] lbl72 ~> stop [] lbl72 ~> stop [] lbl72 ~> lbl72 [D ~=> F,F ~=> G,C ~+> B,F ~+> D,G ~+> B,K ~+> D] start0 ~> start [A ~=> F,C ~=> B,E ~=> D,H ~=> G] lbl72 ~> exitus616 [] start ~> exitus616 [] + Loop: [A ~+> 0.0,C ~+> 0.0,E ~+> 0.0,B ~*> 0.0,K ~*> 0.0] lbl72 ~> lbl72 [D ~=> F,F ~=> G,C ~+> B,F ~+> D,G ~+> B,K ~+> D] + Applied Processor: LareProcessor + Details: start0 ~> stop [A ~=> F ,A ~=> G ,C ~=> B ,E ~=> D ,E ~=> F ,E ~=> G ,H ~=> G ,A ~+> B ,A ~+> D ,A ~+> F ,A ~+> G ,A ~+> 0.0 ,A ~+> tick ,C ~+> B ,C ~+> 0.0 ,C ~+> tick ,E ~+> B ,E ~+> D ,E ~+> F ,E ~+> G ,E ~+> 0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> F ,K ~+> G ,A ~*> D ,A ~*> F ,C ~*> D ,C ~*> F ,C ~*> 0.0 ,C ~*> tick ,E ~*> D ,E ~*> F ,K ~*> B ,K ~*> D ,K ~*> F ,K ~*> G ,K ~*> 0.0 ,K ~*> tick] start0 ~> exitus616 [A ~=> F ,A ~=> G ,C ~=> B ,E ~=> D ,E ~=> F ,E ~=> G ,H ~=> G ,A ~+> B ,A ~+> D ,A ~+> F ,A ~+> G ,A ~+> 0.0 ,A ~+> tick ,C ~+> B ,C ~+> 0.0 ,C ~+> tick ,E ~+> B ,E ~+> D ,E ~+> F ,E ~+> G ,E ~+> 0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> F ,K ~+> G ,A ~*> D ,A ~*> F ,C ~*> D ,C ~*> F ,C ~*> 0.0 ,C ~*> tick ,E ~*> D ,E ~*> F ,K ~*> B ,K ~*> D ,K ~*> F ,K ~*> G ,K ~*> 0.0 ,K ~*> tick] + lbl72> [D ~=> F ,D ~=> G ,F ~=> G ,A ~+> 0.0 ,A ~+> tick ,C ~+> B ,C ~+> 0.0 ,C ~+> tick ,D ~+> B ,D ~+> D ,D ~+> F ,D ~+> G ,E ~+> 0.0 ,E ~+> tick ,F ~+> B ,F ~+> D ,F ~+> F ,F ~+> G ,G ~+> B ,tick ~+> tick ,K ~+> B ,K ~+> D ,K ~+> F ,K ~+> G ,A ~*> D ,A ~*> F ,B ~*> D ,B ~*> F ,B ~*> 0.0 ,B ~*> tick ,C ~*> D ,C ~*> F ,E ~*> D ,E ~*> F ,K ~*> B ,K ~*> D ,K ~*> F ,K ~*> G ,K ~*> 0.0 ,K ~*> tick] YES(?,POLY)