Я готовлюсь к выпускному экзамену по валидации системы, и этот вопрос был в последней экзаменационной работе.Мне нужна помощь, чтобы решить ее.
Интуитивно, отправитель отправляет квадраты первых пяти неотрицательных целых чисел двум процессам-получателям.Каждое число отправляется только один раз, и выбор получателя, которому он отправляется, является случайным.а) Предположим, что каналы могут испортить сообщения.Внесите поправки в вышеупомянутую модель 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)
}