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


%Transitions

t(s(t,Y,A,B,C,D),s(w,Y,A1,B,C1,D)) :- A>=0, B>=0, C>=0, D>=0, A1=:=C, C1=:=C+1.
t(s(w,Y,A,B,C,D),s(u,Y,A,B,C,D)) :- A>=0, B>=0, C>=0, A=<D.
t(s(u,Y,A,B,C,D),s(t,Y,A,B,C,D1)) :- A>=0, B>=0, C>=0, D>=0, D1=:=D+1.
t(s(X,t,A,B,C,D),s(X,w,A,B1,C1,D)) :- A>=0, B>=0, C>=0, D>=0, B1=:=C, C1=:=C+1.
t(s(X,w,A,B,C,D),s(X,u,A,B,C,D)) :- A>=0, B>=0, C>=0, B=<D.
t(s(X,u,A,B,C,D),s(X,t,A,B,C,D1)) :- A>=0, B>=0, C>=0, D>=0, D1=:=D+1.

ts(s(t,t,A,B,T,S),[s(w,t,T,B,T1,S),s(t,w,A,T,T1,S)]) :- T>=0, T1=:=T+1.
ts(s(t,w,A,B,T,S),[s(w,w,T,B,T1,S),s(t,u,A,B,T,S)]) :- T>=0, T1=:=T+1, B=<S.
ts(s(t,w,A,B,T,S),[s(w,w,T,B,T1,S)]) :- T>=0, T1=:=T+1, B>S.
ts(s(t,u,A,B,T,S),[s(w,u,T,B,T1,S),s(t,t,A,B,T,S1)]) :- T>=0, T1=:=T+1, S>=0, S1=:=S+1.
ts(s(w,t,A,B,T,S),[s(u,t,A,B,T,S),s(w,w,A,T,T1,S)]) :- T>=0, T1=:=T+1, A=<S.
ts(s(w,t,A,B,T,S),[s(w,w,A,T,T1,S)]) :- T>=0, T1=:=T+1, A>S.
ts(s(w,w,A,B,T,S),[s(u,w,A,B,T,S),s(w,u,A,B,T,S)]) :- A=<S, B=<S.
ts(s(w,w,A,B,T,S),[s(w,u,A,B,T,S)]) :- A>S, B=<S.
ts(s(w,w,A,B,T,S),[s(u,w,A,B,T,S)]) :- A=<S, B>S.
ts(s(w,u,A,B,T,S),[s(u,u,A,B,T,S),s(w,t,A,B,T,S1)]) :- S>=0, S1=:=S+1, A=<S.
ts(s(w,u,A,B,T,S),[s(w,t,A,B,T,S1)]) :- S>=0, S1=:=S+1, A>S.
ts(s(u,t,A,B,T,S),[s(t,t,A,B,T,S1),s(u,w,A,T,T1,S)]) :- T>=0, T1=:=T+1, S>=0, S1=:=S+1.
ts(s(u,w,A,B,T,S),[s(u,u,A,B,T,S),s(t,w,A,B,T,S1)]) :- S>=0, S1=:=S+1, B=<S.
ts(s(u,w,A,B,T,S),[s(t,w,A,B,T,S1)]) :- S>=0, S1=:=S+1, B>S.
ts(s(u,u,A,B,T,S),[s(t,u,A,B,T,S1),s(u,t,A,B,T,S1)]) :- S>=0, S1=:=S+1.


%Elementary Properties

elem(s(t,t,A,B,C,D),initial) :- A=:=0, B=:=0, C=:=D, C>=0.
elem(s(u,u,A,B,S,T),unsafe) :- A>=0, B>=0, S>=0, T>=0.
elem(s(w,P,A,B,S,T),wait) :- A>=0, B>=0, S>=0, T>=0.
elem(s(u,P,A,B,S,T),use) :- A>=0, B>=0, S>=0, T>=0.


%Temporal Properties

safe :- prop(not(ef(unsafe))).
starvfree :- prop(not(ef(and(wait,not(af(use)))))).