**********************************************************************
*  jobshop
*
*  This is a specification of the "Jobshop" system, described in
*  Milner's book.  The value-passing system has been suitably
*  translated into the pure calculus.
*
*  The definition of "Jobshop" assumes a tool is replaced before the
*  job is output, whereas the modified system "Jobshop'" outputs a job
*  before replacing the tool used for that job.  The first can be
*  shown to be equivalent to two "Strongjobber"'s working together,
*  whereas the latter is different. This distinction can be realised
*  using the "check proposition" command to note that it is possible
*  for the system "Jobshop'" to input a hard job at some point, and
*  then not be able to output that hard job right away; that is, it
*  doesn't satisfy the proposition Bx ([inHard]<<'outHard>>T).  The
*  definition of the Box operator "Bx" is given below.
**********************************************************************
**********************************************************************
*  The definition of the "Hammer"
**********************************************************************
agent Hammer = geth.puth.Hammer;
**********************************************************************
*  The definition of the "Mallet"
**********************************************************************
agent Mallet = getm.putm.Mallet;
**********************************************************************
*  The normal system "Jobshop"
**********************************************************************
agent Jobshop = (Jobber | Jobber | Hammer | Mallet)\{geth,puth,getm,putm};
agent Jobber = inEasy.'outEasy.Jobber + inHard.UsehammerHard + inNormal.Usetool;
agent Usetool = UsehammerNormal + Usemallet;
agent UsehammerNormal = 'geth.'puth.'outNormal.Jobber;
agent UsehammerHard = 'geth.'puth.'outHard.Jobber;
agent Usemallet = 'getm.'putm.'outNormal.Jobber;
**********************************************************************
*  The redefined system "Jobshop'"
**********************************************************************
agent Jobshop' = (Jobber' | Jobber' | Hammer | Mallet)\{geth,puth,getm,putm};
agent Jobber' = inEasy.'outEasy.Jobber' + inHard.UsehammerHard' + inNormal.Usetool';
agent Usetool' = UsehammerNormal' + Usemallet';
agent UsehammerNormal' = 'geth.'outNormal.'puth.Jobber';
agent UsehammerHard' = 'geth.'outHard.'puth.Jobber';
agent Usemallet' = 'getm.'outNormal.'putm.Jobber';
**********************************************************************
*  The specification for the "Strongjobber" which needs no tools
**********************************************************************
agent Strongjobber = inEasy.'outEasy.Strongjobber + inNormal.'outNormal.Strongjobber + inHard.'outHard.Strongjobber;
**********************************************************************
*  The definition of the Box (necessity) temporal operator "Bx"
**********************************************************************
prop Bx(P) =      max(Z.P & [-]Z);

* These are equal, i.e. observationally congruent:
* cong (Jobshop, Strongjobber|Strongjobber);
* * but not strongly bisimilar:
* strongeq (Jobshop, Strongjobber|Strongjobber);
* * as shown e.g. by
* dfstrong (Jobshop, Strongjobber|Strongjobber);
* * The modified Jobshop' is trace equivalent to the Jobshop:
* mayeq (Jobshop, Jobshop');
* dftrace (Jobshop, Jobshop');
* * but not much more:
* eq (Jobshop, Jobshop');
* dfweak (Jobshop, Jobshop');
* cp (Jobshop, Bx ([inHard]<<'outHard>>T));
* cp (Jobshop', Bx ([inHard]<<'outHard>>T));