18 lines
272 B
Promela

mtype = {hi, bye};
chan ch = [0] of {mtype};
active proctype Server () {
mtype msg;
read:
ch ? msg;
do
:: msg == hi -> printf("Hello.\n"); goto read
:: msg == bye -> printf("See you.\n"); break
od
}
active proctype Client() {
ch ! hi; ch ! bye
}