Внесите поправки в модель Promela, приведенную выше, с механизмом искажения сообщений.
Я готовлюсь к итоговому экзамену по проверке системы, и этот вопрос был в последней экзаменационной работе. Мне нужна помощь, чтобы решить это.
Интуитивно, отправитель отправляет квадраты первых пяти неотрицательных целых чисел двум процессам-получателям. Каждое число отправляется только один раз, и выбор получателя, которому он отправляется, является случайным. а) Предположим, что каналы могут испортить сообщения. Внесите поправки в вышеупомянутую модель Promela с помощью механизма для повреждения сообщений, а также механизмов для обнаружения и обработки поврежденных сообщений. В вашем решении вы можете добавлять новые каналы, переменные, процессы, изменять тип сообщений и т. Д.
chan linkA = [5] of {byte};
chan linkB = [5] of {byte};
proctype sender ()
{ byte n;
do
:: n < 5 -> linkA!n*n; n++
:: n < 5 -> linkB!n*n; n++
:: else -> break
od
}
proctype receiver (chan link)
{ byte m, total;
do
:: link?m -> total=total+m
od
}
init
{
run sender (); run receiver (linkA);
run receiver (linkB)
}