/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/mucrl1.trs

The program

(COMMENT 

  Xavier Urbain

  Obtained from a mu-crl specification given by Thomas Arts.

  See mucrl1.tes for a .tes format if this TRS

)


(VAR MCRLFree1  MCRLFree0  Client2  Client1  Pid  E  Tail  Head  List  Client  Resources  Resource  Locks  Lock  Pendings  Pending  Fields  Field  Name  Record  NewF  F2  F1  F0  T2  T1  H2  H1  N2  N1  E3  E2  E1  S2  S1  CS2  CS1  B2  B1  B)
(RULES

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

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend