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 '12 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$ – Gilles 'SO- stop being evil' Mar 17 '12 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 '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 ) ) $$

| cite | improve this answer | |
  • $\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$ – Gilles 'SO- stop being evil' Mar 17 '12 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$ – Stéphane Gimenez Mar 17 '12 at 1:17
  • $\begingroup$ @StéphaneGimenez You're right, I've added that. $\endgroup$ – Gilles 'SO- stop being evil' Mar 17 '12 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 '12 at 1:32
  • $\begingroup$ @Gilles: I chose $\bar b$ too, independently of you. I guess this is the canonical choice :-) $\endgroup$ – 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).

| cite | improve this answer | |
  • $\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 '12 at 10:59
  • $\begingroup$ Well this also gives an idea of how to deal with coins that have different values :-) $\endgroup$ – Stéphane Gimenez Mar 17 '12 at 13:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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