mirror of
https://github.com/tu-darmstadt-informatik/Tu-Darmstadt-Informatik-Kurse.git
synced 2025-12-13 09:55:48 +00:00
28 lines
451 B
Promela
28 lines
451 B
Promela
mtype = { nice, rude };
|
|
chan request = [0] of { mtype, chan };
|
|
|
|
active [2] proctype Server() {
|
|
mtype msg; chan reply;
|
|
end:
|
|
do
|
|
:: request ? msg, reply ->
|
|
reply ! msg
|
|
od
|
|
}
|
|
|
|
active proctype NiceClient() {
|
|
chan reply = [0] of { mtype };
|
|
mtype msg;
|
|
request ! nice, reply;
|
|
reply ? msg;
|
|
assert( msg == nice )
|
|
}
|
|
|
|
active proctype RudeClient() {
|
|
chan reply = [0] of { mtype };
|
|
mtype msg;
|
|
request ! rude, reply;
|
|
reply ? msg
|
|
}
|
|
|