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


%Transitions

t(s(N,E,U,I),s(N1,E1,U1,I1)) :-	%rm
	N>=0,E>=0,U>=0,
	I>=1,
	N1=:=N+E,
	E1=:=0,
	U1=:=U+1,
	I1=:=I-1.

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

t(s(N,E,U,I),s(N1,E1,U1,I1)) :-	%wm
	N>=0,E>=0,U>=0,
	I>=1,
	N1=:=0,
	E1=:=1,
	U1=:=0,
	I1=:=N+E+U+I-1.

t(s(N,E,U,I),s(N1,E1,U1,I1)) :-	%wh1
	N>=0,E>=0,U>=0,I>=0,
	N+U>=1,
	N1=:=0,
	E1=:=E+1,
	U1=:=0,
	I1=:=N+U+I-1.

t(s(N,E,U,I),s(N,E,U,I)) :-	%wh2
	N>=0,U>=0,I>=0,
	E>=1.


%Elementary Properties

elem(s(N,E,U,I),initial) :- N=:=0,E=:=0,U=:=0,I>=1.
elem(s(N,E,U,I),unsafe1) :- N>=0,E>=1,U>=0,I>=0, N+U>=1.
elem(s(N,E,U,I),unsafe2) :- N>=0,E>=2,U>=0,I>=0.


%Temporal Properties

safe1 :- prop(not(ef(unsafe1))).
safe2 :- prop(not(ef(unsafe2))).
safe :- prop(not(ef(or(unsafe1,unsafe2)))).