YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + A && B = C && D = A] (?,1) 1. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + C && B = C && D = A] (?,1) 2. start(A,B,C,D) -> stop(A,B,C,D) [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (?,1) 3. start(A,B,C,D) -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A] (?,1) 4. start(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A] (?,1) 5. lbl81(A,B,C,D) -> stop(A,B,C,D) [C >= 3 + A && A >= 0 && 2 + D = C && B = C] (?,1) 6. lbl81(A,B,C,D) -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 7. lbl81(A,B,C,D) -> lbl91(A,1 + B,C,D) [D >= 3 + C && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 8. lbl91(A,B,C,D) -> stop(A,B,C,D) [A >= 3 + C && C >= 0 && 2 + B = A && D = A] (?,1) 9. lbl91(A,B,C,D) -> lbl81(A,B,C,1 + D) [B >= 3 + A && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 10. lbl91(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{},2->{},3->{5,6,7},4->{8,9,10},5->{},6->{5,6,7},7->{8,9,10},8->{},9->{5,6,7},10->{8,9,10} ,11->{0,1,2,3,4}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatRules WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + C && B = C && D = A] (1,1) 2. start(A,B,C,D) -> stop(A,B,C,D) [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A] (1,1) 4. start(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A] (1,1) 5. lbl81(A,B,C,D) -> stop(A,B,C,D) [C >= 3 + A && A >= 0 && 2 + D = C && B = C] (1,1) 6. lbl81(A,B,C,D) -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 7. lbl81(A,B,C,D) -> lbl91(A,1 + B,C,D) [D >= 3 + C && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 8. lbl91(A,B,C,D) -> stop(A,B,C,D) [A >= 3 + C && C >= 0 && 2 + B = A && D = A] (1,1) 9. lbl91(A,B,C,D) -> lbl81(A,B,C,1 + D) [B >= 3 + A && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 10. lbl91(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{},2->{},3->{5,6,7},4->{8,9,10},5->{},6->{5,6,7},7->{8,9,10},8->{},9->{5,6,7},10->{8,9,10} ,11->{0,1,2,3,4}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [7,9] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + A && B = C && D = A] (1,1) 1. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + C && B = C && D = A] (1,1) 2. start(A,B,C,D) -> stop(A,B,C,D) [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A] (1,1) 4. start(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A] (1,1) 5. lbl81(A,B,C,D) -> stop(A,B,C,D) [C >= 3 + A && A >= 0 && 2 + D = C && B = C] (1,1) 6. lbl81(A,B,C,D) -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 8. lbl91(A,B,C,D) -> stop(A,B,C,D) [A >= 3 + C && C >= 0 && 2 + B = A && D = A] (1,1) 10. lbl91(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{},2->{},3->{5,6},4->{8,10},5->{},6->{5,6},8->{},10->{8,10},11->{0,1,2,3,4}] + Applied Processor: AddSinks + Details: () * Step 4: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + A && B = C && D = A] (?,1) 1. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + C && B = C && D = A] (?,1) 2. start(A,B,C,D) -> stop(A,B,C,D) [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (?,1) 3. start(A,B,C,D) -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A] (?,1) 4. start(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A] (?,1) 5. lbl81(A,B,C,D) -> stop(A,B,C,D) [C >= 3 + A && A >= 0 && 2 + D = C && B = C] (?,1) 6. lbl81(A,B,C,D) -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 8. lbl91(A,B,C,D) -> stop(A,B,C,D) [A >= 3 + C && C >= 0 && 2 + B = A && D = A] (?,1) 10. lbl91(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) 12. lbl91(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 13. lbl81(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 14. start(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(exitus616,4);(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{},2->{},3->{5,6,13},4->{8,10,12},5->{},6->{5,6,13},8->{},10->{8,10,12},11->{0,1,2,3,4,14} ,12->{},13->{},14->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,8,10,11,12,13,14] | +- p:[10] c: [10] | `- p:[6] c: [6] * Step 5: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + A && B = C && D = A] (?,1) 1. start(A,B,C,D) -> stop(A,B,C,D) [0 >= 1 + C && B = C && D = A] (?,1) 2. start(A,B,C,D) -> stop(A,B,C,D) [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (?,1) 3. start(A,B,C,D) -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A] (?,1) 4. start(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A] (?,1) 5. lbl81(A,B,C,D) -> stop(A,B,C,D) [C >= 3 + A && A >= 0 && 2 + D = C && B = C] (?,1) 6. lbl81(A,B,C,D) -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C] (?,1) 8. lbl91(A,B,C,D) -> stop(A,B,C,D) [A >= 3 + C && C >= 0 && 2 + B = A && D = A] (?,1) 10. lbl91(A,B,C,D) -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A] (?,1) 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) 12. lbl91(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 13. lbl81(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 14. start(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(exitus616,4);(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{},2->{},3->{5,6,13},4->{8,10,12},5->{},6->{5,6,13},8->{},10->{8,10,12},11->{0,1,2,3,4,14} ,12->{},13->{},14->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,8,10,11,12,13,14] | +- p:[10] c: [10] | `- p:[6] c: [6]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 6: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.1] start ~> stop [A <= A, B <= B, C <= C, D <= D] start ~> stop [A <= A, B <= B, C <= C, D <= D] start ~> stop [A <= A, B <= B, C <= C, D <= D] start ~> lbl81 [A <= A, B <= B, C <= C, D <= C] start ~> lbl91 [A <= A, B <= A, C <= C, D <= D] lbl81 ~> stop [A <= A, B <= B, C <= C, D <= D] lbl81 ~> lbl81 [A <= A, B <= B, C <= C, D <= C] lbl91 ~> stop [A <= A, B <= B, C <= C, D <= D] lbl91 ~> lbl91 [A <= A, B <= D, C <= C, D <= D] start0 ~> start [A <= A, B <= C, C <= C, D <= A] lbl91 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] lbl81 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] start ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= A + B] lbl91 ~> lbl91 [A <= A, B <= D, C <= C, D <= D] + Loop: [0.1 <= C + D] lbl81 ~> lbl81 [A <= A, B <= B, C <= C, D <= C] + Applied Processor: FlowAbstraction + Details: () * Step 7: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.1] start ~> stop [] start ~> stop [] start ~> stop [] start ~> lbl81 [C ~=> D] start ~> lbl91 [A ~=> B] lbl81 ~> stop [] lbl81 ~> lbl81 [C ~=> D] lbl91 ~> stop [] lbl91 ~> lbl91 [D ~=> B] start0 ~> start [A ~=> D,C ~=> B] lbl91 ~> exitus616 [] lbl81 ~> exitus616 [] start ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] lbl91 ~> lbl91 [D ~=> B] + Loop: [C ~+> 0.1,D ~+> 0.1] lbl81 ~> lbl81 [C ~=> D] + Applied Processor: LareProcessor + Details: start0 ~> exitus616 [A ~=> B ,A ~=> D ,C ~=> B ,C ~=> D ,A ~+> 0.0 ,A ~+> tick ,C ~+> 0.1 ,C ~+> tick ,tick ~+> tick ,A ~*> 0.0 ,A ~*> tick ,C ~*> 0.1 ,C ~*> tick] start0 ~> stop [A ~=> B ,A ~=> D ,C ~=> B ,C ~=> D ,A ~+> 0.0 ,A ~+> tick ,C ~+> 0.1 ,C ~+> tick ,tick ~+> tick ,A ~*> 0.0 ,A ~*> tick ,C ~*> 0.1 ,C ~*> tick] + lbl91> [D ~=> B,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick] + lbl81> [C ~=> D,C ~+> 0.1,C ~+> tick,D ~+> 0.1,D ~+> tick,tick ~+> tick] YES(?,POLY)