YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (?,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (?,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3)] * Step 2: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (?,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (?,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: AddSinks + Details: () * Step 4: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] evaleasy1stop(A,B) -> exitus616(A,B) True Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{10}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | `- p:[2,7,4,8,5,6] c: [2,4,5,6,7,8] * Step 5: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] evaleasy1stop(A,B) -> exitus616(A,B) True Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{10}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | `- p:[2,7,4,8,5,6] c: [2,4,5,6,7,8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,0.0] evaleasy1start ~> evaleasy1entryin [A <= A, B <= B] evaleasy1entryin ~> evaleasy1bb3in [A <= 0*K, B <= B] evaleasy1bb3in ~> evaleasy1bbin [A <= A, B <= B] evaleasy1bb3in ~> evaleasy1returnin [A <= A, B <= B] evaleasy1bbin ~> evaleasy1bb1in [A <= A, B <= B] evaleasy1bbin ~> evaleasy1bb2in [A <= A, B <= B] evaleasy1bbin ~> evaleasy1bb2in [A <= A, B <= B] evaleasy1bb1in ~> evaleasy1bb3in [A <= 40*K, B <= B] evaleasy1bb2in ~> evaleasy1bb3in [A <= 41*K, B <= B] evaleasy1returnin ~> evaleasy1stop [A <= A, B <= B] evaleasy1stop ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= 39*K + A] evaleasy1bb3in ~> evaleasy1bbin [A <= A, B <= B] evaleasy1bb1in ~> evaleasy1bb3in [A <= 40*K, B <= B] evaleasy1bbin ~> evaleasy1bb1in [A <= A, B <= B] evaleasy1bb2in ~> evaleasy1bb3in [A <= 41*K, B <= B] evaleasy1bbin ~> evaleasy1bb2in [A <= A, B <= B] evaleasy1bbin ~> evaleasy1bb2in [A <= A, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0] evaleasy1start ~> evaleasy1entryin [] evaleasy1entryin ~> evaleasy1bb3in [K ~=> A] evaleasy1bb3in ~> evaleasy1bbin [] evaleasy1bb3in ~> evaleasy1returnin [] evaleasy1bbin ~> evaleasy1bb1in [] evaleasy1bbin ~> evaleasy1bb2in [] evaleasy1bbin ~> evaleasy1bb2in [] evaleasy1bb1in ~> evaleasy1bb3in [K ~=> A] evaleasy1bb2in ~> evaleasy1bb3in [K ~=> A] evaleasy1returnin ~> evaleasy1stop [] evaleasy1stop ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] evaleasy1bb3in ~> evaleasy1bbin [] evaleasy1bb1in ~> evaleasy1bb3in [K ~=> A] evaleasy1bbin ~> evaleasy1bb1in [] evaleasy1bb2in ~> evaleasy1bb3in [K ~=> A] evaleasy1bbin ~> evaleasy1bb2in [] evaleasy1bbin ~> evaleasy1bb2in [] + Applied Processor: Lare + Details: evaleasy1start ~> exitus616 [K ~=> A,tick ~+> tick,K ~+> 0.0,K ~+> tick,K ~*> 0.0,K ~*> tick] + evaleasy1bb3in> [K ~=> A,A ~+> 0.0,A ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] YES(?,O(1))