1

私は SPIN と Promela の初心者です。JSPIN ソフトウェアを使用して TFTP (Trivial File Transfer Protocol) をシミュレートしようとしています。ほとんどのシミュレーションを行いました。しかし、私は問題で立ち往生しています。送信者または受信者によるタイムアウトが続くパケット損失をシミュレートすることが重要です。「タイムアウト」というキーワードを使用して、タイムアウトをシミュレートできました。ただし、今回のタイムアウトは期待どおりに機能していないようです。このタイムアウトは、プロセスで他に実行する選択肢がない場合にのみ機能します。ただし、パケットの損失またはパケットの重複の後に発生する特定の期間の後に、そのタイムアウトが機能することを望みます。したがって、私の質問は、「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 ? _ ;はチャネル内のすべてのメッセージを読み取って破棄します。

別の方法として、別のプロセスではなく、メッセージの損失をシミュレートするために の do ループで追加のオプションを使用するオルタネーティング ビット プロトコル(2 番目のモデル)の実装があります。Reciever

于 2013-02-15T18:39:01.130 に答える