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?

  • 1
    $\begingroup$ What is a CCS model/process? Are they equivalent to labeled transition systems (LTS)? $\endgroup$
    – Raphael
    Mar 17, 2012 at 10:55
  • 1
    $\begingroup$ @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. $\endgroup$ Mar 17, 2012 at 13:24
  • $\begingroup$ 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. $\endgroup$
    – Kaveh
    Mar 26, 2012 at 18:20

2 Answers 2


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

  • $\begingroup$ 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?? $\endgroup$ Mar 17, 2012 at 1:11
  • $\begingroup$ @Gilles: $\bar c$ gives back the money, but it would be better I you gave us another name to send back the money. $\endgroup$ Mar 17, 2012 at 1:17
  • $\begingroup$ @StéphaneGimenez You're right, I've added that. $\endgroup$ Mar 17, 2012 at 1:20
  • $\begingroup$ @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!) $\endgroup$
    – jmad
    Mar 17, 2012 at 1:32
  • $\begingroup$ @Gilles: I chose $\bar b$ too, independently of you. I guess this is the canonical choice :-) $\endgroup$
    – jmad
    Mar 17, 2012 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).

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.