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