YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (?,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (?,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (?,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (?,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (?,1) Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (1,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (1,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (1,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (1,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (1,1) Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (?,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (?,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (?,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (?,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (?,1) 7. evalndloopreturnin(A) -> exitus616(A) True (?,1) Signature: {(evalndloopbbin,1) ;(evalndloopentryin,1) ;(evalndloopreturnin,1) ;(evalndloopstart,1) ;(evalndloopstop,1) ;(exitus616,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6,7},4->{6,7},5->{6,7},6->{},7->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7] | `- p:[2] c: [2] * Step 4: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (?,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (?,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (?,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (?,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (?,1) 7. evalndloopreturnin(A) -> exitus616(A) True (?,1) Signature: {(evalndloopbbin,1) ;(evalndloopentryin,1) ;(evalndloopreturnin,1) ;(evalndloopstart,1) ;(evalndloopstop,1) ;(exitus616,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6,7},4->{6,7},5->{6,7},6->{},7->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7] | `- p:[2] c: [2]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,0.0] evalndloopstart ~> evalndloopentryin [A <= A] evalndloopentryin ~> evalndloopbbin [A <= 0*K] evalndloopbbin ~> evalndloopbbin [A <= 9*K] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopbbin ~> evalndloopreturnin [A <= A] evalndloopreturnin ~> evalndloopstop [A <= A] evalndloopreturnin ~> exitus616 [A <= A] + Loop: [0.0 <= 9*K + A] evalndloopbbin ~> evalndloopbbin [A <= 9*K] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,0.0] evalndloopstart ~> evalndloopentryin [] evalndloopentryin ~> evalndloopbbin [K ~=> A] evalndloopbbin ~> evalndloopbbin [K ~=> A] evalndloopbbin ~> evalndloopreturnin [] evalndloopbbin ~> evalndloopreturnin [] evalndloopbbin ~> evalndloopreturnin [] evalndloopreturnin ~> evalndloopstop [] evalndloopreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] evalndloopbbin ~> evalndloopbbin [K ~=> A] + Applied Processor: LareProcessor + Details: evalndloopstart ~> exitus616 [K ~=> A,tick ~+> tick,K ~+> 0.0,K ~+> tick,K ~*> 0.0,K ~*> tick] evalndloopstart ~> evalndloopstop [K ~=> A,tick ~+> tick,K ~+> 0.0,K ~+> tick,K ~*> 0.0,K ~*> tick] + evalndloopbbin> [K ~=> A,A ~+> 0.0,A ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] YES(?,O(1))