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

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

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

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

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

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

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

r(p(s_s,I,S,E,M),p(s_s,I,S,E1,M1), 		%wh2
    {I>=0,S>=0,M>=0,
     E>=1,
     E1=E-1,M1=M+1},5). 

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

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


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