* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ 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:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ 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:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
append(y,z){y -> cons(x,y)} =
append(cons(x,y),z) ->^+ cons(x,append(y,z))
= C[append(y,z) = append(y,z){}]
WORST_CASE(Omega(n^1),?)