% Reset Petri Net [Leuschel-Lehmann 200]
% MAP code
% MP - Nov 2000

%Transitions

t(s(X,Y),s(X1,Y1)) :- X>=1, X1=:=0, Y1=:=Y+2.
t(s(X,Y),s(X1,Y1)) :- Y>=1, X1=:=X+2, Y1=:=Y-1.


%Elementary Properties

elem(s(X,Y),initial) :- X=:=1, Y=:=0.
elem(s(X,Y),p30) :- X=:=3, Y=:=0.
elem(s(X,Y),p4) :- X>=4.


%elem(s(X,Y),initial21) :- X=:=2, Y>=1.
%elem(s(X,Y),initial10) :- X=:=1, Y=:=0.
%elem(s(X,Y),p0) :- X=:=0, Y=:=0.
%elem(s(X,Y),p1) :- X=:=3, Y=:=1.
%elem(s(X,Y),p2) :- X=:=3, Y=:=0.
%elem(s(X,Y),p3) :- X=:=3.

%Temporal Properties

safe :- prop(not(ef(p30))).

%prop0 :- exists_state(and(initial10,not(ef(p0)))).
%prop1 :- \+ exists_state(and(initial21,not(ef(p1)))).
%prop1neg :- \+ exists_state(and(initial21,ef(p1))).
%prop2 :- \+ exists_state(and(initial21,ef(p2))).
%prop3 :- \+ exists_state(and(initial21,ef(p3))).