smg player p1 host, [send1], [send2] endplayer player p2 client endplayer module host h : [0..2] init 0; [send1] h=0 -> (h'=1); // send message 1 [send2] h=0 -> (h'=2); // send message 2 [] c=0 -> (h'=0); // restart endmodule module client c : [0..2] init 0; [send1] c=0 -> 0.85 : (c'=1) + 0.15 : (c'=0); // receive message 1 [send2] c=0 -> 0.85 : (c'=2) + 0.15 : (c'=0); // receive message 2 [] c!=0 -> (c'=0); // request another message [] c!=0 -> true; // wait endmodule