YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E) -> eval(A,B,C,D,E) True (1,1) 1. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) Signature: {(eval,5);(start,5)} Flow Graph: [0->{1,2,3,4},1->{1,2,3,4},2->{1,2,3,4},3->{1,2,3,4},4->{1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3),(1,4),(2,1),(2,3),(2,4),(3,2),(4,1)] * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E) -> eval(A,B,C,D,E) True (1,1) 1. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) Signature: {(eval,5);(start,5)} Flow Graph: [0->{1,2,3,4},1->{1},2->{2},3->{1,3,4},4->{2,3,4}] + Applied Processor: AddSinks + Details: () * Step 3: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E) -> eval(A,B,C,D,E) True (1,1) 1. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 5. eval(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(eval,5);(exitus616,5);(start,5)} Flow Graph: [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2,3,4,5},4->{1,2,3,4,5},5->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3),(1,4),(2,1),(2,3),(2,4),(3,2),(4,1)] * Step 4: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start(A,B,C,D,E) -> eval(A,B,C,D,E) True (1,1) 1. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 5. eval(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(eval,5);(exitus616,5);(start,5)} Flow Graph: [0->{1,2,3,4,5},1->{1,5},2->{2,5},3->{1,3,4,5},4->{2,3,4,5},5->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | +- p:[2] c: [2] | `- p:[1] c: [1] * Step 5: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. start(A,B,C,D,E) -> eval(A,B,C,D,E) True (1,1) 1. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D,E) -> eval(A,B,C,1 + D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D,E) -> eval(A,1 + B,C,D,1 + E) [A >= 1 + B && C >= 1 + D] (?,1) 5. eval(A,B,C,D,E) -> exitus616(A,B,C,D,E) True (?,1) Signature: {(eval,5);(exitus616,5);(start,5)} Flow Graph: [0->{1,2,3,4,5},1->{1,5},2->{2,5},3->{1,3,4,5},4->{2,3,4,5},5->{}] ,We construct a looptree: P: [0,1,2,3,4,5] | +- p:[3,4] c: [4] | | | `- p:[3] c: [3] | +- p:[2] c: [2] | `- p:[1] c: [1]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 6: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.0.0,0.1,0.2] start ~> eval [A <= A, B <= B, C <= C, D <= D, E <= E] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D, E <= K + E] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D, E <= K + E] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D, E <= K + E] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D, E <= K + E] eval ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= A + B] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D, E <= K + E] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D, E <= K + E] + Loop: [0.0.0 <= C + D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D, E <= K + E] + Loop: [0.1 <= C + D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D, E <= K + E] + Loop: [0.2 <= A + B] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D, E <= K + E] + Applied Processor: FlowAbstraction + Details: () * Step 7: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.0.0,0.1,0.2] start ~> eval [] eval ~> eval [A ~+> B,B ~+> B,E ~+> E,K ~+> E] eval ~> eval [C ~+> D,D ~+> D,E ~+> E,K ~+> E] eval ~> eval [C ~+> D,D ~+> D,E ~+> E,K ~+> E] eval ~> eval [A ~+> B,B ~+> B,E ~+> E,K ~+> E] eval ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] eval ~> eval [C ~+> D,D ~+> D,E ~+> E,K ~+> E] eval ~> eval [A ~+> B,B ~+> B,E ~+> E,K ~+> E] + Loop: [C ~+> 0.0.0,D ~+> 0.0.0] eval ~> eval [C ~+> D,D ~+> D,E ~+> E,K ~+> E] + Loop: [C ~+> 0.1,D ~+> 0.1] eval ~> eval [C ~+> D,D ~+> D,E ~+> E,K ~+> E] + Loop: [A ~+> 0.2,B ~+> 0.2] eval ~> eval [A ~+> B,B ~+> B,E ~+> E,K ~+> E] + Applied Processor: LareProcessor + Details: start ~> exitus616 [A ~+> B ,A ~+> 0.0 ,A ~+> 0.2 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> 0.2 ,B ~+> tick ,C ~+> D ,C ~+> 0.0.0 ,C ~+> 0.1 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> 0.1 ,D ~+> tick ,E ~+> E ,tick ~+> tick ,K ~+> E ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> tick ,C ~*> D ,C ~*> E ,D ~*> D ,D ~*> E ,K ~*> E ,A ~^> D ,B ~^> D] + eval> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,C ~+> D ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> E ,tick ~+> tick ,K ~+> E ,A ~*> B ,A ~*> D ,A ~*> E ,A ~*> tick ,B ~*> B ,B ~*> D ,B ~*> E ,B ~*> tick ,C ~*> D ,C ~*> E ,D ~*> D ,D ~*> E ,K ~*> E ,A ~^> D ,B ~^> D] + eval> [C ~+> D ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> E ,tick ~+> tick ,K ~+> E ,C ~*> D ,C ~*> E ,D ~*> D ,D ~*> E ,K ~*> E] + eval> [C ~+> D ,C ~+> 0.1 ,C ~+> tick ,D ~+> D ,D ~+> 0.1 ,D ~+> tick ,E ~+> E ,tick ~+> tick ,K ~+> E ,C ~*> D ,C ~*> E ,D ~*> D ,D ~*> E ,K ~*> E] + eval> [A ~+> B ,A ~+> 0.2 ,A ~+> tick ,B ~+> B ,B ~+> 0.2 ,B ~+> tick ,E ~+> E ,tick ~+> tick ,K ~+> E ,A ~*> B ,A ~*> E ,B ~*> B ,B ~*> E ,K ~*> E] YES(?,POLY)