modeling - 如何将 ABP 从 promela 转换为 microclr？

Question

我已经用 Promela 建模语言准备了一个 ABP 模型。但是我需要一些帮助来用另一种建模语言 - mCRL 重写它。我没有任何经验。有人可以告诉我一个开始的方法，或者给我指出 mCRL 的好教程吗？无论如何， mCRL 和 mCRL2 之间的代码有区别吗？

我在 promela 中的代码：

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
}

Answer 1

不再积极支持 mCRL。我认为它甚至不能用最新的 GCC 编译。mCRL2 来源中实际上有一个示例 ABP 模型：https ://svn.win.tue.nl/repos/MCRL2/trunk/examples/academic/abp/abp.mcrl2 。