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)).
+