26 lines
376 B
Promela

mtype = { nice, rude };
chan request = [0] of { mtype };
chan reply = [0] of { mtype };
active [2] proctype Server() {
mtype msg;
end:
do
:: request ? msg ->
reply ! msg
od
}
active proctype NiceClient() {
mtype msg;
request ! nice;
reply ? msg;
assert( msg == nice )
}
active proctype RudeClient() {
mtype msg;
request ! rude;
reply ? msg
}