Commit d7fb6581 authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Adding PRISM DTMC model of type 1-slot for 3-machines production line

parent 3072209a
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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment