% MAP code
% Futurebus Protocol [Delzanno, FORTE-2000]
% MP - Nov 20, 2007

%Transitions

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r1
  s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
   	EM+SU+EU>=1.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r2
  s(I1,SU1,EU1,EM1,PR1,PW,PSU1,PEMR1,PEMW)) :-
	SU>=0,EU>=0,EM>=0,PR>=0,PSU>=0,PEMR>=0,PEMW>=0,
   	I>=1,PW=:=0,
   	I1=:=I-1,
   	PR1=:=PR+1,
   	PSU1=:=PSU+SU+EU,
   	PEMR1=:=PEMR+EM,
   	SU1=:=0,
   	EU1=:=0,
   	EM1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r3
  s(I,SU1,EU,EM,PR1,PW,PSU,PEMR1,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMW>=0,
   	PEMR>=1,
   	SU1=:=SU+PR+1,
   	PEMR1=:=PEMR-1,
   	PR1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r4
  s(I,SU1,EU,EM,PR1,PW,PSU1,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PEMR>=0,PEMW>=0,
   	PSU>=1,
   	SU1=:=SU+PSU+PR,
   	PR1=:=0,
   	PSU1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r5
  s(I,SU1,EU,EM,PR1,PW,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PW>=0,PEMW>=0,
   	PR>=2,PSU=:=0,PEMR=:=0,
   	SU1=:=SU+PR,
   	PR1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r6
  s(I,SU,EU1,EM,PR1,PW,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PW>=0,PEMW>=0,
   	PR=:=1,PSU=:=0,PEMR=:=0,
   	EU1=:=EU+1,
   	PR1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm1
  s(I1,SU1,EU1,EM1,PR1,PW1,PSU1,PEMR1,PEMW1)) :-
	SU>=0,EU>=0,EM>=0,PR>=0,PSU>=0,PEMR>=0,PEMW>=0,
   	I>=1,PW=:=0,
   	PW1=:=1,
   	I1=:=I+SU+EU+PR+PSU+PEMR-1,
   	PEMW1=:=PEMW+EM,
   	SU1=:=0,
   	EU1=:=0,
   	EM1=:=0,
   	PR1=:=0,
   	PSU1=:=0,
   	PEMR1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm2
  s(I1,SU,EU,EM1,PR,PW1,PSU,PEMR,PEMW1)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,
	PEMW>=1,
   	I1=:=I+1,
   	PEMW1=:=PEMW-1,
   	EM1=:=EM+PW,
   	PW1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm3
  s(I,SU,EU,EM1,PR,PW1,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,
   	PEMW=:=0,
   	EM1=:=EM+PW,
   	PW1=:=0.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh1
  s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EU>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
	EM>=1.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh2
  s(I,SU,EU1,EM1,PR,PW,PSU,PEMR,PEMW)) :-
	I>=0,SU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
   	EU>=1,
   	EU1=:=EU-1,
   	EM1=:=EM+1.

t(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh3
  s(I1,SU1,EU,EM1,PR,PW,PSU,PEMR,PEMW)) :-
	I>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
   	SU>=1,
   	I1=:=I+SU-1,
   	SU1=:=0,
   	EM1=:=EM+1.



%Elementary Properties

elem(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),initial) :-
	I>=0,SU=:=0,EU=:=0,EM=:=0,PR=:=0,PW=:=0,PSU=:=0,PEMR=:=0,PEMW=:=0.
elem(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),unsafe1) :-
	I>=0,SU>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
	EU+EM>=2.
elem(s(I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),unsafe2) :-
	I>=0,EU>=0,EM>=0,PR>=0,PW>=0,PSU>=0,PEMR>=0,PEMW>=0,
        EU+EM>=1, SU>=1.


%Temporal Properties

safe1 :- prop(not(ef(unsafe1))).
safe2 :- prop(not(ef(unsafe2))).
safe :- prop(not(ef(or(unsafe1,unsafe2)))).