% Bakery Protocol 2 proc. - safety [Delzanno-Podelski, 2001]
% MAP code
% MP - Nov 21, 2007


% Transitions

t(s(t,A,S,B),s(w,D,S,B)) :- D=:=B+1, A>=0, B>=0.
t(s(w,A,S,B),s(u,A,S,B)) :- A<B, A>=0.
t(s(w,A,S,B),s(u,A,S,B)) :- B=:=0, A>=0.
t(s(u,A,S,B),s(t,D,S,B)) :- D=:=0, A>=0, B>=0.
t(s(S,A,t,B),s(S,A,w,D)) :- D=:=A+1, A>=0.
t(s(S,A,w,B),s(S,A,u,B)) :- B<A, B>=0.
t(s(S,A,w,B),s(S,A,u,B)) :- A=:=0, B>=0.
t(s(S,A,u,B),s(S,A,t,D)) :- D=:=0, B>=0, A>=0.

ts(s(t,T1,t,T2),[s(w,T3,t,T2),s(t,T1,w,T4)]) :- T3=:=T2+1,T4=:=T1+1.
ts(s(t,T1,u,T2),[s(w,T3,u,T2),s(t,T1,t,T4)]) :- T3=:=T2+1,T4=:=0.
ts(s(t,T1,w,T2),[s(w,T3,w,T2),s(t,T1,u,T2)]) :- T3=:=T2+1,T2<T1.
ts(s(t,T1,w,T2),[s(w,T3,w,T2),s(t,T1,u,T2)]) :- T3=:=T2+1,T1=:=0.
ts(s(t,T1,w,T2),[s(w,T3,w,T2)]) :- T3=:=T2+1,T1>0,T1=<T2.
ts(s(u,T1,u,T2),[s(t,T3,u,T2),s(u,T1,t,T4)]) :- T3=:=0,T4=:=0.
ts(s(u,T1,w,T2),[s(t,T3,w,T2),s(u,T1,u,T2)]) :- T3=:=0,T2<T1.
ts(s(u,T1,w,T2),[s(t,T3,w,T2),s(u,T1,u,T2)]) :- T3=:=0,T1=:=0.
ts(s(u,T1,w,T2),[s(t,T3,w,T2)]) :- T3=:=0,T1>0,T1=<T2.
ts(s(w,T1,w,T2),[s(u,T1,w,T2),s(w,T1,u,T2)]) :- T1<T2, T1=:=0.
ts(s(w,T1,w,T2),[s(u,T1,w,T2)]) :- T1<T2, T1>0.
ts(s(w,T1,w,T2),[s(u,T1,w,T2),s(w,T1,u,T2)]) :- T2=:=0, T1=:=0.

ts(s(u,T2,t,T1),[s(u,T2,w,T3),s(t,T4,t,T1)]) :- T3=:=T2+1,T4=:=0.
ts(s(w,T2,t,T1),[s(w,T2,w,T3),s(u,T2,t,T1)]) :- T3=:=T2+1,T2<T1.
ts(s(w,T2,t,T1),[s(w,T2,w,T3),s(u,T2,t,T1)]) :- T3=:=T2+1,T1=:=0.
ts(s(w,T2,t,T1),[s(w,T2,w,T3)]) :- T3=:=T2+1,T1>0,T1=<T2.
ts(s(u,T2,u,T1),[s(u,T2,t,T3),s(t,T4,u,T1)]) :- T3=:=0,T4=:=0.
ts(s(w,T2,u,T1),[s(w,T2,t,T3),s(u,T2,u,T1)]) :- T3=:=0,T2<T1.
ts(s(w,T2,u,T1),[s(w,T2,t,T3),s(u,T2,u,T1)]) :- T3=:=0,T1=:=0.
ts(s(w,T2,u,T1),[s(w,T2,t,T3)]) :- T3=:=0,T1>0,T1=<T2.
ts(s(w,T2,w,T1),[s(w,T2,u,T1),s(u,T2,w,T1)]) :- T1<T2, T1=:=0.
ts(s(w,T2,w,T1),[s(w,T2,u,T1)]) :- T1<T2, T1>0.
ts(s(w,T2,w,T1),[s(w,T2,u,T1),s(u,T2,w,T1)]) :- T2=:=0, T1=:=0.


% Elementary Properties

%elem(s(A1,A2,B1,B2),has_successor) :- t(s(A1,A2,B1,B2),S).
elem(s(u,A,u,B),unsafe) :- A>=0, B>=0.
elem(s(w,A,_B,C),wait) :- A>=0, C>=0.
elem(s(u,A,_B,C),use) :- A>=0, C>=0.
elem(s(t,A,t,C),initial) :- A=:=0, C=:=0.
%elem(s(w,A,w,A),initial):- A>0.


% Temporal Properties

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

%total :- prop(ag(has_successor)).