
// The Alternating Bit Protocol modelled by James Edwards in // the paper "Process Algebras for Protocol Validation and Analysis", // Proceedings of PREP 2001. def = 1.25; retry = 10.5; loss = 0.001; S0 = (gm, def).(send0, def).S1; S1 = (gm, def).S2 + (time0, retry).S3 + (ack0, infty).S5 + (ack1, infty).S1; S2 = (time0, retry).S4 + (ack0, infty).S6 + (ack1, infty).S2; S3 = (send0, def).S1; S4 = (send0, def).S2; S5 = (gm, def).(send1, def).S7; S6 = (send1, def).S7; S7 = (gm, def).S8 + (time1, retry).S6 + (ack0, infty).S7 + (ack1, infty).S0; S8 = (time1, retry).S9 + (ack0, infty).S8 + (ack1, infty).S3; S9 = (send1, def).S8; R0 = (recv0, infty).(cm, def).(a0, def).R1; R1 = (recv0, infty).(a0, def).R1 + (recv1, infty).R2; R2 = (cm, def).(a1, def).R3; R3 = (recv1, infty).(a1, def).R3 + (recv0, infty).R4; R4 = (cm, def).(a0, def).R1; M0 = (send0, infty).M1 + (send1, infty).M2 + (a0, infty).M3 + (a1, infty).M4; M1 = (drop, loss).M0 + (recv0, def).M0; M2 = (drop, loss).M0 + (recv1, def).M0; M3 = (drop, loss).M0 + (ack0, def).M0; M4 = (drop, loss).M0 + (ack1, def).M0; (S0 <send0, send1, ack0, ack1> M0) <recv0, recv1, a0, a1> R0 
Contact addresses:
Jane Hillston and
Stephen Gilmore,
{jeh,stg}@inf.ed.ac.uk.
Laboratory for Foundations of Computer Science,
The University of Edinburgh.
Last modified:
Sun 25 Aug 2013 08:12:06 BST