dtmc

const double psend =0.8;
const double pdelay =0.5;


module node0
active0:[0..1] init 1;
send0:  [0..1] init 0;

[tick] active0=1 & send0=0 -> psend:(active0'=1)&(send0'=1)+(1-psend):(active0'=0)&(send0'=0);
[tick] active0=1 & send0=1 -> (send0'=0)& (active0'=0);
[tick] active0=0  -> (send0'=0)& (active0'=0);
endmodule


module node1
active1:[0..2] init 1;
send1:  [0..1] init 0;

[tick] active1=1 & send1=0 & send0+send2+send4 =1 -> (1-pdelay)* psend: (active1'=1)&(send1'=1)
                                                     +(1-pdelay)*(1-psend):(active1'=0)&(send1'=0)
                                                     +   pdelay:           (active1'=2)&(send1'=0);
[tick] active1=2                                   -> (1-pdelay)*psend: (active1'=1)&(send1'=1)
                                                     +(1-pdelay)*(1-psend):(active1'=0)&(send1'=0)
                                                     +   pdelay:           (active1'=2)&(send1'=0);
[tick] active1=1 & send1=0 &  send0+send2+send4 !=1 -> (active1'=1)& (send1'=0);
[tick] active1=1 & send1=1 -> (send1'=0)& (active1'=0);
[tick] active1=0           -> (send1'=0)& (active1'=0);
endmodule

module node2
active2:[0..2] init 1;
send2:  [0..1] init 0;

[tick] active2=1 & send2=0 & send1+send5 =1 ->       (1-pdelay)*psend: (active2'=1)&(send2'=1)
                                                     +(1-pdelay)*(1-psend):(active2'=0)&(send2'=0)
                                                     +   pdelay:           (active2'=2)&(send2'=0);
[tick] active2=2                                  ->  (1-pdelay)*psend: (active2'=1)&(send2'=1)
                                                     +(1-pdelay)*(1-psend):(active2'=0)&(send2'=0)
                                                     +   pdelay:           (active2'=2)&(send2'=0);
[tick] active2=1 & send2=0 & send1+send5 !=1 -> (active2'=1)& (send2'=0);
[tick] active2=1 & send2=1   -> (send2'=0)& (active2'=0);
[tick] active2=0  -> (send2'=0)& (active2'=0);
endmodule


module node3
active3:[0..2] init 1;
send3:  [0..1] init 0;

[tick] active3=1 & send3=0 & send0+send4+ send6  =1 ->       (1-pdelay)*psend: (active3'=1)&(send3'=1)
                                                     +(1-pdelay)*(1-psend):(active3'=0)&(send3'=0)
                                                     +   pdelay:           (active3'=2)&(send3'=0);
[tick] active3=2                                   ->       (1-pdelay)*psend: (active3'=1)&(send3'=1)
                                                     +(1-pdelay)*(1-psend):(active3'=0)&(send3'=0)
                                                     +   pdelay:           (active3'=2)&(send3'=0);
[tick] active3=1 & send3=0 & send0+send4+ send6 !=1 -> (active3'=1)& (send3'=0);
[tick] active3=1 & send3=1    -> (send3'=0)& (active3'=0);
[tick] active3=0  -> (send3'=0)& (active3'=0);
endmodule


module node4
active4:[0..2] init 1;
send4:  [0..1] init 0;

[tick] active4=1 & send4=0 & send1+send3+send5+send7 =1 ->       (1-pdelay)*psend: (active4'=1)&(send4'=1)
                                                     +(1-pdelay)*(1-psend):(active4'=0)&(send4'=0)
                                                     +   pdelay:           (active4'=2)&(send4'=0);
[tick] active4=2                                   ->       (1-pdelay)*psend: (active4'=1)&(send4'=1)
                                                     +(1-pdelay)*(1-psend):(active4'=0)&(send4'=0)
                                                     +   pdelay:           (active4'=2)&(send4'=0);
[tick] active4=1 & send4=0 & send1+send3+ send5 +send7 !=1 -> (active4'=1) & (send4'=0);
[tick] active4=1 & send4=1 -> (send4'=0)& (active4'=0);
[tick] active4=0  -> (send4'=0)& (active4'=0);
endmodule

module node5
active5:[0..2] init 1;
send5:  [0..1] init 0;

[tick] active5=1 & send5=0 & send2+send4+ send8=1 ->       (1-pdelay)*psend: (active5'=1)&(send5'=1)
                                                     +(1-pdelay)*(1-psend):(active5'=0)&(send5'=0)
                                                     +   pdelay:           (active5'=2)&(send5'=0);
[tick] active5=2                                   ->       (1-pdelay)*psend: (active5'=1)&(send5'=1)
                                                     +(1-pdelay)*(1-psend):(active5'=0)&(send5'=0)
                                                     +   pdelay:           (active5'=2)&(send5'=0);
[tick] active5=1 & send5=0 & send2+send4+ send8 !=1 -> (active5'=1) & (send5'=0);
[tick] active5=1 & send5=1 -> (send5'=0)& (active5'=0);
[tick] active5=0  -> (send5'=0)& (active5'=0);
endmodule

module node6
active6:[0..2] init 1;
send6:  [0..1] init 0;

[tick] active6=1 & send6=0 & send3+send7=1  ->       (1-pdelay)*psend: (active6'=1)&(send6'=1)
                                                     +(1-pdelay)*(1-psend):(active6'=0)&(send6'=0)
                                                     +   pdelay:           (active6'=2)&(send6'=0);
[tick] active6=2                                   ->       (1-pdelay)*psend: (active6'=1)&(send6'=1)
                                                     +(1-pdelay)*(1-psend):(active6'=0)&(send6'=0)
                                                     +   pdelay:           (active6'=2)&(send6'=0);
[tick] active6=1 & send6=0 & send3+send7 !=1 -> (active6'=1) & (send6'=0);
[tick] active6=1 & send6=1    -> (send6'=0)& (active6'=0);
[tick] active6=0  -> (send6'=0)& (active6'=0);
endmodule

module node7
active7:[0..2] init 1;
send7:  [0..1] init 0;

[tick] active7=1 & send7=0 & send4+send6+ send8=1 -> (1-pdelay)*psend: (active7'=1)&(send7'=1)
                                                     +(1-pdelay)*(1-psend):(active7'=0)&(send7'=0)
                                                     +   pdelay:           (active7'=2)&(send7'=0);
[tick] active7=2                                   -> (1-pdelay)*psend: (active7'=1)&(send7'=1)
                                                     +(1-pdelay)*(1-psend):(active7'=0)&(send7'=0)
                                                     +   pdelay:           (active7'=2)&(send7'=0);
[tick] active7=1 & send7=0 & send4+send6+ send8 != 1 -> (active7'=1) & (send7'=0);
[tick] active7=1 & send7=1    -> (send7'=0)& (active7'=0);
[tick] active7=0  -> (send7'=0)& (active7'=0);
endmodule

module node8
active8:[0..2] init 1;
send8:  [0..1] init 0;

[tick] active8=1 & send8=0 & send5+send7 =1 ->       (1-pdelay)*psend: (active8'=1)&(send8'=1)
                                                     +(1-pdelay)*(1-psend):(active8'=0)&(send8'=0)
                                                     +   pdelay:           (active8'=2)&(send8'=0);
[tick] active8=2                                   ->(1-pdelay)*psend: (active8'=1)&(send8'=1)
                                                     +(1-pdelay)*(1-psend):(active8'=0)&(send8'=0)
                                                     +   pdelay:           (active8'=2)&(send8'=0);
[tick] active8=1 & send8=0 & send5+send7 !=1 -> (active8'=1) & (send8'=0);
[tick] active8=1 & send8=1    -> (send8'=0)& (active8'=0);
[tick] active8=0  -> (send8'=0)& (active8'=0);
endmodule