Mercurial > hg > Applications > Tokio
diff Examples/etc/dekker @ 0:cfb7c6b24319
Initial revision
author | kono |
---|---|
date | Thu, 30 Aug 2007 14:57:44 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Examples/etc/dekker Thu Aug 30 14:57:44 2007 +0900 @@ -0,0 +1,37 @@ +'$define' progress(Cr1,Crit,Conc):- + #(Cr1=true),Crit + && @ (#(Cr1=false),Conc). + +'$define' ( exclusion(Id,Id2,T,Cr1,Cr2,Crit,Conc):- H ) +'$clause' ( H :- + Cr1=true, + enter(Id,Id2,T,Cr1,Cr2) + && progress(Cr1,Crit,Conc) + && @ H) . + +enter(Id,Id2,T,Cr1,Cr2) :- + Cr2=true,T=Id2,@Cr1=false, + @enter(Id,Id2,T,Cr1,Cr2). +enter(Id,Id2,T,Cr1,Cr2) :- + Cr2=true,T=Id,@Cr1=true,@T=Id, + @trust(Id,Id2,T,Cr1,Cr2). +enter(Id,Id2,T,Cr1,Cr2) :- + Cr2=false,@Cr1=true,skip. + +trust(Id,Id2,T,Cr1,Cr2) :-stable(T), + Cr2=true,@Cr1=true, + @trust(Id,Id2,T,Cr1,Cr2). +trust(Id,Id2,T,Cr1,Cr2) :- + Cr2=false,@Cr1=true,skip. + + +dekker:-T=0,Cr1=true,Cr2=true, + exclusion(0,1,T,Cr1,Cr2,critical(0),concurrent(0)), + exclusion(1,0,T,Cr2,Cr1,critical(1),concurrent(1)). + +critical(Id):-length(2), + keep((write('critical-region'),write(Id),nl)). + +concurrent(Id):-length(3), + keep((write('concurrent-region'),write(Id),nl)). +