как перевести АБП с промела на микроклр?

Я подготовил модель ABP на языке моделирования Promela. Но мне нужна помощь, чтобы переписать его на другом языке моделирования — 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
}