Search code examples
modelingpromela

how to transform ABP from promela to microclr?


I've prepared an ABP model in Promela modeling language. But I'd need some help with rewriting it in another modelling language - mCRL. I do not have any experience in it. Could someone, please, show me a way to start, or point me to good tutorial for mCRL ? Anyway, is there a difference in code between mCRL and mCRL2 ?

my code in 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
}

Solution

  • mCRL is not actively supported anymore. I think it does not even compile with the newest GCC. There is actually an example ABP model in the mCRL2 sources: https://svn.win.tue.nl/repos/MCRL2/trunk/examples/academic/abp/abp.mcrl2.