CCS process for a drink dispenser with two different prices

A drink dispenser requires the user to insert a coin ($\bar c$), then press one of three buttons: $\bar d_{\text{tea}}$ requests a cup of tea $e_{\text{tea}}$, ditto for coffee, and $\bar r$ requests a refund (i.e. the machine gives back the coin: $\bar b$). This dispenser can be modeled by the following CCS process:

$$ M \stackrel{\mathrm{def}}= c.(d_{\text{tea}}.\bar e_{\text{tea}}.M + d_{\text{coffee}}.\bar e_{\text{coffee}}.M + r.\bar b.M)$$

A civil war raises the price of coffee to two coins, while the price of tea remains one coin. We want a modified machine that delivers coffee only after two coins, and acquiesces to a refund after either one or two coins. How can we model the modified machine with a CCS process?

You can easily profit from warfare that way:

$$ M \stackrel{\mathrm{def}} =
c.(
d_{\text{tea}}.\bar e_{\text{tea}}.M
+ r.\bar b.M
+ c.(
d_{\text{coffee}}.\bar e_{\text{coffee}}.M
+ r.\bar b.\bar b.M
)
)
$$

note that you have to press refund to get a tea if you put too many coins. If you don't want that, you can adapt it (or maybe set up a (finite is enough) counter) :

$$ M \stackrel{\mathrm{def}} =
c.(
d_{\text{tea}}.\bar e_{\text{tea}}.M
+ r.\bar b.M
+ c.(
d_{\text{coffee}}.\bar e_{\text{coffee}}.M
+ d_{\text{tea}}.\bar b.\bar e_{\text{tea}}.M
+ r.\bar b.\bar b.M
)
)
$$

StackExchange Computer Science Q#444, answer score: 9