%
% BERKELEY -- DMC Code [Delzanno 2003]
% MP - Nov 12, 2007

:-dynamic r/4.
:-dynamic info/4.

info(1,[p],4,[i,e,n,u]).

r(init,p(s_s,I,E,N,U),{I>=1,E=0,N=0,U=0},1).	%initial state

r(p(s_s,I,E,N,U),p(s_s,I1,E1,N1,U1),  		%rm
 {N>=0,E>=0,U>=0,I>=1, I1=I-1,U1=U+1,N1=N+E,E1=0},2).

r(p(s_s,I,E,N,U),p(s_s,I,E,N,U), 		%rh
 {N>=0,E>=0,U>=0,I>=0, E+N+U>=1},3).  

r(p(s_s,I,E,N,U),p(s_s,I1,E1,N1,U1),		%wm   
  {N>=0,E>=0,U>=0, I>=1, N1=0,E1=1,U1=0,I1=N+E+U+I-1},4).

r(p(s_s,I,E,N,U),p(s_s,I1,E1,N1,U1), 		%wh1
  {N>=0,E>=0,U>=0,I>=0,	N+U>=1,N1=0,E1=E+1,U1=0,I1=N+U+I-1},5).

r(p(s_s,I,E,N,U),p(s_s,I,E,N,U), 		%wh2
 {N>=0,U>=0,I>=0,E>=1},6).  

%unsafe12
prop(unsafe, p: s * (i>=0) * (e>=1) * (n>=0) * (u>=0) * (u+n >=1) + 
             p: s * (i>=0) * (e>=0) * (n>=2) * (u>=0)).