dtmc

const double p1=1.000000000000e-02;
const double p2=5.000000000000e-02;
const double p3=2.000000000000e-02;
const double r1=1.000000000000e-01;
const double r2=2.000000000000e-01;
const double r3=1.500000000000e-01;
const int n1=8;
const int n2=5;
const int m1init=1;
const int m2init=0;
const int m3init=1;
const int b1init=2;
const int b2init=3;

module ProductionLine
m1: [0..1] init m1init;
m2: [0..1] init m2init;
m3: [0..1] init m3init;
b1: [0..n1] init b1init;
b2: [0..n2] init b2init;

 [] (m1=0)&(m2=0)&(m3=0)&(b1=0)&(b2=0) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)+
      (1-r1)*r2*(1-r3):(m2'=1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1+1);
 [] (m1=0)&(m2=0)&(m3=0)&(b1=0)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2-1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=0)&(b1=0)&(b2=n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2-1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(b2=0) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)+
      (1-r1)*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b2'=b2+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b2'=b2+1);
 [] (m1=0)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b2'=b2+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1);
 [] (m1=0)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(b2=n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2-1)+
      r1*(1-r2)*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=0)&(b1=n1)&(b2=0) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)+
      (1-r1)*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-r2)*(1-r3):(m1'=1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=0)&(m2=0)&(m3=0)&(b1=n1)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1)+
      r1*(1-r2)*(1-r3):(m1'=1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b1'=b1-1);
 [] (m1=0)&(m2=0)&(m3=0)&(b1=n1)&(b2=n2) ->
      (1-r1)*(1-r2)*(1-r3):true+
      (1-r1)*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      (1-r1)*r2*(1-r3):(m2'=1)+
      (1-r1)*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2-1)+
      r1*(1-r2)*(1-r3):(m1'=1)+
      r1*(1-r2)*r3:(m1'=1)&(m3'=1)&(b2'=b2-1)+
      r1*r2*(1-r3):(m1'=1)&(m2'=1)+
      r1*r2*r3:(m1'=1)&(m2'=1)&(m3'=1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=0)&(b2=0) ->
      (1-r1)*(1-r2)*1.0:true+
      (1-r1)*r2*1.0:(m2'=1)+
      r1*(1-r2)*1.0:(m1'=1)&(b1'=b1+1)+
      r1*r2*1.0:(m1'=1)&(m2'=1)&(b1'=b1+1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=0)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b2'=b2-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)&(b1'=b1+1)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=0)&(b2=n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b2'=b2-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)&(b1'=b1+1)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(b2=0) ->
      (1-r1)*(1-r2)*1.0:true+
      (1-r1)*r2*1.0:(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-r2)*1.0:(m1'=1)&(b1'=b1+1)+
      r1*r2*1.0:(m1'=1)&(m2'=1)&(b2'=b2+1);
 [] (m1=0)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b1'=b1-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)&(b2'=b2+1)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1);
 [] (m1=0)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(b2=n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b2'=b2-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)&(b1'=b1+1)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=n1)&(b2=0) ->
      (1-r1)*(1-r2)*1.0:true+
      (1-r1)*r2*1.0:(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-r2)*1.0:(m1'=1)+
      r1*r2*1.0:(m1'=1)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=n1)&(0<b2)&(b2<n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b1'=b1-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1)&(b1'=b1-1);
 [] (m1=0)&(m2=0)&(m3=1)&(b1=n1)&(b2=n2) ->
      (1-r1)*(1-r2)*p3:(m3'=0)+
      (1-r1)*(1-r2)*(1-p3):(b2'=b2-1)+
      (1-r1)*r2*p3:(m2'=1)&(m3'=0)+
      (1-r1)*r2*(1-p3):(m2'=1)&(b2'=b2-1)+
      r1*(1-r2)*p3:(m1'=1)&(m3'=0)+
      r1*(1-r2)*(1-p3):(m1'=1)&(b2'=b2-1)+
      r1*r2*p3:(m1'=1)&(m2'=1)&(m3'=0)+
      r1*r2*(1-p3):(m1'=1)&(m2'=1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=0)&(b2=0) ->
      (1-r1)*1.0*(1-r3):true+
      (1-r1)*1.0*r3:(m3'=1)+
      r1*1.0*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*1.0*r3:(m1'=1)&(m3'=1)&(b1'=b1+1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=0)&(0<b2)&(b2<n2) ->
      (1-r1)*1.0*(1-r3):true+
      (1-r1)*1.0*r3:(m3'=1)&(b2'=b2-1)+
      r1*1.0*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*1.0*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=0)&(b2=n2) ->
      (1-r1)*1.0*(1-r3):true+
      (1-r1)*1.0*r3:(m3'=1)&(b2'=b2-1)+
      r1*1.0*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*1.0*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(b2=0) ->
      (1-r1)*p2*(1-r3):(m2'=0)+
      (1-r1)*p2*r3:(m2'=0)&(m3'=1)+
      (1-r1)*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*r3:(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*p2*(1-r3):(m1'=1)&(m2'=0)&(b1'=b1+1)+
      r1*p2*r3:(m1'=1)&(m2'=0)&(m3'=1)&(b1'=b1+1)+
      r1*(1-p2)*(1-r3):(m1'=1)&(b2'=b2+1)+
      r1*(1-p2)*r3:(m1'=1)&(m3'=1)&(b2'=b2+1);
 [] (m1=0)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      (1-r1)*p2*(1-r3):(m2'=0)+
      (1-r1)*p2*r3:(m2'=0)&(m3'=1)&(b2'=b2-1)+
      (1-r1)*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*r3:(m3'=1)&(b1'=b1-1)+
      r1*p2*(1-r3):(m1'=1)&(m2'=0)&(b1'=b1+1)+
      r1*p2*r3:(m1'=1)&(m2'=0)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      r1*(1-p2)*(1-r3):(m1'=1)&(b2'=b2+1)+
      r1*(1-p2)*r3:(m1'=1)&(m3'=1);
 [] (m1=0)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(b2=n2) ->
      (1-r1)*1.0*(1-r3):true+
      (1-r1)*1.0*r3:(m3'=1)&(b2'=b2-1)+
      r1*1.0*(1-r3):(m1'=1)&(b1'=b1+1)+
      r1*1.0*r3:(m1'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=n1)&(b2=0) ->
      (1-r1)*p2*(1-r3):(m2'=0)+
      (1-r1)*p2*r3:(m2'=0)&(m3'=1)+
      (1-r1)*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*r3:(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*p2*(1-r3):(m1'=1)&(m2'=0)+
      r1*p2*r3:(m1'=1)&(m2'=0)&(m3'=1)+
      r1*(1-p2)*(1-r3):(m1'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-p2)*r3:(m1'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=n1)&(0<b2)&(b2<n2) ->
      (1-r1)*p2*(1-r3):(m2'=0)+
      (1-r1)*p2*r3:(m2'=0)&(m3'=1)&(b2'=b2-1)+
      (1-r1)*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*r3:(m3'=1)&(b1'=b1-1)+
      r1*p2*(1-r3):(m1'=1)&(m2'=0)+
      r1*p2*r3:(m1'=1)&(m2'=0)&(m3'=1)&(b2'=b2-1)+
      r1*(1-p2)*(1-r3):(m1'=1)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-p2)*r3:(m1'=1)&(m3'=1)&(b1'=b1-1);
 [] (m1=0)&(m2=1)&(m3=0)&(b1=n1)&(b2=n2) ->
      (1-r1)*1.0*(1-r3):true+
      (1-r1)*1.0*r3:(m3'=1)&(b2'=b2-1)+
      r1*1.0*(1-r3):(m1'=1)+
      r1*1.0*r3:(m1'=1)&(m3'=1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=0)&(b2=0) ->
      (1-r1)*1.0*1.0:true+
      r1*1.0*1.0:(m1'=1)&(b1'=b1+1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=0)&(0<b2)&(b2<n2) ->
      (1-r1)*1.0*p3:(m3'=0)+
      (1-r1)*1.0*(1-p3):(b2'=b2-1)+
      r1*1.0*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*1.0*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=0)&(b2=n2) ->
      (1-r1)*1.0*p3:(m3'=0)+
      (1-r1)*1.0*(1-p3):(b2'=b2-1)+
      r1*1.0*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*1.0*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(b2=0) ->
      (1-r1)*p2*1.0:(m2'=0)+
      (1-r1)*(1-p2)*1.0:(b1'=b1-1)&(b2'=b2+1)+
      r1*p2*1.0:(m1'=1)&(m2'=0)&(b1'=b1+1)+
      r1*(1-p2)*1.0:(m1'=1)&(b2'=b2+1);
 [] (m1=0)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      (1-r1)*p2*p3:(m2'=0)&(m3'=0)+
      (1-r1)*p2*(1-p3):(m2'=0)&(b2'=b2-1)+
      (1-r1)*(1-p2)*p3:(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*(1-p3):(b1'=b1-1)+
      r1*p2*p3:(m1'=1)&(m2'=0)&(m3'=0)&(b1'=b1+1)+
      r1*p2*(1-p3):(m1'=1)&(m2'=0)&(b1'=b1+1)&(b2'=b2-1)+
      r1*(1-p2)*p3:(m1'=1)&(m3'=0)&(b2'=b2+1)+
      r1*(1-p2)*(1-p3):(m1'=1);
 [] (m1=0)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(b2=n2) ->
      (1-r1)*1.0*p3:(m3'=0)+
      (1-r1)*1.0*(1-p3):(b2'=b2-1)+
      r1*1.0*p3:(m1'=1)&(m3'=0)&(b1'=b1+1)+
      r1*1.0*(1-p3):(m1'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=n1)&(b2=0) ->
      (1-r1)*p2*1.0:(m2'=0)+
      (1-r1)*(1-p2)*1.0:(b1'=b1-1)&(b2'=b2+1)+
      r1*p2*1.0:(m1'=1)&(m2'=0)+
      r1*(1-p2)*1.0:(m1'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=n1)&(0<b2)&(b2<n2) ->
      (1-r1)*p2*p3:(m2'=0)&(m3'=0)+
      (1-r1)*p2*(1-p3):(m2'=0)&(b2'=b2-1)+
      (1-r1)*(1-p2)*p3:(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      (1-r1)*(1-p2)*(1-p3):(b1'=b1-1)+
      r1*p2*p3:(m1'=1)&(m2'=0)&(m3'=0)+
      r1*p2*(1-p3):(m1'=1)&(m2'=0)&(b2'=b2-1)+
      r1*(1-p2)*p3:(m1'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      r1*(1-p2)*(1-p3):(m1'=1)&(b1'=b1-1);
 [] (m1=0)&(m2=1)&(m3=1)&(b1=n1)&(b2=n2) ->
      (1-r1)*1.0*p3:(m3'=0)+
      (1-r1)*1.0*(1-p3):(b2'=b2-1)+
      r1*1.0*p3:(m1'=1)&(m3'=0)+
      r1*1.0*(1-p3):(m1'=1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=0)&(b2=0) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b1'=b1+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1+1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=0)&(0<b2)&(b2<n2) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b1'=b1+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=0)&(b2=n2) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b1'=b1+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(b2=0) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b2'=b2+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2+1);
 [] (m1=1)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)&(b1'=b1-1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b2'=b2+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1);
 [] (m1=1)&(m2=0)&(m3=0)&(0<b1)&(b1<n1)&(b2=n2) ->
      p1*(1-r2)*(1-r3):(m1'=0)+
      p1*(1-r2)*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      p1*r2*(1-r3):(m1'=0)&(m2'=1)+
      p1*r2*r3:(m1'=0)&(m2'=1)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*(1-r3):(b1'=b1+1)+
      (1-p1)*(1-r2)*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*(1-r3):(m2'=1)&(b1'=b1+1)+
      (1-p1)*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=n1)&(b2=0) ->
      1.0*(1-r2)*(1-r3):true+
      1.0*(1-r2)*r3:(m3'=1)+
      1.0*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      1.0*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=n1)&(0<b2)&(b2<n2) ->
      1.0*(1-r2)*(1-r3):true+
      1.0*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      1.0*r2*(1-r3):(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      1.0*r2*r3:(m2'=1)&(m3'=1)&(b1'=b1-1);
 [] (m1=1)&(m2=0)&(m3=0)&(b1=n1)&(b2=n2) ->
      1.0*(1-r2)*(1-r3):true+
      1.0*(1-r2)*r3:(m3'=1)&(b2'=b2-1)+
      1.0*r2*(1-r3):(m2'=1)+
      1.0*r2*r3:(m2'=1)&(m3'=1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=0)&(b2=0) ->
      p1*(1-r2)*1.0:(m1'=0)+
      p1*r2*1.0:(m1'=0)&(m2'=1)+
      (1-p1)*(1-r2)*1.0:(b1'=b1+1)+
      (1-p1)*r2*1.0:(m2'=1)&(b1'=b1+1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=0)&(0<b2)&(b2<n2) ->
      p1*(1-r2)*p3:(m1'=0)&(m3'=0)+
      p1*(1-r2)*(1-p3):(m1'=0)&(b2'=b2-1)+
      p1*r2*p3:(m1'=0)&(m2'=1)&(m3'=0)+
      p1*r2*(1-p3):(m1'=0)&(m2'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*(1-r2)*(1-p3):(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1+1)+
      (1-p1)*r2*(1-p3):(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=0)&(b2=n2) ->
      p1*(1-r2)*p3:(m1'=0)&(m3'=0)+
      p1*(1-r2)*(1-p3):(m1'=0)&(b2'=b2-1)+
      p1*r2*p3:(m1'=0)&(m2'=1)&(m3'=0)+
      p1*r2*(1-p3):(m1'=0)&(m2'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*(1-r2)*(1-p3):(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1+1)+
      (1-p1)*r2*(1-p3):(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(b2=0) ->
      p1*(1-r2)*1.0:(m1'=0)+
      p1*r2*1.0:(m1'=0)&(m2'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-p1)*(1-r2)*1.0:(b1'=b1+1)+
      (1-p1)*r2*1.0:(m2'=1)&(b2'=b2+1);
 [] (m1=1)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      p1*(1-r2)*p3:(m1'=0)&(m3'=0)+
      p1*(1-r2)*(1-p3):(m1'=0)&(b2'=b2-1)+
      p1*r2*p3:(m1'=0)&(m2'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      p1*r2*(1-p3):(m1'=0)&(m2'=1)&(b1'=b1-1)+
      (1-p1)*(1-r2)*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*(1-r2)*(1-p3):(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*p3:(m2'=1)&(m3'=0)&(b2'=b2+1)+
      (1-p1)*r2*(1-p3):(m2'=1);
 [] (m1=1)&(m2=0)&(m3=1)&(0<b1)&(b1<n1)&(b2=n2) ->
      p1*(1-r2)*p3:(m1'=0)&(m3'=0)+
      p1*(1-r2)*(1-p3):(m1'=0)&(b2'=b2-1)+
      p1*r2*p3:(m1'=0)&(m2'=1)&(m3'=0)+
      p1*r2*(1-p3):(m1'=0)&(m2'=1)&(b2'=b2-1)+
      (1-p1)*(1-r2)*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*(1-r2)*(1-p3):(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1+1)+
      (1-p1)*r2*(1-p3):(m2'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=n1)&(b2=0) ->
      1.0*(1-r2)*1.0:true+
      1.0*r2*1.0:(m2'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=n1)&(0<b2)&(b2<n2) ->
      1.0*(1-r2)*p3:(m3'=0)+
      1.0*(1-r2)*(1-p3):(b2'=b2-1)+
      1.0*r2*p3:(m2'=1)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      1.0*r2*(1-p3):(m2'=1)&(b1'=b1-1);
 [] (m1=1)&(m2=0)&(m3=1)&(b1=n1)&(b2=n2) ->
      1.0*(1-r2)*p3:(m3'=0)+
      1.0*(1-r2)*(1-p3):(b2'=b2-1)+
      1.0*r2*p3:(m2'=1)&(m3'=0)+
      1.0*r2*(1-p3):(m2'=1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=0)&(b2=0) ->
      p1*1.0*(1-r3):(m1'=0)+
      p1*1.0*r3:(m1'=0)&(m3'=1)+
      (1-p1)*1.0*(1-r3):(b1'=b1+1)+
      (1-p1)*1.0*r3:(m3'=1)&(b1'=b1+1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=0)&(0<b2)&(b2<n2) ->
      p1*1.0*(1-r3):(m1'=0)+
      p1*1.0*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*1.0*(1-r3):(b1'=b1+1)+
      (1-p1)*1.0*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=0)&(b2=n2) ->
      p1*1.0*(1-r3):(m1'=0)+
      p1*1.0*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*1.0*(1-r3):(b1'=b1+1)+
      (1-p1)*1.0*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(b2=0) ->
      p1*p2*(1-r3):(m1'=0)&(m2'=0)+
      p1*p2*r3:(m1'=0)&(m2'=0)&(m3'=1)+
      p1*(1-p2)*(1-r3):(m1'=0)&(b1'=b1-1)&(b2'=b2+1)+
      p1*(1-p2)*r3:(m1'=0)&(m3'=1)&(b1'=b1-1)&(b2'=b2+1)+
      (1-p1)*p2*(1-r3):(m2'=0)&(b1'=b1+1)+
      (1-p1)*p2*r3:(m2'=0)&(m3'=1)&(b1'=b1+1)+
      (1-p1)*(1-p2)*(1-r3):(b2'=b2+1)+
      (1-p1)*(1-p2)*r3:(m3'=1)&(b2'=b2+1);
 [] (m1=1)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      p1*p2*(1-r3):(m1'=0)&(m2'=0)+
      p1*p2*r3:(m1'=0)&(m2'=0)&(m3'=1)&(b2'=b2-1)+
      p1*(1-p2)*(1-r3):(m1'=0)&(b1'=b1-1)&(b2'=b2+1)+
      p1*(1-p2)*r3:(m1'=0)&(m3'=1)&(b1'=b1-1)+
      (1-p1)*p2*(1-r3):(m2'=0)&(b1'=b1+1)+
      (1-p1)*p2*r3:(m2'=0)&(m3'=1)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*(1-p2)*(1-r3):(b2'=b2+1)+
      (1-p1)*(1-p2)*r3:(m3'=1);
 [] (m1=1)&(m2=1)&(m3=0)&(0<b1)&(b1<n1)&(b2=n2) ->
      p1*1.0*(1-r3):(m1'=0)+
      p1*1.0*r3:(m1'=0)&(m3'=1)&(b2'=b2-1)+
      (1-p1)*1.0*(1-r3):(b1'=b1+1)+
      (1-p1)*1.0*r3:(m3'=1)&(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=n1)&(b2=0) ->
      1.0*p2*(1-r3):(m2'=0)+
      1.0*p2*r3:(m2'=0)&(m3'=1)+
      1.0*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      1.0*(1-p2)*r3:(m3'=1)&(b1'=b1-1)&(b2'=b2+1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=n1)&(0<b2)&(b2<n2) ->
      1.0*p2*(1-r3):(m2'=0)+
      1.0*p2*r3:(m2'=0)&(m3'=1)&(b2'=b2-1)+
      1.0*(1-p2)*(1-r3):(b1'=b1-1)&(b2'=b2+1)+
      1.0*(1-p2)*r3:(m3'=1)&(b1'=b1-1);
 [] (m1=1)&(m2=1)&(m3=0)&(b1=n1)&(b2=n2) ->
      1.0*1.0*(1-r3):true+
      1.0*1.0*r3:(m3'=1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=0)&(b2=0) ->
      p1*1.0*1.0:(m1'=0)+
      (1-p1)*1.0*1.0:(b1'=b1+1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=0)&(0<b2)&(b2<n2) ->
      p1*1.0*p3:(m1'=0)&(m3'=0)+
      p1*1.0*(1-p3):(m1'=0)&(b2'=b2-1)+
      (1-p1)*1.0*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*1.0*(1-p3):(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=0)&(b2=n2) ->
      p1*1.0*p3:(m1'=0)&(m3'=0)+
      p1*1.0*(1-p3):(m1'=0)&(b2'=b2-1)+
      (1-p1)*1.0*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*1.0*(1-p3):(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(b2=0) ->
      p1*p2*1.0:(m1'=0)&(m2'=0)+
      p1*(1-p2)*1.0:(m1'=0)&(b1'=b1-1)&(b2'=b2+1)+
      (1-p1)*p2*1.0:(m2'=0)&(b1'=b1+1)+
      (1-p1)*(1-p2)*1.0:(b2'=b2+1);
 [] (m1=1)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(0<b2)&(b2<n2) ->
      p1*p2*p3:(m1'=0)&(m2'=0)&(m3'=0)+
      p1*p2*(1-p3):(m1'=0)&(m2'=0)&(b2'=b2-1)+
      p1*(1-p2)*p3:(m1'=0)&(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      p1*(1-p2)*(1-p3):(m1'=0)&(b1'=b1-1)+
      (1-p1)*p2*p3:(m2'=0)&(m3'=0)&(b1'=b1+1)+
      (1-p1)*p2*(1-p3):(m2'=0)&(b1'=b1+1)&(b2'=b2-1)+
      (1-p1)*(1-p2)*p3:(m3'=0)&(b2'=b2+1)+
      (1-p1)*(1-p2)*(1-p3):true;
 [] (m1=1)&(m2=1)&(m3=1)&(0<b1)&(b1<n1)&(b2=n2) ->
      p1*1.0*p3:(m1'=0)&(m3'=0)+
      p1*1.0*(1-p3):(m1'=0)&(b2'=b2-1)+
      (1-p1)*1.0*p3:(m3'=0)&(b1'=b1+1)+
      (1-p1)*1.0*(1-p3):(b1'=b1+1)&(b2'=b2-1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=n1)&(b2=0) ->
      1.0*p2*1.0:(m2'=0)+
      1.0*(1-p2)*1.0:(b1'=b1-1)&(b2'=b2+1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=n1)&(0<b2)&(b2<n2) ->
      1.0*p2*p3:(m2'=0)&(m3'=0)+
      1.0*p2*(1-p3):(m2'=0)&(b2'=b2-1)+
      1.0*(1-p2)*p3:(m3'=0)&(b1'=b1-1)&(b2'=b2+1)+
      1.0*(1-p2)*(1-p3):(b1'=b1-1);
 [] (m1=1)&(m2=1)&(m3=1)&(b1=n1)&(b2=n2) ->
      1.0*1.0*p3:(m3'=0)+
      1.0*1.0*(1-p3):(b2'=b2-1);
endmodule