**********************************************************************
*  csma   (written by Joachim Parrow)
*
*  This file contains a development of the "Carrier Sense/Multiple
*  Access with Collision Detection" protocol.
*
*  The specification is the agent "SSCS", and the implementation is
*  "CSPROT".
*
*  A complete description of this development of the protocol can be
*  found in the Edinburgh University technical report ECS-LFCS-86-18
*  by Joachim Parrow, entitled "Verifying a CSMA/CD Protocol with
*  CCS".
* ' replaces * in identifiers, since in v7 * is only the comment character.
**********************************************************************
agent MAC1 = send1.MAC1' + br1.(er1.('rec1.MAC1 + send1.'rec1.MAC1') + send1.er1.'rec1.MAC1');
agent MAC1' = 'b1.(c1.MAC1' + 'e1.MAC1) + br1.er1.'rec1.MAC1';
agent MAC2 = MAC1[b2/b1, e2/e1, c2/c1, br2/br1, er2/er1, send2/send1, rec2/rec1];
agent M = b1.(b2.M' + 'br2.(b2.M' +e1.(b2.M' + 'er2.M))) + b2.(b1.M' + 'br1.(b1.M' +e2.(b1.M' + 'er1.M)));
agent M' = 'c1.'c2.M + 'c2.'c1.M;
agent CSPROT = (MAC1 | M | MAC2)\{b1,e1,br1,er1,c1,b2,e2,br2,er2,c2};
agent B12 = send1.B12';
agent B12' = p.(send1.'rec2.v.B12' + 'rec2.v.B12);
agent B21 = B12[send2/send1, rec1/rec2];
agent SE = 'p.'v.SE;
agent SSCS = (B12 | SE | B21)\{p,v};