# 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?

• What is a CCS model/process? Are they equivalent to labeled transition systems (LTS)?
– Raphael
Mar 17 '12 at 10:55
• @Raphael CCS is a process calculus, a precursor of the pi calculus. A CCS model is just a model in CCS. I've added a Wikipedia link and a tag wiki. Mar 17 '12 at 13:24
• I think logic and programming-languages are appropriate for this question. Process algebras are studied in these areas, and for this question logic seems more appropriate one, e.g. please check the area tags here. Mar 26 '12 at 18:20

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 ) )$$

• I don't understand your answer. The first process you show has the price of coffee at one coin, and has the machine somehow cause the user to insert a coin. I don't see any connection with the question. The second process looks on the right track, but what's $\bar c$ supposed to do?? Mar 17 '12 at 1:11
• @Gilles: $\bar c$ gives back the money, but it would be better I you gave us another name to send back the money. Mar 17 '12 at 1:17
• @StéphaneGimenez You're right, I've added that. Mar 17 '12 at 1:20
• @Gilles and Stéphane: you are right, $\bar c$ is a very bad choice for the refund. (For example you could require the machine to be asynchronous: $r.(\bar c\mid M)$ and then the machine could take it itself so you'll need to be quick to catch your money!)
Mar 17 '12 at 1:32
• @Gilles: I chose $\bar b$ too, independently of you. I guess this is the canonical choice :-)
Mar 17 '12 at 1:39

This $M_0$ machine is more convenient than the one you propose:

$$M_0 := c.M_1$$

$$M_1 := d_{\text{tea}}.\bar e_{\text{tea}}.M_1 + r.\bar b.M_0 + c.M_2$$

$$M_{n} := d_{\text{tea}}.\bar e_{\text{tea}}.M_{n-1} + d_{\text{coffee}}.\bar e_{\text{coffee}}.M_{n-2} + r.\underbrace{\bar b.\dots\bar b.}_{n}M_0 + c.M_{n+1}$$

(But using infinite processes is like cheating).

• I like the compositional aspect here. However, I guess it is fine for the automaton to not allow more than two coins?
– Raphael
Mar 17 '12 at 10:59
• Well this also gives an idea of how to deal with coins that have different values :-) Mar 17 '12 at 13:21