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. – Gilles 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. – Kaveh 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?? – Gilles 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. – Stéphane Gimenez Mar 17 '12 at 1:17
• @StéphaneGimenez You're right, I've added that. – Gilles 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!) – jmad Mar 17 '12 at 1:32
• @Gilles: I chose $\bar b$ too, independently of you. I guess this is the canonical choice :-) – jmad 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 :-) – Stéphane Gimenez Mar 17 '12 at 13:21