MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (?,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (?,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (?,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (?,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (1,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (1,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (1,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (1,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10},4->{10},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{}] + Applied Processor: AddSinks + Details: () * Step 3: Failure MAYBE + Considered Problem: Rules: 0. evalEx2start(A,B,C,D) -> evalEx2entryin(A,B,C,D) True (1,1) 1. evalEx2entryin(A,B,C,D) -> evalEx2bb3in(B,A,C,D) True (?,1) 2. evalEx2bb3in(A,B,C,D) -> evalEx2bbin(A,B,C,D) [B >= 1 && A >= 1] (?,1) 3. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= B] (?,1) 4. evalEx2bb3in(A,B,C,D) -> evalEx2returnin(A,B,C,D) [0 >= A] (?,1) 5. evalEx2bbin(A,B,C,D) -> evalEx2bb2in(A,B,-1 + A,-1 + B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 6. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E] 7. evalEx2bb2in(A,B,C,D) -> evalEx2bb1in(A,B,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1] 8. evalEx2bb2in(A,B,C,D) -> evalEx2bb3in(C,D,C,D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalEx2bb1in(A,B,C,D) -> evalEx2bb2in(A,B,1 + C,-1 + D) [-1 + B + -1*D >= 0 (?,1) && C + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 10. evalEx2returnin(A,B,C,D) -> evalEx2stop(A,B,C,D) True (?,1) 11. evalEx2returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalEx2bb1in,4) ;(evalEx2bb2in,4) ;(evalEx2bb3in,4) ;(evalEx2bbin,4) ;(evalEx2entryin,4) ;(evalEx2returnin,4) ;(evalEx2start,4) ;(evalEx2stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5},3->{10,11},4->{10,11},5->{6,7,8},6->{9},7->{9},8->{2,3,4},9->{6,7,8},10->{} ,11->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[2,8,5,9,6,7] c: [8] | `- p:[6,9,7] c: [] MAYBE