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

:-dynamic r/4.
:-dynamic info/4.

info(1,[p],9,[i,sU,eU,eM,pR,pW,pSU,pEMR,pEMW]).

r(init,p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),		%initial state
 {I>=0,SU=0,EU=0,EM=0,PR=0,PW=0,PSU=0,PEMR=0,PEMW=0},1).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r1
  p(s_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},1).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r2
  p(s_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
   },2).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r3
  p(s_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
  },3).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r4
  p(s_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 
   },4).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r5
  p(s_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
   },5).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%r6
  p(s_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
  },6).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm1
  p(s_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
  },7).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm2
  p(s_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
  },8).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wm3
  p(s_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
  },9).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh1
  p(s_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},10).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh2
  p(s_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
   },11).

r(p(s_s,I,SU,EU,EM,PR,PW,PSU,PEMR,PEMW),			%wh3
  p(s_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
  },12).



prop(unsafe,p:s * (i>=0) * (sU>=0) * (eU>=0) * (eM>=0) * (pR>=0) * (pW>=0) * (pSU>=0) * (pEMR>=0) * (pEMW>=0) * (eU+eM>=2) +  
            p:s * (i>=0) * (eU>=0) * (eM>=0) * (pR>=0) * (pW>=0) * (pSU>=0) * (pEMR>=0) * (pEMW>=0) * (eU+eM>=1) * (sU>=1)).