1

我是 SPIN 和 Promela 的初学者。我正在尝试使用 JSPIN 软件模拟 TFTP（普通文件传输协议）。我已经完成了大部分模拟。但是，我遇到了一个问题。对我来说，模拟丢包后发送方或接收方超时是很重要的。我可以通过使用关键字“超时”来模拟超时。但是，这次超时似乎没有像我预期的那样工作。只有在流程中没有其他选择要执行时，此超时才有效。但是，我希望在数据包丢失或数据包重复之后发生的特定时间段后超时工作。因此，我的问题是“如何模拟 SPIN 中的数据包丢失并在超时后跟随它？”

下面是我的代码。

mtype {MSG, ACK, RRQ, WRQ};
chan toS = [3] of {mtype, byte, short};
chan toR = [3] of {mtype, byte, short};
bool readRequest=1;
bool writeRequest=1;

proctype Receiver(chan IN,OUT)
{
byte recvbit;
short size;


do 

:: readRequest==1 -> 

atomic{
readRequest=0;
size=512;
OUT ! RRQ, recvbit, size;
}

:: IN ? WRQ, recvbit, size 
-> OUT ! ACK, recvbit, size;


:: IN ? MSG, recvbit, size 
-> 


response:
atomic {


OUT ! ACK, recvbit, size;

if 
  ::size<512 ->
    if
       ::timeout -> break;
       ::IN ? MSG, recvbit, size -> goto response;
     fi
  ::else
fi;
}

:: timeout -> OUT ! ACK, recvbit, size;

od
}


proctype Sender(chan IN,OUT)
{

byte recvbit;
short size=512;
int repeat=0;
do


:: IN ? RRQ, recvbit, size ->
atomic{

  recvbit=(recvbit+1)%8; 
  size= size - (repeat/2); //after 10 times it becomes 511;
  OUT ! MSG, recvbit,size;
  repeat++;
}

:: writeRequest==1 ->
atomic {
writeRequest=0;
size= size - (repeat/10);
OUT ! WRQ, recvbit,size;
repeat++;

}


:: IN ? ACK, recvbit, size -> 
atomic {


if 
  :: size < 512 -> break;
  :: else ->
  recvbit=(recvbit+1)%8; 
  size= size - (repeat/2); //after 10 times it becomes 511;
  OUT ! MSG, recvbit,size;
  repeat++;
fi


}

:: timeout -> 
atomic {
size= size - (repeat/10);
OUT ! MSG, recvbit,size;
repeat++;

}

od
}


init
{
run Sender(toS, toR);
run Receiver (toR, toS);
}
4

1 回答 1

1

以下示例使用该Demon过程来模拟“丢失”的消息：

chan sendChan = [1] of {bit};
chan replyChan = [1] of {bit};

active proctype Sender() {
  bit replyVal, value = 1;
  do
  :: sendChan ! value -> /*Send msg over sendChan*/
    if
      :: replyChan ? replyVal;  /*Wait for a reply*/
      :: timeout;              /*or timeout if none*/   
    fi
  od
}

active proctype Reciever() {
  bit msg;
  do
    :: sendChan ? msg -> replyChan ! 1; /*Reciever gets msg, sends reply*/
  od
}

active proctype Demon() {
  do
    :: sendChan ? _ ; /*Msg stolen from sendChan!*/
  od
}

在此Demon过程中，_in:: sendChan ? _ ;将读取并丢弃通道中的任何消息。

或者，有一个交替位协议（第二个模型）的实现，它在 's do 循环中使用一个额外的选项Reciever来模拟消息丢失，而不是一个单独的过程。

于 2013-02-15T18:39:01.130 回答