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

%Transitions

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

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

t(s(I,D,E,SC,SD),s(I1,D1,E1,SC1,SD1)) :-		%rm2
	D>=0,SC>=0,SD>=0,E>=0,
	I>=1,D+E+SC+SD>=1,
	I1=:=I-1,D1=:=0,E1=:=0,SC1=:=SC+E+1,SD1=:=SD+D.

t(s(I,D,E,SC,SD),s(I1,D1,E,SC,SD)) :-		%wm1
	I>=1,D=:=0,SC=:=0,E=:=0,SD=:=0,
	I1=:=I-1,D1=:=D+1.

t(s(I,D,E,SC,SD),s(I1,D1,E1,SC1,SD1)) :-		%wm2
	D>=0,SC>=0,SD>=0,E>=0,
	I>=1,D+E+SC+SD>=1,
	I1=:=I-1,D1=:=0,E1=:=0,SC1=:=SC+E+D+SD,SD1=:=1.

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

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

t(s(I,D,E,SC,SD),s(I,D1,E,SC,SD1)) :-		%wh3
	E>=0,I>=0,D>=0,
	SD=:=1,SC=:=0,
	SD1=:=0,D1=:=D+1.

t(s(I,D,E,SC,SD),s(I,D1,E,SC1,SD)) :-		%wh4
	E>=0,I>=0,D>=0,
	SC=:=1,SD=:=0,
	SC1=:=0,D1=:=D+1.

t(s(I,D,E,SC,SD),s(I,D,E,SC1,SD1)) :-		%wh5
	E>=0,I>=0,D>=0,SC>=0,SD>=0,
	SC+SD>=2,
	SC1=:=SC+SD-1,SD1=:=1.

%Elementary Properties

elem(s(I,D,E,SC,SD),initial) :- I>=1,D=:=0,E=:=0,SC=:=0,SD=:=0.
elem(s(I,D,E,SC,SD),unsafe1) :- I>=0,E>=0,SC>=0,SD>=0, E+SC+SD>=1,D>=1.
elem(s(I,D,E,SC,SD),unsafe2) :- I>=0,D>=0,SC>=0,SD>=0, E>=1, SC+SD>=1.
elem(s(I,D,E,SC,SD),unsafe3) :- I>=0,E>=0,SC>=0,SD>=0, D>=2.
elem(s(I,D,E,SC,SD),unsafe4) :- I>=0,D>=0,SC>=0,SD>=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(or(ef(unsafe1),or(unsafe2,or(unsafe3,unsafe4))))).