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


% Transitions

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

t(s(I,V,D),s(I1,V1,D1)) :-		%rm
	V>=0,D>=0,
	I>=1,
	I1=:=I+D-1,V1=:=V+1,D1=:=0.

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

t(s(I,V,D),s(I1,V1,D1)) :-		%wh2
	I>=0,D>=0,
	V>=1,
	I1=:=I+D+V-1,V1=:=0,D1=:=1.

t(s(I,V,D),s(I1,V1,D1)) :-		%wm
	V>=0,D>=0,
	I>=1,
	I1=:=I+D+V-1,V1=:=0,D1=:=1.


% Elementary Properties

elem(s(I,V,D),initial) :- I>=0, V=:=0,D=:=0.
elem(s(I,V,D),unsafe1) :- I>=0, V>=1, D>=1.
elem(s(I,V,D),unsafe2) :- I>=0, V>=0, D>=2.


% Temporal Properties

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