% BAKERY 3 proc. - safety [Delzanno-Podelski, 2001]
% MAP code
% MP - Nov 21, 2007


t(s(think,P,Q,A,B,C),s(wait,P,Q,A1,B,C)) :- A>=0,A1=:=B+1,B>C.
t(s(think,P,Q,A,B,C),s(wait,P,Q,A1,B,C)) :- A>=0,A1=:=C+1,C>=B.
t(s(wait,P,Q,A,B,C), s(use,P,Q,A,B,C)) :- A<B,A<C.
t(s(wait,P,Q,A,B,C), s(use,P,Q,A,B,C)) :- A<B,C=:=0.
t(s(wait,P,Q,A,B,C), s(use,P,Q,A,B,C)) :- B=:=0,A<C.
t(s(wait,P,Q,A,B,C), s(use,P,Q,A,B,C)) :- B=:=0,C=:=0.
t(s(use,P,Q,A,B,C),  s(think,P,Q,A1,B,C)) :- A>=0,A1=:=0.

t(s(P,think,Q,A,B,C),s(P,wait ,Q,A,B1,C)) :- B>=0,B1=:=A+1,A>C.
t(s(P,think,Q,A,B,C),s(P,wait, Q,A,B1,C)) :- B>=0,B1=:=C+1,C>=A.
t(s(P,wait, Q,A,B,C),s(P,use,  Q,A,B,C)) :- B<A,B<C.
t(s(P,wait, Q,A,B,C),s(P,use,  Q,A,B,C)) :- B<A,C=:=0.
t(s(P,wait, Q,A,B,C),s(P,use,  Q,A,B,C)) :- A=:=0,B<C.
t(s(P,wait, Q,A,B,C),s(P,use,  Q,A,B,C)) :- A=:=0,C=:=0.
t(s(P,use,  Q,A,B,C),s(P,think,Q,A,B1,C)) :- B>=0,B1=:=0.

t(s(P,Q,think,A,B,C),s(P,Q,wait ,A,B,C1)) :- C>=0,C1=:=A+1,A>B.
t(s(P,Q,think,A,B,C),s(P,Q,wait, A,B,C1)) :- C>=0,C1=:=B+1,B>=A.
t(s(P,Q,wait, A,B,C),s(P,Q,use,  A,B,C)) :- C<A,C<B.
t(s(P,Q,wait, A,B,C),s(P,Q,use,  A,B,C)) :- C<A,B=:=0.
t(s(P,Q,wait, A,B,C),s(P,Q,use,  A,B,C)) :- A=:=0,C<B.
t(s(P,Q,wait, A,B,C),s(P,Q,use,  A,B,C)) :- A=:=0,B=:=0.
t(s(P,Q,use,  A,B,C),s(P,Q,think,A,B,C1)) :- C>=0,C1=:=0.

%INITIAL STATE
elem(s(think,think,think,A,B,C),initial) :- A=:=0,B=:=0,C=:=0.

% UNSAFE STATE
elem(s(use,use,_,A,B,C),unsafe) :- A>=0, B>=0, C>=0.
elem(s(use,_,use,A,B,C),unsafe) :- A>=0, B>=0, C>=0.
elem(s(_,use,use,A,B,C),unsafe) :- A>=0, B>=0, C>=0.


% Temporal Properties

safe :- prop(not(ef(unsafe))).