'$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)).