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
}
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.