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


% Transitions

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

t(s(I,D,S,E),s(I1,D,S,E1)) :-			%r2
	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)) :-			%r3
	I>=1,D>=0,S>=0,E>=0,D+S+E>=1,
     	I1=:=I-1,D1=:=0,S1=:=D+S+E+1,E1=:=0.

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

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

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

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

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

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


%Elementery 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, D>=1, S>=0, E>=0, S+E>=1.
elem(s(I,D,S,E),unsafe2) :- I>=0, D>=2, S>=0, E>=0.
elem(s(I,D,S,E),unsafe3) :- I>=0, D>=0, S>=0, E>=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)))))).