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


% Transitions

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

t(s(I,D,S,E),s(I1,D,S,E1)) :-		%rm1
	I>=1,D=:=0,S=:=0,E=:=0,
	I1=:=I-1,E1=:=E+1.

t(s(I,D,S,E),s(I1,D1,S1,E1)) :-		%rm2
	D>=0,S>=0,E>=0,
	I>=1,D+S+E>=1,
	I1=:=I-1,D1=:=0,S1=:=S+D+E+1,E1=:=0.

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

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

t(s(I,D,S,E),s(I,D,S1,E1)) :-		%wh3
	I>=0,D>=0,E>=0,
	S=:=1,
	E1=:=E+1,S1=:=S-1.

t(s(I,D,S,E),s(I,D,S,E)) :-		%wh4
	I>=0,D>=0,E>=0,
	S>=2.

t(s(I,D,S,E),s(I1,D1,S1,E1)) :-		%wm
	D>=0,S>=0,E>=0,
	I>=1,	
	I1=:=I+D+S+E-1,D1=:=1,S1=:=0,E1=:=0.


%Elementary Properties

elem(s(I,D,S,E),initial) :- I>=1,D=:=0,S=:=0,E=:=0.

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


%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)))))).