MAYBE 0.38/0.44 MAYBE 0.38/0.45 0.38/0.45 Problem: 0.38/0.45 or(T(),T()) -> T() 0.38/0.45 or(F(),T()) -> T() 0.38/0.45 or(T(),F()) -> T() 0.38/0.45 or(F(),F()) -> F() 0.38/0.45 and(T(),B) -> B 0.38/0.45 and(B,T()) -> B 0.38/0.45 and(F(),B) -> F() 0.38/0.45 and(B,F()) -> F() 0.38/0.45 imp(T(),B) -> B 0.38/0.45 imp(F(),B) -> T() 0.38/0.45 not(T()) -> F() 0.38/0.45 not(F()) -> T() 0.38/0.45 if(T(),B1,B2) -> B1 0.38/0.45 if(F(),B1,B2) -> B2 0.38/0.45 eq(T(),T()) -> T() 0.38/0.45 eq(F(),F()) -> T() 0.38/0.45 eq(T(),F()) -> F() 0.38/0.45 eq(F(),T()) -> F() 0.38/0.45 eqt(nil(),undefined()) -> F() 0.38/0.45 eqt(nil(),pid(N2)) -> F() 0.38/0.45 eqt(nil(),int(N2)) -> F() 0.38/0.45 eqt(nil(),cons(H2,T2)) -> F() 0.38/0.45 eqt(nil(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(nil(),tuplenil(H2)) -> F() 0.38/0.45 eqt(a(),nil()) -> F() 0.38/0.45 eqt(a(),a()) -> T() 0.38/0.45 eqt(a(),excl()) -> F() 0.38/0.45 eqt(a(),false()) -> F() 0.38/0.45 eqt(a(),lock()) -> F() 0.38/0.45 eqt(a(),locker()) -> F() 0.38/0.45 eqt(a(),mcrlrecord()) -> F() 0.38/0.45 eqt(a(),ok()) -> F() 0.38/0.45 eqt(a(),pending()) -> F() 0.38/0.45 eqt(a(),release()) -> F() 0.38/0.45 eqt(a(),request()) -> F() 0.38/0.45 eqt(a(),resource()) -> F() 0.38/0.45 eqt(a(),tag()) -> F() 0.38/0.45 eqt(a(),true()) -> F() 0.38/0.45 eqt(a(),undefined()) -> F() 0.38/0.45 eqt(a(),pid(N2)) -> F() 0.38/0.45 eqt(a(),int(N2)) -> F() 0.38/0.45 eqt(a(),cons(H2,T2)) -> F() 0.38/0.45 eqt(a(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(a(),tuplenil(H2)) -> F() 0.38/0.45 eqt(excl(),nil()) -> F() 0.38/0.45 eqt(excl(),a()) -> F() 0.38/0.45 eqt(excl(),excl()) -> T() 0.38/0.45 eqt(excl(),false()) -> F() 0.38/0.45 eqt(excl(),lock()) -> F() 0.38/0.45 eqt(excl(),locker()) -> F() 0.38/0.45 eqt(excl(),mcrlrecord()) -> F() 0.38/0.45 eqt(excl(),ok()) -> F() 0.38/0.45 eqt(excl(),pending()) -> F() 0.38/0.45 eqt(excl(),release()) -> F() 0.38/0.45 eqt(excl(),request()) -> F() 0.38/0.45 eqt(excl(),resource()) -> F() 0.38/0.45 eqt(excl(),tag()) -> F() 0.38/0.45 eqt(excl(),true()) -> F() 0.38/0.45 eqt(excl(),undefined()) -> F() 0.38/0.45 eqt(excl(),pid(N2)) -> F() 0.38/0.45 eqt(excl(),eqt(false(),int(N2))) -> F() 0.38/0.45 eqt(false(),cons(H2,T2)) -> F() 0.38/0.45 eqt(false(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(false(),tuplenil(H2)) -> F() 0.38/0.45 eqt(lock(),nil()) -> F() 0.38/0.45 eqt(lock(),a()) -> F() 0.38/0.45 eqt(lock(),excl()) -> F() 0.38/0.45 eqt(lock(),false()) -> F() 0.38/0.45 eqt(lock(),lock()) -> T() 0.38/0.45 eqt(lock(),locker()) -> F() 0.38/0.45 eqt(lock(),mcrlrecord()) -> F() 0.38/0.45 eqt(lock(),ok()) -> F() 0.38/0.45 eqt(lock(),pending()) -> F() 0.38/0.45 eqt(lock(),release()) -> F() 0.38/0.45 eqt(lock(),request()) -> F() 0.38/0.45 eqt(lock(),resource()) -> F() 0.38/0.45 eqt(lock(),tag()) -> F() 0.38/0.45 eqt(lock(),true()) -> F() 0.38/0.45 eqt(lock(),undefined()) -> F() 0.38/0.45 eqt(lock(),pid(N2)) -> F() 0.38/0.45 eqt(lock(),int(N2)) -> F() 0.38/0.45 eqt(lock(),cons(H2,T2)) -> F() 0.38/0.45 eqt(lock(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(lock(),tuplenil(H2)) -> F() 0.38/0.45 eqt(locker(),nil()) -> F() 0.38/0.45 eqt(locker(),a()) -> F() 0.38/0.45 eqt(locker(),excl()) -> F() 0.38/0.45 eqt(locker(),false()) -> F() 0.38/0.45 eqt(locker(),lock()) -> F() 0.38/0.45 eqt(locker(),locker()) -> T() 0.38/0.45 eqt(locker(),mcrlrecord()) -> F() 0.38/0.45 eqt(locker(),ok()) -> F() 0.38/0.45 eqt(locker(),pending()) -> F() 0.38/0.45 eqt(locker(),release()) -> F() 0.38/0.45 eqt(locker(),request()) -> F() 0.38/0.45 eqt(locker(),resource()) -> F() 0.38/0.45 eqt(locker(),tag()) -> F() 0.38/0.45 eqt(locker(),true()) -> F() 0.38/0.45 eqt(locker(),undefined()) -> F() 0.38/0.45 eqt(locker(),pid(N2)) -> F() 0.38/0.45 eqt(locker(),int(N2)) -> F() 0.38/0.45 eqt(locker(),cons(H2,T2)) -> F() 0.38/0.45 eqt(locker(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(locker(),tuplenil(H2)) -> F() 0.38/0.45 eqt(mcrlrecord(),nil()) -> F() 0.38/0.45 eqt(mcrlrecord(),a()) -> F() 0.38/0.45 eqt(mcrlrecord(),excl()) -> F() 0.38/0.45 eqt(mcrlrecord(),false()) -> F() 0.38/0.45 eqt(mcrlrecord(),lock()) -> F() 0.38/0.45 eqt(mcrlrecord(),locker()) -> F() 0.38/0.45 eqt(mcrlrecord(),mcrlrecord()) -> T() 0.38/0.45 eqt(mcrlrecord(),ok()) -> F() 0.38/0.45 eqt(mcrlrecord(),pending()) -> F() 0.38/0.45 eqt(mcrlrecord(),release()) -> F() 0.38/0.45 eqt(mcrlrecord(),request()) -> F() 0.38/0.45 eqt(mcrlrecord(),resource()) -> F() 0.38/0.45 eqt(ok(),resource()) -> F() 0.38/0.45 eqt(ok(),tag()) -> F() 0.38/0.45 eqt(ok(),true()) -> F() 0.38/0.45 eqt(ok(),undefined()) -> F() 0.38/0.45 eqt(ok(),pid(N2)) -> F() 0.38/0.45 eqt(ok(),int(N2)) -> F() 0.38/0.45 eqt(ok(),cons(H2,T2)) -> F() 0.38/0.45 eqt(ok(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(ok(),tuplenil(H2)) -> F() 0.38/0.45 eqt(pending(),nil()) -> F() 0.38/0.45 eqt(pending(),a()) -> F() 0.38/0.45 eqt(pending(),excl()) -> F() 0.38/0.45 eqt(pending(),false()) -> F() 0.38/0.45 eqt(pending(),lock()) -> F() 0.38/0.45 eqt(pending(),locker()) -> F() 0.38/0.45 eqt(pending(),mcrlrecord()) -> F() 0.38/0.45 eqt(pending(),ok()) -> F() 0.38/0.45 eqt(pending(),pending()) -> T() 0.38/0.45 eqt(pending(),release()) -> F() 0.38/0.45 eqt(pending(),request()) -> F() 0.38/0.45 eqt(pending(),resource()) -> F() 0.38/0.45 eqt(pending(),tag()) -> F() 0.38/0.45 eqt(pending(),true()) -> F() 0.38/0.45 eqt(pending(),undefined()) -> F() 0.38/0.45 eqt(pending(),pid(N2)) -> F() 0.38/0.45 eqt(pending(),int(N2)) -> F() 0.38/0.45 eqt(pending(),cons(H2,T2)) -> F() 0.38/0.45 eqt(pending(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(pending(),tuplenil(H2)) -> F() 0.38/0.45 eqt(release(),nil()) -> F() 0.38/0.45 eqt(release(),a()) -> F() 0.38/0.45 eqt(release(),excl()) -> F() 0.38/0.45 eqt(release(),false()) -> F() 0.38/0.45 eqt(release(),lock()) -> F() 0.38/0.45 eqt(release(),locker()) -> F() 0.38/0.45 eqt(release(),mcrlrecord()) -> F() 0.38/0.45 eqt(release(),ok()) -> F() 0.38/0.45 eqt(request(),mcrlrecord()) -> F() 0.38/0.45 eqt(request(),ok()) -> F() 0.38/0.45 eqt(request(),pending()) -> F() 0.38/0.45 eqt(request(),release()) -> F() 0.38/0.45 eqt(request(),request()) -> T() 0.38/0.45 eqt(request(),resource()) -> F() 0.38/0.45 eqt(request(),tag()) -> F() 0.38/0.45 eqt(request(),true()) -> F() 0.38/0.45 eqt(request(),undefined()) -> F() 0.38/0.45 eqt(request(),pid(N2)) -> F() 0.38/0.45 eqt(request(),int(N2)) -> F() 0.38/0.45 eqt(request(),cons(H2,T2)) -> F() 0.38/0.45 eqt(request(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(request(),tuplenil(H2)) -> F() 0.38/0.45 eqt(resource(),nil()) -> F() 0.38/0.45 eqt(resource(),a()) -> F() 0.38/0.45 eqt(resource(),excl()) -> F() 0.38/0.45 eqt(resource(),false()) -> F() 0.38/0.45 eqt(resource(),lock()) -> F() 0.38/0.45 eqt(resource(),locker()) -> F() 0.38/0.45 eqt(resource(),mcrlrecord()) -> F() 0.38/0.45 eqt(resource(),ok()) -> F() 0.38/0.45 eqt(resource(),pending()) -> F() 0.38/0.45 eqt(resource(),release()) -> F() 0.38/0.45 eqt(resource(),request()) -> F() 0.38/0.45 eqt(resource(),resource()) -> T() 0.38/0.45 eqt(resource(),tag()) -> F() 0.38/0.45 eqt(resource(),true()) -> F() 0.38/0.45 eqt(resource(),undefined()) -> F() 0.38/0.45 eqt(resource(),pid(N2)) -> F() 0.38/0.45 eqt(resource(),int(N2)) -> F() 0.38/0.45 eqt(resource(),cons(H2,T2)) -> F() 0.38/0.45 eqt(resource(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(resource(),tuplenil(H2)) -> F() 0.38/0.45 eqt(tag(),nil()) -> F() 0.38/0.45 eqt(tag(),a()) -> F() 0.38/0.45 eqt(tag(),excl()) -> F() 0.38/0.45 eqt(tag(),false()) -> F() 0.38/0.45 eqt(tag(),lock()) -> F() 0.38/0.45 eqt(tag(),locker()) -> F() 0.38/0.45 eqt(tag(),mcrlrecord()) -> F() 0.38/0.45 eqt(tag(),ok()) -> F() 0.38/0.45 eqt(tag(),pending()) -> F() 0.38/0.45 eqt(tag(),release()) -> F() 0.38/0.45 eqt(tag(),request()) -> F() 0.38/0.45 eqt(tag(),resource()) -> F() 0.38/0.45 eqt(tag(),tag()) -> T() 0.38/0.45 eqt(tag(),true()) -> F() 0.38/0.45 eqt(tag(),undefined()) -> F() 0.38/0.45 eqt(tag(),pid(N2)) -> F() 0.38/0.45 eqt(tag(),int(N2)) -> F() 0.38/0.45 eqt(tag(),cons(H2,T2)) -> F() 0.38/0.45 eqt(tag(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(tag(),tuplenil(H2)) -> F() 0.38/0.45 eqt(true(),nil()) -> F() 0.38/0.45 eqt(true(),a()) -> F() 0.38/0.45 eqt(true(),excl()) -> F() 0.38/0.45 eqt(true(),false()) -> F() 0.38/0.45 eqt(true(),lock()) -> F() 0.38/0.45 eqt(true(),locker()) -> F() 0.38/0.45 eqt(true(),mcrlrecord()) -> F() 0.38/0.45 eqt(true(),ok()) -> F() 0.38/0.45 eqt(true(),pending()) -> F() 0.38/0.45 eqt(true(),release()) -> F() 0.38/0.45 eqt(true(),request()) -> F() 0.38/0.45 eqt(true(),resource()) -> F() 0.38/0.45 eqt(true(),tag()) -> F() 0.38/0.45 eqt(true(),true()) -> T() 0.38/0.45 eqt(true(),undefined()) -> F() 0.38/0.45 eqt(true(),pid(N2)) -> F() 0.38/0.45 eqt(true(),int(N2)) -> F() 0.38/0.45 eqt(true(),cons(H2,T2)) -> F() 0.38/0.45 eqt(true(),tuple(H2,T2)) -> F() 0.38/0.45 eqt(true(),tuplenil(H2)) -> F() 0.38/0.45 eqt(undefined(),nil()) -> F() 0.38/0.45 eqt(undefined(),a()) -> F() 0.38/0.45 eqt(undefined(),tuplenil(H2)) -> F() 0.38/0.45 eqt(pid(N1),nil()) -> F() 0.38/0.45 eqt(pid(N1),a()) -> F() 0.38/0.45 eqt(pid(N1),excl()) -> F() 0.38/0.45 eqt(pid(N1),false()) -> F() 0.38/0.45 eqt(pid(N1),lock()) -> F() 0.38/0.45 eqt(pid(N1),locker()) -> F() 0.38/0.45 eqt(pid(N1),mcrlrecord()) -> F() 0.38/0.45 eqt(pid(N1),ok()) -> F() 0.38/0.45 eqt(pid(N1),pending()) -> F() 0.38/0.45 eqt(pid(N1),release()) -> F() 0.38/0.45 eqt(pid(N1),request()) -> F() 0.38/0.45 eqt(pid(N1),resource()) -> F() 0.38/0.45 eqt(pid(N1),tag()) -> F() 0.38/0.45 eqt(pid(N1),true()) -> F() 0.38/0.45 eqt(pid(N1),undefined()) -> F() 0.38/0.46 eqt(pid(N1),pid(N2)) -> eqt(N1,N2) 0.38/0.46 eqt(pid(N1),int(N2)) -> F() 0.38/0.46 eqt(pid(N1),cons(H2,T2)) -> F() 0.38/0.46 eqt(pid(N1),tuple(H2,T2)) -> F() 0.38/0.46 eqt(pid(N1),tuplenil(H2)) -> F() 0.38/0.46 eqt(int(N1),nil()) -> F() 0.38/0.46 eqt(int(N1),a()) -> F() 0.38/0.46 eqt(int(N1),excl()) -> F() 0.38/0.46 eqt(int(N1),false()) -> F() 0.38/0.46 eqt(int(N1),lock()) -> F() 0.38/0.46 eqt(int(N1),locker()) -> F() 0.38/0.46 eqt(int(N1),mcrlrecord()) -> F() 0.38/0.46 eqt(int(N1),ok()) -> F() 0.38/0.46 eqt(int(N1),pending()) -> F() 0.38/0.46 eqt(int(N1),release()) -> F() 0.38/0.46 eqt(int(N1),request()) -> F() 0.38/0.46 eqt(int(N1),resource()) -> F() 0.38/0.46 eqt(int(N1),tag()) -> F() 0.38/0.46 eqt(int(N1),true()) -> F() 0.38/0.46 eqt(int(N1),undefined()) -> F() 0.38/0.46 eqt(cons(H1,T1),resource()) -> F() 0.38/0.46 eqt(cons(H1,T1),tag()) -> F() 0.38/0.46 eqt(cons(H1,T1),true()) -> F() 0.38/0.46 eqt(cons(H1,T1),undefined()) -> F() 0.38/0.46 eqt(cons(H1,T1),pid(N2)) -> F() 0.38/0.46 eqt(cons(H1,T1),int(N2)) -> F() 0.38/0.46 eqt(cons(H1,T1),cons(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2)) 0.38/0.46 eqt(cons(H1,T1),tuple(H2,T2)) -> F() 0.38/0.46 eqt(cons(H1,T1),tuplenil(H2)) -> F() 0.38/0.46 eqt(tuple(H1,T1),nil()) -> F() 0.38/0.46 eqt(tuple(H1,T1),a()) -> F() 0.38/0.46 eqt(tuple(H1,T1),excl()) -> F() 0.38/0.46 eqt(tuple(H1,T1),false()) -> F() 0.38/0.46 eqt(tuple(H1,T1),lock()) -> F() 0.38/0.46 eqt(tuple(H1,T1),locker()) -> F() 0.38/0.46 eqt(tuple(H1,T1),mcrlrecord()) -> F() 0.38/0.46 eqt(tuple(H1,T1),ok()) -> F() 0.38/0.46 eqt(tuple(H1,T1),pending()) -> F() 0.38/0.46 eqt(tuple(H1,T1),release()) -> F() 0.38/0.46 eqt(tuple(H1,T1),request()) -> F() 0.38/0.46 eqt(tuple(H1,T1),resource()) -> F() 0.38/0.46 eqt(tuple(H1,T1),tag()) -> F() 0.38/0.46 eqt(tuple(H1,T1),true()) -> F() 0.38/0.46 eqt(tuple(H1,T1),undefined()) -> F() 0.38/0.46 eqt(tuple(H1,T1),pid(N2)) -> F() 0.38/0.46 eqt(tuple(H1,T1),int(N2)) -> F() 0.38/0.46 eqt(tuple(H1,T1),cons(H2,T2)) -> F() 0.38/0.46 eqt(tuple(H1,T1),tuple(H2,T2)) -> and(eqt(H1,H2),eqt(T1,T2)) 0.38/0.46 eqt(tuple(H1,T1),tuplenil(H2)) -> F() 0.38/0.46 eqt(tuplenil(H1),nil()) -> F() 0.38/0.46 eqt(tuplenil(H1),a()) -> F() 0.38/0.46 eqt(tuplenil(H1),excl()) -> F() 0.38/0.46 eqt(tuplenil(H1),false()) -> F() 0.38/0.46 eqt(tuplenil(H1),lock()) -> F() 0.38/0.46 eqt(tuplenil(H1),locker()) -> F() 0.38/0.46 eqt(tuplenil(H1),mcrlrecord()) -> F() 0.38/0.46 eqt(tuplenil(H1),ok()) -> F() 0.38/0.46 eqt(tuplenil(H1),pending()) -> F() 0.38/0.46 eqt(tuplenil(H1),release()) -> F() 0.38/0.46 eqt(tuplenil(H1),request()) -> F() 0.38/0.46 eqt(tuplenil(H1),resource()) -> F() 0.38/0.46 eqt(tuplenil(H1),tag()) -> F() 0.38/0.46 eqt(tuplenil(H1),true()) -> F() 0.38/0.46 eqt(tuplenil(H1),undefined()) -> F() 0.38/0.46 eqt(tuplenil(H1),pid(N2)) -> F() 0.38/0.46 eqt(tuplenil(H1),int(N2)) -> F() 0.38/0.46 eqt(tuplenil(H1),cons(H2,T2)) -> F() 0.38/0.46 eqt(tuplenil(H1),tuple(H2,T2)) -> F() 0.38/0.46 eqt(tuplenil(H1),tuplenil(H2)) -> eqt(H1,H2) 0.38/0.46 element(int(s(0())),tuplenil(T1)) -> T1 0.38/0.46 element(int(s(0())),tuple(T1,T2)) -> T1 0.38/0.46 element(int(s(s(N1))),tuple(T1,T2)) -> element(int(s(N1)),T2) 0.38/0.46 record_new(lock()) -> 0.38/0.46 tuple(mcrlrecord(),tuple(lock(),tuple(undefined(),tuple(nil(),tuplenil(nil()))))) 0.38/0.46 record_extract(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), 0.38/0.46 lock(),resource()) 0.38/0.46 -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))) 0.38/0.46 record_update(tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(F2))))), 0.38/0.46 lock(),pending(),NewF) 0.38/0.46 -> tuple(mcrlrecord(),tuple(lock(),tuple(F0,tuple(F1,tuplenil(NewF))))) 0.38/0.46 record_updates(Record,Name,nil()) -> Record 0.38/0.46 record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) -> 0.38/0.46 record_updates(record_update(Record,Name,Field,NewF),Name,Fields) 0.38/0.46 locker2_map_promote_pending(nil(),Pending) -> nil() 0.38/0.46 locker2_map_promote_pending(cons(Lock,Locks),Pending) -> 0.38/0.46 cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending)) 0.38/0.46 locker2_map_claim_lock(nil(),Resources,Client) -> nil() 0.38/0.46 locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) -> 0.38/0.46 cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client)) 0.38/0.46 locker2_map_add_pending(nil(),Resources,Client) -> nil() 0.38/0.46 locker2_promote_pending(Lock,Client) -> case0(Client,Lock,record_extract(Lock,lock(),pending())) 0.38/0.46 case0(Client,Lock,cons(Client,Pendings)) -> 0.38/0.46 record_updates(Lock,lock(),cons(tuple(excl(),tuplenil(Client)),cons( 0.38/0.46 tuple 0.38/0.46 ( 0.38/0.46 pending(),tuplenil(Pendings)), 0.38/0.46 nil 0.38/0.46 ()))) 0.38/0.46 case0(Client,Lock,MCRLFree0) -> Lock 0.38/0.46 locker2_remove_pending(Lock,Client) -> 0.38/0.46 record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(subtract(record_extract 0.38/0.46 (Lock,lock(),pending()), 0.38/0.46 cons 0.38/0.46 (Client,nil())))), 0.38/0.46 nil())) 0.38/0.46 locker2_add_pending(Lock,Resources,Client) -> 0.38/0.46 case1(Client,Resources,Lock,member(record_extract(Lock,lock(),resource()),Resources)) 0.38/0.46 case1(Client,Resources,Lock,true()) -> 0.38/0.46 record_updates(Lock,lock(),cons(tuple(pending(),tuplenil(append(record_extract 0.38/0.46 (Lock,lock(),pending()), 0.38/0.46 cons 0.38/0.46 (Client,nil())))), 0.38/0.46 nil())) 0.38/0.46 case1(Client,Resources,Lock,false()) -> Lock 0.38/0.46 locker2_release_lock(Lock,Client) -> 0.38/0.46 case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock(),excl()))) 0.38/0.46 case2(Client,Lock,true()) -> record_updates(Lock,lock(),cons(tuple(excllock(),excl()),nil())) 0.38/0.46 case4(Client,Lock,MCRLFree1) -> false() 0.38/0.46 locker2_obtainables(nil(),Client) -> true() 0.38/0.46 locker2_obtainables(cons(Lock,Locks),Client) -> 0.38/0.46 case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock(),pending()))) 0.38/0.46 case5(Client,Locks,Lock,true()) -> 0.38/0.46 andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client)) 0.38/0.46 case5(Client,Locks,Lock,false()) -> locker2_obtainables(Locks,Client) 0.38/0.46 locker2_check_available(Resource,nil()) -> false() 0.38/0.46 locker2_check_available(Resource,cons(Lock,Locks)) -> 0.38/0.46 case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock(),resource()))) 0.38/0.46 case6(Locks,Lock,Resource,true()) -> 0.38/0.46 andt(equal(record_extract(Lock,lock(),excl()),nil()),equal(record_extract(Lock,lock(),pending()), 0.38/0.46 nil())) 0.38/0.46 case6(Locks,Lock,Resource,false()) -> locker2_check_available(Resource,Locks) 0.38/0.46 locker2_check_availables(nil(),Locks) -> true() 0.38/0.46 locker2_check_availables(cons(Resource,Resources),Locks) -> 0.38/0.46 andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks)) 0.38/0.46 locker2_adduniq(nil(),List) -> List 0.38/0.46 append(cons(Head,Tail),List) -> cons(Head,append(Tail,List)) 0.38/0.46 subtract(List,nil()) -> List 0.38/0.46 subtract(List,cons(Head,Tail)) -> subtract(delete(Head,List),Tail) 0.38/0.46 delete(E,nil()) -> nil() 0.38/0.46 delete(E,cons(Head,Tail)) -> case8(Tail,Head,E,equal(E,Head)) 0.38/0.46 case8(Tail,Head,E,true()) -> Tail 0.38/0.46 case8(Tail,Head,E,false()) -> cons(Head,delete(E,Tail)) 0.38/0.46 gen_tag(Pid) -> tuple(Pid,tuplenil(tag())) 0.38/0.46 gen_modtageq(Client1,Client2) -> equal(Client1,Client2) 0.38/0.46 member(E,nil()) -> false() 0.38/0.46 member(E,cons(Head,Tail)) -> case9(Tail,Head,E,equal(E,Head)) 0.38/0.46 case9(Tail,Head,E,true()) -> true() 0.38/0.46 case9(Tail,Head,E,false()) -> member(E,Tail) 0.38/0.46 eqs(empty(),empty()) -> T() 0.38/0.46 eqs(empty(),stack(E2,S2)) -> F() 0.38/0.46 eqs(stack(E1,S1),empty()) -> F() 0.38/0.46 eqs(stack(E1,S1),stack(E2,S2)) -> and(eqt(E1,E2),eqs(S1,S2)) 0.38/0.46 pushs(E1,S1) -> stack(E1,S1) 0.38/0.46 pops(stack(E1,S1)) -> S1 0.38/0.46 tops(stack(E1,S1)) -> E1 0.38/0.46 istops(E1,empty()) -> F() 0.38/0.46 istops(E1,stack(E2,S1)) -> eqt(E1,E2) 0.38/0.46 eqc(nocalls(),nocalls()) -> T() 0.38/0.46 eqc(nocalls(),calls(E2,S2,CS2)) -> F() 0.38/0.46 eqc(calls(E1,S1,CS1),nocalls()) -> F() 0.38/0.46 eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) -> and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) 0.38/0.46 push(E1,E2,nocalls()) -> calls(E1,stack(E2,empty()),nocalls()) 0.38/0.46 push(E1,E2,calls(E3,S1,CS1)) -> push1(E1,E2,E3,S1,CS1,eqt(E1,E3)) 0.38/0.46 push1(E1,E2,E3,S1,CS1,T()) -> calls(E3,pushs(E2,S1),CS1) 0.38/0.46 0.38/0.46 Proof: 0.38/0.46 Open 0.38/0.46 EOF