% MESI Protocol [Delzanno 2003]
% MAP code
% MP - Nov 2007 


%Transitions

t(s(I,S,E,M),s(I,S,E,M)) :-		%rh
	I>=0,S>=0,M>=0,E>=0, 
	S+M+E>=1.

t(s(I,S,E,M),s(I1,S1,E1,M1)) :-		%rm
	S>=0,E>=0,M>=0,
	I>=1,
	I1=:=I-1, S1=:=S+E+M+1,	E1=:=0, M1=:=0.

t(s(I,S,E,M),s(I,S,E,M)) :-		%wh1
	I>=0,E>=0,S>=0,
	M>=1.

t(s(I,S,E,M),s(I,S,E1,M1)) :-		%wh2
  	I>=0,S>=0,M>=0,
	E>=1,
  	E1=:=E-1,M1=:=M+1.

t(s(I,S,E,M),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.

t(s(I,S,E,M),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.


%Elementary Propeties

elem(s(I,S,E,M),initial) :- I>=1,S=:=0,E=:=0,M=:=0.
elem(s(I,S,E,M),unsafe1) :- I>=0,S>=0,E>=0, M>=1,S+E>=1.
elem(s(I,S,E,M),unsafe2) :- I>=0,S>=0,E>=0, M>=2.
elem(s(I,S,E,M),unsafe3) :- I>=0,M>=0, E>=1,S>=1.
elem(s(I,S,E,M),unsafe4) :- I>=0,S>=0,M>=0, E>=2.


%Temporal Properties

safe1 :- prop(not(ef(unsafe1))).
safe2 :- prop(not(ef(unsafe2))).
safe3 :- prop(not(ef(unsafe3))).
safe4 :- prop(not(ef(unsafe4))).
safe :- prop(not(ef(or(unsafe1, or(unsafe2, or(unsafe3, unsafe4)))))).