C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_MP3\MP3_ABS.bpel C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_MP3\MP3.wsdl C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_Buy\Buy_ABS.bpel C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_Buy\Buy.wsdl C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_CD-Mania\CD-Mania_ABS.bpel C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_Buy\Buy.wsdl C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_MP3\MP3.wsdl C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_CD-Mania\CD-Mania.wsdl C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_User\User_ABS.bpel C:\Eclipse3.2.2\eclipse\workspace\CD-Mania_CD-Mania\CD-Mania.wsdl ASTRO Requirement composition goal CD-Mania Deadlock deadlock Verification ofdeadlock states CD-Mania_ABS SimultaneousSuccess assertion (F (instate(User_ABS,SUCC))<->(F (instate(Buy_ABS,SUCC))&F (instate(MP3_ABS,SUCC)))) Services reach their successfull statessimultaneously CD-Mania_ABS AllOffer instance (cause(CD-Mania_ABS.pc=FAIL_NACK)&O(cause(CD-Mania_ABS.pc=pick)))->(!O(cause(Buy_ABS.pc=FAIL))|!O(cause(MP3_ABS.pc=pick))) if both Buy and MP3 make an offer, then User wont receive a not_avail CD-Mania_ABS OfferToCD instance (cause(CD-Mania_ABS.pc=FAIL)&!O(cause(CD-Mania_ABS.pc=pick)))->(!O(cause(Buy_ABS.pc=FAIL))|!O(cause(MP3_ABS.pc=pick))) if both Buy and MP3 make an offer, then User will accept CD-Mania_ABS