**********************************************************************
*  peterson-2   (written by David Walker)
*
*  This file contains a development of Peterson's mutual exclusion
*  algorithm for two processes.
*
*  The specification is the agent "Spec", and the implementation is
*  "Peterson-2".
*
*  A complete description of this development of the algorithm can be
*  found in the Edinburgh University technical report ECS-LFCS-89-91
*  by David Walker, entitled "Automated Analysis of Mutual Exclusion
*  Algorithms using CCS".
**********************************************************************
agent B1f = 'b1rf.B1f + b1wf.B1f + b1wt.B1t;
agent B1t = 'b1rt.B1t + b1wt.B1t + b1wf.B1f;
agent B2f = 'b2rf.B2f + b2wf.B2f + b2wt.B2t;
agent B2t = 'b2rt.B2t + b2wt.B2t + b2wf.B2f;
agent K1 = 'kr1.K1 + kw1.K1 + kw2.K2;
agent K2 = 'kr2.K2 + kw2.K2 + kw1.K1;
agent P1 = 'b1wt.'kw2.P11;
agent P11 = b2rt.P11 + b2rf.P12 + kr2.P11 + kr1.P12;
agent P12 = enter.exit.'b1wf.P1;
agent P2 = 'b2wt.'kw1.P21;
agent P21 = b1rf.P22 + b1rt.P21 + kr1.P21 + kr2.P22;
agent P22 = enter.exit.'b2wf.P2;
agent Pre-Peterson-2 = P1 | P2 | K1 | B1f | B2f;
set L = {b1rf,b1rt,b1wf,b1wt,b2rf,b2rt,b2wf,b2wt,kr1,kr2,kw1,kw2};
agent Peterson-2 = Pre-Peterson-2\L;
agent Spec = enter.exit.Spec;