0

Promela モデリング言語で ABP モデルを用意しました。しかし、別のモデリング言語である mCRL で書き直すには、助けが必要です。私はその経験がありません。誰かが開始方法を教えてくれますか、または mCRL の良いチュートリアルを教えてくれませんか? とにかく、 mCRL と mCRL2 のコードに違いはありますか?

プロメラの私のコード:

mtype = { msg, ack }
chan to_sender = [2] of { mtype, bit };
chan to_recvr  = [2] of { mtype, bit };


active proctype Sender()
{
  bit s_out=0, s_in;
  do
  :: to_recvr!msg,s_out ->
     if
     :: to_sender?ack,s_in ->
        if
        :: s_in == s_out ->
end:         s_out = !s_out
        :: else -> 
            skip
        fi
     :: timeout
     fi
  od
}

active proctype Receiver()
{ 
  bit s_in, s_exp = 0;
  do
  :: to_recvr?msg,s_in ->
       to_sender!ack,s_in;
     if
     :: s_in == s_exp ->
end:       s_exp = !s_exp
     :: else -> 
        skip
     fi
  :: to_recvr?msg,s_in -> skip
  od
}
4

1 に答える 1

0

mCRL は現在積極的にサポートされていません。最新のGCCでもコンパイルできないと思います。実際には、mCRL2 ソースに ABP モデルの例があります: https://svn.win.tue.nl/repos/MCRL2/trunk/examples/academic/abp/abp.mcrl2。

于 2015-03-25T09:05:33.517 に答える