mdp

const double psend;


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

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


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

[msg0] active1=1 & send1=0 -> psend:(active1'=1)&(send1'=1)+(1-psend):(active1'=0)&(send1'=0);
[msg2] active1=1 & send1=0 -> psend:(active1'=1)&(send1'=1)+(1-psend):(active1'=0)&(send1'=0);
[msg4] active1=1 & send1=0 -> psend:(active1'=1)&(send1'=1)+(1-psend):(active1'=0)&(send1'=0);
[msg0] active1=1 & send1!=0  -> (active1'=1) & (send1'=2);
[msg2] active1=1 & send1!=0  -> (active1'=1) & (send1'=2);
[msg4] active1=1 & send1!=0  -> (active1'=1) & (send1'=2);
[]     active1=1 & send1 =2  -> (active1'=1) & (send1'=0);
[msg1] active1=1 & send1=1 -> (send1'=0)& (active1'=0);
[msg0] active1=0 -> (send1'=0)& (active1'=0);
[msg2] active1=0 -> (send1'=0)& (active1'=0);
[msg4] active1=0 -> (send1'=0)& (active1'=0);
endmodule

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

[msg1] active2=1 & send2=0  -> psend:(active2'=1)&(send2'=1)+(1-psend):(active2'=0)&(send2'=0);
[msg5] active2=1 & send2=0  -> psend:(active2'=1)&(send2'=1)+(1-psend):(active2'=0)&(send2'=0);
[msg1] active2=1 & send2!=0  -> (active2'=1) & (send2'=2);
[msg5] active2=1 & send2!=0  -> (active2'=1) & (send2'=2);
[]     active2=1 & send2 =2  -> (active2'=1) & (send2'=0);
[msg2] active2=1 & send2=1    -> (send2'=0)& (active2'=0);
[msg1] active2=0 -> (send2'=0)& (active2'=0);
[msg5] active2=0 -> (send2'=0)& (active2'=0);
endmodule


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

[msg0] active3=1 & send3=0    -> psend:(active3'=1)&(send3'=1)+(1-psend):(active3'=0)&(send3'=0);
[msg4] active3=1 & send3=0    -> psend:(active3'=1)&(send3'=1)+(1-psend):(active3'=0)&(send3'=0);
[msg6] active3=1 & send3=0    -> psend:(active3'=1)&(send3'=1)+(1-psend):(active3'=0)&(send3'=0);
[msg0] active3=1 & send3!=0  -> (active3'=1) & (send3'=2);
[msg4] active3=1 & send3!=0  -> (active3'=1) & (send3'=2);
[msg6] active3=1 & send3!=0  -> (active3'=1) & (send3'=2);
[]     active3=1 & send3 =2  -> (active3'=1) & (send3'=0);
[msg3] active3=1 & send3=1    -> (send3'=0)& (active3'=0);
[msg0] active3=0 -> (send3'=0)& (active3'=0);
[msg4] active3=0 -> (send3'=0)& (active3'=0);
[msg6] active3=0 -> (send3'=0)& (active3'=0);
endmodule


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

[msg1] active4=1 & send4=0 -> psend:(active4'=1)&(send4'=1)+(1-psend):(active4'=0)&(send4'=0);
[msg3] active4=1 & send4=0 -> psend:(active4'=1)&(send4'=1)+(1-psend):(active4'=0)&(send4'=0);
[msg5] active4=1 & send4=0 -> psend:(active4'=1)&(send4'=1)+(1-psend):(active4'=0)&(send4'=0);
[msg7] active4=1 & send4=0 -> psend:(active4'=1)&(send4'=1)+(1-psend):(active4'=0)&(send4'=0);
[msg1] active4=1 & send4!=0  -> (active4'=1) & (send4'=2);
[msg3] active4=1 & send4!=0  -> (active4'=1) & (send4'=2);
[msg5] active4=1 & send4!=0  -> (active4'=1) & (send4'=2);
[msg7] active4=1 & send4!=0  -> (active4'=1) & (send4'=2);
[]     active4=1 & send4 =2  -> (active4'=1) & (send4'=0);
[msg4] active4=1 & send4=1 -> (send4'=0)& (active4'=0);
[msg1] active4=0 -> (send4'=0)& (active4'=0);
[msg3] active4=0 -> (send4'=0)& (active4'=0);
[msg5] active4=0 -> (send4'=0)& (active4'=0);
[msg7] active4=0 -> (send4'=0)& (active4'=0);
endmodule

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

[msg2] active5=1 & send5=0 -> psend:(active5'=1)&(send5'=1)+(1-psend):(active5'=0)&(send5'=0);
[msg4] active5=1 & send5=0 -> psend:(active5'=1)&(send5'=1)+(1-psend):(active5'=0)&(send5'=0);
[msg8] active5=1 & send5=0 -> psend:(active5'=1)&(send5'=1)+(1-psend):(active5'=0)&(send5'=0);
[msg2] active5=1 & send5!=0  -> (active5'=1) & (send5'=2);
[msg4] active5=1 & send5!=0  -> (active5'=1) & (send5'=2);
[msg8] active5=1 & send5!=0  -> (active5'=1) & (send5'=2);
[]     active5=1 & send5 =2  -> (active5'=1) & (send5'=0);
[msg5] active5=1 & send5=1 -> (send5'=0)& (active5'=0);
[msg2] active5=0 -> (send5'=0)& (active5'=0);
[msg4] active5=0 -> (send5'=0)& (active5'=0);
[msg8] active5=0 -> (send5'=0)& (active5'=0);
endmodule

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

[msg3] active6=1 & send6=0 -> psend:(active6'=1)&(send6'=1)+(1-psend):(active6'=0)&(send6'=0);
[msg7] active6=1 & send6=0 -> psend:(active6'=1)&(send6'=1)+(1-psend):(active6'=0)&(send6'=0);
[msg3] active6=1 & send6!=0  -> (active6'=1) & (send6'=2);
[msg7] active6=1 & send6!=0  -> (active6'=1) & (send6'=2);
[]     active6=1 & send6 =2  -> (active6'=1) & (send6'=0);
[msg6] active6=1 & send6=1 -> (send6'=0)& (active6'=0);
[msg3] active6=0 -> (send6'=0)& (active6'=0);
[msg7] active6=0 -> (send6'=0)& (active6'=0);
endmodule

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

[msg4] active7=1 & send7=0 -> psend:(active7'=1)&(send7'=1)+(1-psend):(active7'=0)&(send7'=0);
[msg6] active7=1 & send7=0 -> psend:(active7'=1)&(send7'=1)+(1-psend):(active7'=0)&(send7'=0);
[msg8] active7=1 & send7=0 -> psend:(active7'=1)&(send7'=1)+(1-psend):(active7'=0)&(send7'=0);
[msg4] active7=1 & send7!=0  -> (active7'=1) & (send7'=2);
[msg6] active7=1 & send7!=0  -> (active7'=1) & (send7'=2);
[msg8] active7=1 & send7!=0  -> (active7'=1) & (send7'=2);
[]     active7=1 & send7 =2  -> (active7'=1) & (send7'=0);
[msg7] active7=1 & send7=1 -> (send7'=0)& (active7'=0);
[msg4] active7=0 -> (send7'=0)& (active7'=0);
[msg6] active7=0 -> (send7'=0)& (active7'=0);
[msg8] active7=0 -> (send7'=0)& (active7'=0);
endmodule

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

[msg5] active8=1 & send8=0 -> psend:(active8'=1)&(send8'=1)+(1-psend):(active8'=0)&(send8'=0);
[msg7] active8=1 & send8=0 -> psend:(active8'=1)&(send8'=1)+(1-psend):(active8'=0)&(send8'=0);
[msg5] active8=1 & send8!=0  -> (active8'=1) & (send8'=2);
[msg7] active8=1 & send8!=0  -> (active8'=1) & (send8'=2);
[]     active8=1 & send8 =2  -> (active8'=1) & (send8'=0);
[msg8] active8=1 & send8=1 -> (send8'=0)& (active8'=0);
[msg5] active8=0 -> (send8'=0)& (active8'=0);
[msg7] active8=0 -> (send8'=0)& (active8'=0);
endmodule