MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: and(B,F()) -> F() and(B,T()) -> B and(F(),B) -> F() and(T(),B) -> B append(cons(Head,Tail),List) -> cons(Head,append(Tail,List)) case0(Client,Lock,MCRLFree0) -> Lock case0(Client,Lock,cons(Client,Pendings)) -> record_updates(Lock ,lock() ,cons(tuple(excl(),tuplenil(Client)) ,cons(tuple(pending(),tuplenil(Pendings)) ,nil()))) case1(Client,Resources,Lock,false()) -> Lock case1(Client,Resources,Lock,true()) -> record_updates(Lock ,lock() ,cons(tuple(pending() ,tuplenil(append(record_extract(Lock ,lock() ,pending()) ,cons(Client,nil())))) ,nil())) case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil())) case4(Client,Lock,MCRLFree1) -> false() case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client) case5(Client,Locks,Lock,true()) -> andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client)) case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks) case6(Locks,Lock,Resource,true()) -> andt(equal(record_extract(Lock,lock(),excl()),nil()) ,equal(record_extract(Lock,lock(),pending()),nil())) case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail)) case8(Tail,Head,E,true()) -> Tail case9(Tail,Head,E,false()) -> member(E,Tail) case9(Tail,Head,E,true()) -> true() delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head)) delete(E,nil()) -> nil() element(int(s(0())),tuple(T1,T2)) -> T1 element(int(s(0())),tuplenil(T1)) -> T1 element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2) eq(F(),F()) -> T() eq(F(),T()) -> F() eq(T(),F()) -> F() eq(T(),T()) -> T() eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) eqc(calls(E1,S1,CS1),nocalls()) -> F() eqc(nocalls(),calls(E2,S2,CS2)) -> F() eqc(nocalls(),nocalls()) -> T() eqs(empty(),empty()) -> T() eqs(empty(),stack(E2,S2)) -> F() eqs(stack(E1,S1),empty()) -> F() eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2)) eqt(a(),a()) -> T() eqt(a(),cons(H2,T2)) -> F() eqt(a(),excl()) -> F() eqt(a(),false()) -> F() eqt(a(),int(N2)) -> F() eqt(a(),lock()) -> F() eqt(a(),locker()) -> F() eqt(a(),mcrlrecord()) -> F() eqt(a(),nil()) -> F() eqt(a(),ok()) -> F() eqt(a(),pending()) -> F() eqt(a(),pid(N2)) -> F() eqt(a(),release()) -> F() eqt(a(),request()) -> F() eqt(a(),resource()) -> F() eqt(a(),tag()) -> F() eqt(a(),true()) -> F() eqt(a(),tuple(H2,T2)) -> F() eqt(a(),tuplenil(H2)) -> F() eqt(a(),undefined()) -> F() eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2)) eqt(cons(H1,T1),int(N2)) -> F() eqt(cons(H1,T1),pid(N2)) -> F() eqt(cons(H1,T1),resource()) -> F() eqt(cons(H1,T1),tag()) -> F() eqt(cons(H1,T1),true()) -> F() eqt(cons(H1,T1),tuple(H2,T2)) -> F() eqt(cons(H1,T1),tuplenil(H2)) -> F() eqt(cons(H1,T1),undefined()) -> F() eqt(excl(),a()) -> F() eqt(excl(),eqt(false(),int(N2))) -> F() eqt(excl(),excl()) -> T() eqt(excl(),false()) -> F() eqt(excl(),lock()) -> F() eqt(excl(),locker()) -> F() eqt(excl(),mcrlrecord()) -> F() eqt(excl(),nil()) -> F() eqt(excl(),ok()) -> F() eqt(excl(),pending()) -> F() eqt(excl(),pid(N2)) -> F() eqt(excl(),release()) -> F() eqt(excl(),request()) -> F() eqt(excl(),resource()) -> F() eqt(excl(),tag()) -> F() eqt(excl(),true()) -> F() eqt(excl(),undefined()) -> F() eqt(false(),cons(H2,T2)) -> F() eqt(false(),tuple(H2,T2)) -> F() eqt(false(),tuplenil(H2)) -> F() eqt(int(N1),a()) -> F() eqt(int(N1),excl()) -> F() eqt(int(N1),false()) -> F() eqt(int(N1),lock()) -> F() eqt(int(N1),locker()) -> F() eqt(int(N1),mcrlrecord()) -> F() eqt(int(N1),nil()) -> F() eqt(int(N1),ok()) -> F() eqt(int(N1),pending()) -> F() eqt(int(N1),release()) -> F() eqt(int(N1),request()) -> F() eqt(int(N1),resource()) -> F() eqt(int(N1),tag()) -> F() eqt(int(N1),true()) -> F() eqt(int(N1),undefined()) -> F() eqt(lock(),a()) -> F() eqt(lock(),cons(H2,T2)) -> F() eqt(lock(),excl()) -> F() eqt(lock(),false()) -> F() eqt(lock(),int(N2)) -> F() eqt(lock(),lock()) -> T() eqt(lock(),locker()) -> F() eqt(lock(),mcrlrecord()) -> F() eqt(lock(),nil()) -> F() eqt(lock(),ok()) -> F() eqt(lock(),pending()) -> F() eqt(lock(),pid(N2)) -> F() eqt(lock(),release()) -> F() eqt(lock(),request()) -> F() eqt(lock(),resource()) -> F() eqt(lock(),tag()) -> F() eqt(lock(),true()) -> F() eqt(lock(),tuple(H2,T2)) -> F() eqt(lock(),tuplenil(H2)) -> F() eqt(lock(),undefined()) -> F() eqt(locker(),a()) -> F() eqt(locker(),cons(H2,T2)) -> F() eqt(locker(),excl()) -> F() eqt(locker(),false()) -> F() eqt(locker(),int(N2)) -> F() eqt(locker(),lock()) -> F() eqt(locker(),locker()) -> T() eqt(locker(),mcrlrecord()) -> F() eqt(locker(),nil()) -> F() eqt(locker(),ok()) -> F() eqt(locker(),pending()) -> F() eqt(locker(),pid(N2)) -> F() eqt(locker(),release()) -> F() eqt(locker(),request()) -> F() eqt(locker(),resource()) -> F() eqt(locker(),tag()) -> F() eqt(locker(),true()) -> F() eqt(locker(),tuple(H2,T2)) -> F() eqt(locker(),tuplenil(H2)) -> F() eqt(locker(),undefined()) -> F() eqt(mcrlrecord(),a()) -> F() eqt(mcrlrecord(),excl()) -> F() eqt(mcrlrecord(),false()) -> F() eqt(mcrlrecord(),lock()) -> F() eqt(mcrlrecord(),locker()) -> F() eqt(mcrlrecord(),mcrlrecord()) -> T() eqt(mcrlrecord(),nil()) -> F() eqt(mcrlrecord(),ok()) -> F() eqt(mcrlrecord(),pending()) -> F() eqt(mcrlrecord(),release()) -> F() eqt(mcrlrecord(),request()) -> F() eqt(mcrlrecord(),resource()) -> F() eqt(nil(),cons(H2,T2)) -> F() eqt(nil(),int(N2)) -> F() eqt(nil(),pid(N2)) -> F() eqt(nil(),tuple(H2,T2)) -> F() eqt(nil(),tuplenil(H2)) -> F() eqt(nil(),undefined()) -> F() eqt(ok(),cons(H2,T2)) -> F() eqt(ok(),int(N2)) -> F() eqt(ok(),pid(N2)) -> F() eqt(ok(),resource()) -> F() eqt(ok(),tag()) -> F() eqt(ok(),true()) -> F() eqt(ok(),tuple(H2,T2)) -> F() eqt(ok(),tuplenil(H2)) -> F() eqt(ok(),undefined()) -> F() eqt(pending(),a()) -> F() eqt(pending(),cons(H2,T2)) -> F() eqt(pending(),excl()) -> F() eqt(pending(),false()) -> F() eqt(pending(),int(N2)) -> F() eqt(pending(),lock()) -> F() eqt(pending(),locker()) -> F() eqt(pending(),mcrlrecord()) -> F() eqt(pending(),nil()) -> F() eqt(pending(),ok()) -> F() eqt(pending(),pending()) -> T() eqt(pending(),pid(N2)) -> F() eqt(pending(),release()) -> F() eqt(pending(),request()) -> F() eqt(pending(),resource()) -> F() eqt(pending(),tag()) -> F() eqt(pending(),true()) -> F() eqt(pending(),tuple(H2,T2)) -> F() eqt(pending(),tuplenil(H2)) -> F() eqt(pending(),undefined()) -> F() eqt(pid(N1),a()) -> F() eqt(pid(N1),cons(H2,T2)) -> F() eqt(pid(N1),excl()) -> F() eqt(pid(N1),false()) -> F() eqt(pid(N1),int(N2)) -> F() eqt(pid(N1),lock()) -> F() eqt(pid(N1),locker()) -> F() eqt(pid(N1),mcrlrecord()) -> F() eqt(pid(N1),nil()) -> F() eqt(pid(N1),ok()) -> F() eqt(pid(N1),pending()) -> F() eqt(pid(N1),pid(N2)) -> eqt(N1,N2) eqt(pid(N1),release()) -> F() eqt(pid(N1),request()) -> F() eqt(pid(N1),resource()) -> F() eqt(pid(N1),tag()) -> F() eqt(pid(N1),true()) -> F() eqt(pid(N1),tuple(H2,T2)) -> F() eqt(pid(N1),tuplenil(H2)) -> F() eqt(pid(N1),undefined()) -> F() eqt(release(),a()) -> F() eqt(release(),excl()) -> F() eqt(release(),false()) -> F() eqt(release(),lock()) -> F() eqt(release(),locker()) -> F() eqt(release(),mcrlrecord()) -> F() eqt(release(),nil()) -> F() eqt(release(),ok()) -> F() eqt(request(),cons(H2,T2)) -> F() eqt(request(),int(N2)) -> F() eqt(request(),mcrlrecord()) -> F() eqt(request(),ok()) -> F() eqt(request(),pending()) -> F() eqt(request(),pid(N2)) -> F() eqt(request(),release()) -> F() eqt(request(),request()) -> T() eqt(request(),resource()) -> F() eqt(request(),tag()) -> F() eqt(request(),true()) -> F() eqt(request(),tuple(H2,T2)) -> F() eqt(request(),tuplenil(H2)) -> F() eqt(request(),undefined()) -> F() eqt(resource(),a()) -> F() eqt(resource(),cons(H2,T2)) -> F() eqt(resource(),excl()) -> F() eqt(resource(),false()) -> F() eqt(resource(),int(N2)) -> F() eqt(resource(),lock()) -> F() eqt(resource(),locker()) -> F() eqt(resource(),mcrlrecord()) -> F() eqt(resource(),nil()) -> F() eqt(resource(),ok()) -> F() eqt(resource(),pending()) -> F() eqt(resource(),pid(N2)) -> F() eqt(resource(),release()) -> F() eqt(resource(),request()) -> F() eqt(resource(),resource()) -> T() eqt(resource(),tag()) -> F() eqt(resource(),true()) -> F() eqt(resource(),tuple(H2,T2)) -> F() eqt(resource(),tuplenil(H2)) -> F() eqt(resource(),undefined()) -> F() eqt(tag(),a()) -> F() eqt(tag(),cons(H2,T2)) -> F() eqt(tag(),excl()) -> F() eqt(tag(),false()) -> F() eqt(tag(),int(N2)) -> F() eqt(tag(),lock()) -> F() eqt(tag(),locker()) -> F() eqt(tag(),mcrlrecord()) -> F() eqt(tag(),nil()) -> F() eqt(tag(),ok()) -> F() eqt(tag(),pending()) -> F() eqt(tag(),pid(N2)) -> F() eqt(tag(),release()) -> F() eqt(tag(),request()) -> F() eqt(tag(),resource()) -> F() eqt(tag(),tag()) -> T() eqt(tag(),true()) -> F() eqt(tag(),tuple(H2,T2)) -> F() eqt(tag(),tuplenil(H2)) -> F() eqt(tag(),undefined()) -> F() eqt(true(),a()) -> F() eqt(true(),cons(H2,T2)) -> F() eqt(true(),excl()) -> F() eqt(true(),false()) -> F() eqt(true(),int(N2)) -> F() eqt(true(),lock()) -> F() eqt(true(),locker()) -> F() eqt(true(),mcrlrecord()) -> F() eqt(true(),nil()) -> F() eqt(true(),ok()) -> F() eqt(true(),pending()) -> F() eqt(true(),pid(N2)) -> F() eqt(true(),release()) -> F() eqt(true(),request()) -> F() eqt(true(),resource()) -> F() eqt(true(),tag()) -> F() eqt(true(),true()) -> T() eqt(true(),tuple(H2,T2)) -> F() eqt(true(),tuplenil(H2)) -> F() eqt(true(),undefined()) -> F() eqt(tuple(H1,T1),a()) -> F() eqt(tuple(H1,T1),cons(H2,T2)) -> F() eqt(tuple(H1,T1),excl()) -> F() eqt(tuple(H1,T1),false()) -> F() eqt(tuple(H1,T1),int(N2)) -> F() eqt(tuple(H1,T1),lock()) -> F() eqt(tuple(H1,T1),locker()) -> F() eqt(tuple(H1,T1),mcrlrecord()) -> F() eqt(tuple(H1,T1),nil()) -> F() eqt(tuple(H1,T1),ok()) -> F() eqt(tuple(H1,T1),pending()) -> F() eqt(tuple(H1,T1),pid(N2)) -> F() eqt(tuple(H1,T1),release()) -> F() eqt(tuple(H1,T1),request()) -> F() eqt(tuple(H1,T1),resource()) -> F() eqt(tuple(H1,T1),tag()) -> F() eqt(tuple(H1,T1),true()) -> F() eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2)) eqt(tuple(H1,T1),tuplenil(H2)) -> F() eqt(tuple(H1,T1),undefined()) -> F() eqt(tuplenil(H1),a()) -> F() eqt(tuplenil(H1),cons(H2,T2)) -> F() eqt(tuplenil(H1),excl()) -> F() eqt(tuplenil(H1),false()) -> F() eqt(tuplenil(H1),int(N2)) -> F() eqt(tuplenil(H1),lock()) -> F() eqt(tuplenil(H1),locker()) -> F() eqt(tuplenil(H1),mcrlrecord()) -> F() eqt(tuplenil(H1),nil()) -> F() eqt(tuplenil(H1),ok()) -> F() eqt(tuplenil(H1),pending()) -> F() eqt(tuplenil(H1),pid(N2)) -> F() eqt(tuplenil(H1),release()) -> F() eqt(tuplenil(H1),request()) -> F() eqt(tuplenil(H1),resource()) -> F() eqt(tuplenil(H1),tag()) -> F() eqt(tuplenil(H1),true()) -> F() eqt(tuplenil(H1),tuple(H2,T2)) -> F() eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2) eqt(tuplenil(H1),undefined()) -> F() eqt(undefined(),a()) -> F() eqt(undefined(),nil()) -> F() eqt(undefined(),tuplenil(H2)) -> F() gen_modtageq(Client1,Client2) -> equal(Client1,Client2) gen_tag(Pid) -> tuple(Pid,tuplenil(tag())) if(F(),B1,B2) -> B2 if(T(),B1,B2) -> B1 imp(F(),B) -> T() imp(T(),B) -> B istops(E1,empty()) -> F() istops(E1,stack(E2,S1)) -> eqt(E1,E2) locker2_add_pending(Lock,Resources,Client) -> case1(Client ,Resources ,Lock ,member(record_extract(Lock,lock(),resource()),Resources)) locker2_adduniq(nil(),List) -> List locker2_check_available(Resource,cons(Lock,Locks)) -> case6(Locks ,Lock ,Resource ,equal(Resource ,record_extract(Lock,lock(),resource()))) locker2_check_available(Resource,nil()) -> false() locker2_check_availables(cons(Resource,Resources),Locks) -> andt(locker2_check_available(Resource,Locks) ,locker2_check_availables(Resources,Locks)) locker2_check_availables(nil(),Locks) -> true() locker2_map_add_pending(nil(),Resources,Client) -> nil() locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> cons(locker2_claim_lock(Lock,Resources,Client) ,locker2_map_claim_lock(Locks ,Resources ,Client)) locker2_map_claim_lock(nil(),Resources,Client) -> nil() locker2_map_promote_pending(cons(Lock,Locks),Pending) -> cons(locker2_promote_pending(Lock,Pending) ,locker2_map_promote_pending(Locks,Pending)) locker2_map_promote_pending(nil(),Pending) -> nil() locker2_obtainables(cons(Lock,Locks),Client) -> case5(Client ,Locks ,Lock ,member(Client,record_extract(Lock,lock(),pending()))) locker2_obtainables(nil(),Client) -> true() locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending())) locker2_release_lock(Lock,Client) -> case2(Client ,Lock ,gen_modtageq(Client,record_extract(Lock,lock(),excl()))) locker2_remove_pending(Lock,Client) -> record_updates(Lock ,lock() ,cons(tuple(pending() ,tuplenil(subtract(record_extract(Lock ,lock() ,pending()) ,cons(Client,nil())))) ,nil())) member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head)) member(E,nil()) -> false() not(F()) -> T() not(T()) -> F() or(F(),F()) -> F() or(F(),T()) -> T() or(T(),F()) -> T() or(T(),T()) -> T() pops(stack(E1,S1)) -> S1 push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3)) push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls()) push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1) pushs(E1,S1) -> stack(E1,S1) record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),resource()) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) record_new(lock()) -> tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil()))))) record_update(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))),lock(),pending(),NewF) -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(NewF))))) record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> record_updates(record_update(Record ,Name ,Field ,NewF) ,Name ,Fields) record_updates(Record,Name,nil()) -> Record subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail) subtract(List,nil()) -> List tops(stack(E1,S1)) -> E1 - Signature: {and/2,append/2,case0/3,case1/4,case2/3,case4/3,case5/4,case6/4,case8/4,case9/4,delete/2,element/2,eq/2 ,eqc/2,eqs/2,eqt/2,gen_modtageq/2,gen_tag/1,if/3,imp/2,istops/2,locker2_add_pending/3,locker2_adduniq/2 ,locker2_check_available/2,locker2_check_availables/2,locker2_map_add_pending/3,locker2_map_claim_lock/3 ,locker2_map_promote_pending/2,locker2_obtainables/2,locker2_promote_pending/2,locker2_release_lock/2 ,locker2_remove_pending/2,member/2,not/1,or/2,pops/1,push/3,push1/6,pushs/2,record_extract/3,record_new/1 ,record_update/4,record_updates/3,subtract/2,tops/1} / {0/0,F/0,T/0,a/0,andt/2,calls/3,cons/2,empty/0 ,equal/2,excl/0,excllock/0,false/0,int/1,lock/0,locker/0,locker2_claim_lock/3,locker2_obtainable/2 ,mcrlrecord/0,nil/0,nocalls/0,ok/0,pending/0,pid/1,release/0,request/0,resource/0,s/1,stack/2,tag/0,true/0 ,tuple/2,tuplenil/1,undefined/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,append,case0,case1,case2,case4,case5,case6,case8 ,case9,delete,element,eq,eqc,eqs,eqt,gen_modtageq,gen_tag,if,imp,istops,locker2_add_pending,locker2_adduniq ,locker2_check_available,locker2_check_availables,locker2_map_add_pending,locker2_map_claim_lock ,locker2_map_promote_pending,locker2_obtainables,locker2_promote_pending,locker2_release_lock ,locker2_remove_pending,member,not,or,pops,push,push1,pushs,record_extract,record_new,record_update ,record_updates,subtract,tops} and constructors {0,F,T,a,andt,calls,cons,empty,equal,excl,excllock,false,int ,lock,locker,locker2_claim_lock,locker2_obtainable,mcrlrecord,nil,nocalls,ok,pending,pid,release,request ,resource,s,stack,tag,true,tuple,tuplenil,undefined} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE