**********************************************************************
*  vending-machine
*
*  This is a specification of the "user friendly" vending machine
*  described on pages 23-24 of Milner's book.  The machine "VM" will
*  accept 1p and 2p coins (actions "in1" and "in2") and deliver either
*  little chocolates (worth 1p) or big chocolates (worth 2p) upon
*  under the following constraints:
*           #  the machine can never make a profit nor a loss;
*           #  the machine cannot hold a credit of more than 4p;
*           #  a chocolate cannot be requested if one has previously
*              been delivered but not yet collected.
*  The last of these constraints can be confirmed using the hiding of
*  coin inputs to see that what remains repeatedly does a request for
*  a chocolate followed by the collection of the chocolate (which is
*  given by the agents "VMnew" and "VMnewSpec" below).
**********************************************************************
agent VM = VM0;
agent VM0 = in1.VM1 + in2.VM2;
agent VM1 = in1.VM2 + in2.VM3 + little.VM0';
agent VM2 = in1.VM3 + in2.VM4 + little.VM1' + big.VM0';
agent VM3 = in1.VM4 + little.VM2' + big.VM1';
agent VM4 = little.VM3' + big.VM2';
agent VM0' = in1.VM1' + in2.VM2';
agent VM1' = in1.VM2' + in2.VM3' + collect.VM1;
agent VM2' = in1.VM3' + in2.VM4' + collect.VM2;
agent VM3' = in1.VM4' + collect.VM3;
agent VM4' = collect.VM4;
**********************************************************************
*  Here we define the vending machine with the coin input actions
*  hidden away ("VMnew"), as well as its specification ("VMnewSpec").
**********************************************************************
agent VMnew = VM[tau/in1,tau/in2];
agent VMnewSpec = big.collect.VMnewSpec + little.collect.VMnewSpec;