YES(?,O(n^1)) * Step 1: ArgumentFilter WORST_CASE(?,O(n^1)) + 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: ArgumentFilter [4] + Details: We remove following argument positions: [4]. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> eval(A,B,C,D) True (1,1) 1. eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D) -> eval(A,B,C,1 + D) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D) -> eval(A,B,C,1 + D) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D) -> eval(A,1 + B,C,D) [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 3: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> eval(A,B,C,D) True (1,1) 1. eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && D >= C] (?,1) 2. eval(A,B,C,D) -> eval(A,B,C,1 + D) [B >= A && C >= 1 + D] (?,1) 3. eval(A,B,C,D) -> eval(A,B,C,1 + D) [A >= 1 + B && C >= 1 + D] (?,1) 4. eval(A,B,C,D) -> eval(A,1 + B,C,D) [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: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: start(A,B,C,D) -> eval(A,B,C,D) True eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && D >= C] eval(A,B,C,D) -> eval(A,B,C,1 + D) [B >= A && C >= 1 + D] eval(A,B,C,D) -> eval(A,B,C,1 + D) [A >= 1 + B && C >= 1 + D] eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && C >= 1 + D] Signature: {(eval,5);(start,5)} Rule Graph: [0->{1,2,3,4},1->{1},2->{2},3->{1,3,4},4->{2,3,4}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: start(A,B,C,D) -> eval(A,B,C,D) True eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && D >= C] eval(A,B,C,D) -> eval(A,B,C,1 + D) [B >= A && C >= 1 + D] eval(A,B,C,D) -> eval(A,B,C,1 + D) [A >= 1 + B && C >= 1 + D] eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && C >= 1 + D] eval(A,B,C,D) -> exitus616(A,B,C,D) True eval(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(eval,5);(exitus616,4);(start,5)} Rule Graph: [0->{1,2,3,4},1->{1,6},2->{2,5},3->{1,3,4},4->{2,3,4}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[3,4] c: [3,4] | +- p:[2] c: [2] | `- p:[1] c: [1] * Step 6: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: start(A,B,C,D) -> eval(A,B,C,D) True eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && D >= C] eval(A,B,C,D) -> eval(A,B,C,1 + D) [B >= A && C >= 1 + D] eval(A,B,C,D) -> eval(A,B,C,1 + D) [A >= 1 + B && C >= 1 + D] eval(A,B,C,D) -> eval(A,1 + B,C,D) [A >= 1 + B && C >= 1 + D] eval(A,B,C,D) -> exitus616(A,B,C,D) True eval(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(eval,5);(exitus616,4);(start,5)} Rule Graph: [0->{1,2,3,4},1->{1,6},2->{2,5},3->{1,3,4},4->{2,3,4}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | +- p:[3,4] c: [3,4] | +- p:[2] c: [2] | `- p:[1] c: [1]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.1,0.2] start ~> eval [A <= A, B <= B, C <= C, D <= D] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D] eval ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B + C + D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D] + Loop: [0.1 <= K + C + D] eval ~> eval [A <= A, B <= B, C <= C, D <= C + D] + Loop: [0.2 <= K + A + B] eval ~> eval [A <= A, B <= A + B, C <= C, D <= D] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.1,0.2] start ~> eval [] eval ~> eval [A ~+> B,B ~+> B] eval ~> eval [C ~+> D,D ~+> D] eval ~> eval [C ~+> D,D ~+> D] eval ~> eval [A ~+> B,B ~+> B] eval ~> exitus616 [] eval ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,C ~+> 0.0,D ~+> 0.0,K ~+> 0.0] eval ~> eval [C ~+> D,D ~+> D] eval ~> eval [A ~+> B,B ~+> B] + Loop: [C ~+> 0.1,D ~+> 0.1,K ~+> 0.1] eval ~> eval [C ~+> D,D ~+> D] + Loop: [A ~+> 0.2,B ~+> 0.2,K ~+> 0.2] eval ~> eval [A ~+> B,B ~+> B] + Applied Processor: Lare + 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 ,C ~+> 0.1 ,C ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> tick ,A ~*> B ,A ~*> D ,B ~*> B ,B ~*> D ,C ~*> B ,C ~*> D ,D ~*> B ,D ~*> D ,K ~*> B ,K ~*> D] + eval> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,C ~+> D ,C ~+> 0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,A ~*> D ,B ~*> B ,B ~*> D ,C ~*> B ,C ~*> D ,D ~*> B ,D ~*> D ,K ~*> B ,K ~*> D] + eval> [C ~+> D ,C ~+> 0.1 ,C ~+> tick ,D ~+> D ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,C ~*> D ,D ~*> D ,K ~*> D] + eval> [A ~+> B ,A ~+> 0.2 ,A ~+> tick ,B ~+> B ,B ~+> 0.2 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.2 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,O(n^1))