YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (1,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (1,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (1,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) 12. evalSimpleSingle2returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11,12},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11,12},10->{2,3,4} ,11->{},12->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,7,5,3,10,8,6] c: [8] | `- p:[2,7,5,3] c: [5] * Step 4: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) True (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [D >= 1 + A] (?,1) 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A >= D] (?,1) 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True (?,1) 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) True (?,1) 12. evalSimpleSingle2returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11,12},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11,12},10->{2,3,4} ,11->{},12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,7,5,3,10,8,6] c: [8] | `- p:[2,7,5,3] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalSimpleSingle2start ~> evalSimpleSingle2entryin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2entryin ~> evalSimpleSingle2bb4in [A <= 0*K, B <= 0*K, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2returnin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= K + A, B <= K + B, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2returnin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A <= K + A, B <= K + B, C <= C, D <= D] evalSimpleSingle2returnin ~> evalSimpleSingle2stop [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2returnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 2*K + A + D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= K + A, B <= K + B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A <= K + A, B <= K + B, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= 2*K + B + C] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= K + A, B <= K + B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalSimpleSingle2start ~> evalSimpleSingle2entryin [] evalSimpleSingle2entryin ~> evalSimpleSingle2bb4in [K ~=> A,K ~=> B] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb4in ~> evalSimpleSingle2returnin [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A ~+> A,B ~+> B,K ~+> A,K ~+> B] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [] evalSimpleSingle2bb2in ~> evalSimpleSingle2returnin [] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A ~+> A,B ~+> B,K ~+> A,K ~+> B] evalSimpleSingle2returnin ~> evalSimpleSingle2stop [] evalSimpleSingle2returnin ~> exitus616 [] + Loop: [A ~+> 0.0,D ~+> 0.0,K ~*> 0.0] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A ~+> A,B ~+> B,K ~+> A,K ~+> B] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A ~+> A,B ~+> B,K ~+> A,K ~+> B] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [] + Loop: [B ~+> 0.0.0,C ~+> 0.0.0,K ~*> 0.0.0] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A ~+> A,B ~+> B,K ~+> A,K ~+> B] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] + Applied Processor: LareProcessor + Details: evalSimpleSingle2start ~> exitus616 [K ~=> A ,K ~=> B ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> A ,C ~*> B ,C ~*> 0.0 ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> A ,D ~*> B ,D ~*> 0.0 ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,C ~^> A ,C ~^> B ,C ~^> 0.0.0 ,C ~^> tick ,D ~^> A ,D ~^> B ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> A ,K ~^> B ,K ~^> 0.0.0 ,K ~^> tick] evalSimpleSingle2start ~> evalSimpleSingle2stop [K ~=> A ,K ~=> B ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> A ,C ~*> B ,C ~*> 0.0 ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> A ,D ~*> B ,D ~*> 0.0 ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,C ~^> A ,C ~^> B ,C ~^> 0.0.0 ,C ~^> tick ,D ~^> A ,D ~^> B ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> A ,K ~^> B ,K ~^> 0.0.0 ,K ~^> tick] + evalSimpleSingle2bb4in> [A ~+> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> A ,D ~*> B ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,D ~^> B ,K ~^> B] evalSimpleSingle2bb2in> [A ~+> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> A ,D ~*> B ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> A ,A ~^> B ,A ~^> 0.0.0 ,A ~^> tick ,D ~^> A ,D ~^> B ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> A ,K ~^> B ,K ~^> 0.0.0 ,K ~^> tick] + evalSimpleSingle2bbin> [A ~+> A ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,B ~*> A ,B ~*> B ,C ~*> A ,C ~*> B ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick] evalSimpleSingle2bb4in> [A ~+> A ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,B ~*> A ,B ~*> B ,C ~*> A ,C ~*> B ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)