%
% MOESI - DMC Code [Delzanno 2003]
% MP - Nov 20, 2007

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

info(1,[p],5,[i,s,e,o,m]).

r(init,p(s_s,I,S,E,O,M),{I>=0,S=0,E=0,O=0,M=0},1).	%initial state

r(p(s_s,I,S,E,O,M),p(s_s,I,S,E,O,M), 			%Rh
    {I>=0,S>=0,E>=0,O>=0,M>=0,
     S+E+O+M>=1},2). 

r(p(s_s,I,S,E,O,M),p(s_s,I1,S1,E1,O1,M1), 		%Rm
   {S>=0,E>=0,M>=0,O>=0,
    I>=1,
    I1=I-1,S1=S+E+1,O1=O+M,E1=0,M1=0},3).

r(p(s_s,I,S,E,O,M),p(s_s,I,S,E,O,M), 		%wh1: subsumed by Rh
    {I>=0,E>=0,S>=0,O>=0,
     M>=1},4). 

r(p(s_s,I,S,E,O,M),p(s_s,I,S,E1,O,M1), 			%wh2
    {I>=0,S>=0,M>=0,
     E>=1,
     E1=E-1,M1=M+1},5).
	
r(p(s_s,I,S,E,O,M),p(s_s,I1,S1,E1,O1,M1), 		%wh3
    {I>=0,S>=0,O>=0,M>=0,E>=0,
     S+O>=1,
     I1=I+O+M+E+S-1,E1=1,M1=0,O1=0,S1=0},6).
	 
r(p(s_s,I,S,E,O,M),p(s_s,I1,S1,E1,O1,M1), 		%wm
   {S>=0,E>=0,M>=0,O>=0,
    I>=1, 
    I1=I+O+S+E+M-1,S1=0,E1=1,M1=0,O1=0},7).

%unsafe1
%prop(unsafe,p:s * (i>=0) * (s>=0) * (e>=0) * (o>=0) * (m>=1) * (e+s+o>=1)).
%unsafe2
%prop(unsafe,p:s * (i>=0) * (s>=0) * (e>=1) * (o>=0) * (m>=0) * (s+o>=1)).

%unsafe3
%prop(unsafe,p:s * (i>=0) * (s>=0) * (e>=0) * (o>=0) * (m>=2) ).

%unsafe4
%prop(unsafe,p:s * (i>=0) * (s>=0) * (e>=2) * (o>=0) * (m>=0) ).

%unsafe14
prop(unsafe,p:s * (i>=0) * (s>=0) * (e>=0) * (o>=0) * (m>=1) * (e+s+o>=1) +
            p:s * (i>=0) * (s>=0) * (e>=1) * (o>=0) * (m>=0) * (s+o>=1) +
            p:s * (i>=0) * (s>=0) * (e>=0) * (o>=0) * (m>=2) +
            p:s * (i>=0) * (s>=0) * (e>=2) * (o>=0) * (m>=0) ).