Модель Promela со спином - дублирующее сообщение и поврежденное сообщение - PullRequest
Новая
       42

Модель Promela со спином - дублирующее сообщение и поврежденное сообщение

0 голосов
/ 14 января 2019

У меня есть этот код promela, и мне нужно смоделировать дублирование сообщений и их повреждение, а также мне нужно добавить механизмы для обнаружения и обработки поврежденных сообщений и дублирования сообщений

из моего чтения я обнаружил, что мне нужно добавить новые процессы, один для дублирования сообщения, а другой для повреждения сообщения. Также для обнаружения дубликата мне нужно добавить порядковый номер, а для искажения - контрольную сумму. мои навыки в pormela не могли помочь мне перенести эту информацию в код. если вы можете помочь или знаете полезный сайт, я буду признателен 

chan linkA = [1] of {byte};
chan linkB = [1] of {byte};
proctype sender (chan link; byte first)
{ byte n=first;
do
:: n <= 10 -> link!n; n=n+2
:: else -> break
od
}
proctype receiver ()
{ byte m, totaleven, totalodd;
do
:: linkA?m -> totaleven=totaleven+m
:: linkB?m -> totalodd=totalodd+m
od
}
init
{
run sender (linkA,2);
run sender (linkB,1);
run receiver ()
}

1 Ответ

0 голосов
/ 14 января 2019

Поскольку это выглядит как упражнение, вместо того, чтобы предоставить вам правильное решение, я постараюсь просто дать вам несколько советов.

  • дублирование сообщения : вместо отправки сообщения один раз, добавьте вариант ветвления для отправки сообщения дважды, аналогично следующему: 

    if
    :: channel!MSG(value, seq_no, checksum)
    :: channel!MSG(value, seq_no, checksum);
       channel!MSG(value, seq_no, checksum); // msg. duplication
    :: true; // msg. loss
fi

    На стороне получателя вы справляетесь с дублированием и потерей, проверяя значение seq_no. Когда сообщение дублируется, вы отбрасываете его. Когда (предыдущее) сообщение отсутствует, вы отбрасываете (для простоты) текущее сообщение и просите, чтобы сообщение с желаемым seq_no было отправлено снова, например, 

    channel!NACK(seq_no)

  • повреждение сообщения : сначала вычислите контрольную сумму, а затем измените содержимое value

    checksum = (seq_no ^ value) % 2
select(value : 1 .. 100)
...
channel!MSG(value, seq_no, checksum);

    checksum очень просто, я не думаю, что это имеет значение для целей упражнения. На стороне получателя вы вычисляете контрольную сумму полученных данных и сравниваете ее со значением контрольной суммы в сообщении. Если это не хорошо, вы просите, чтобы оно было отправлено снова.

...