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


% Transitions

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

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

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

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

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

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


%Elementary Properties

elem(s(I,S,E,O,M),initial) :- I>=0,S=:=0,E=:=0,M=:=0,O1=:=0.
elem(s(I,S,E,O,M),unsafe1) :- I>=0,S>=0,E>=0,O>=0, E+S+O>=1, M>=1.
elem(s(I,S,E,O,M),unsafe2) :- I>=0,S>=0,O>=0,M>=0, E>=1,S+O>=1.
elem(s(I,S,E,O,M),unsafe3) :- I>=0,S>=0,E>=0,O>=0, M>=2.
elem(s(I,S,E,O,M),unsafe4) :- I>=0,S>=0,O>=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)))))).