Problem Detail: 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?
Asked By : Gilles
Answered By : jmad
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 ) ) $$
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/444 3.2K people like this
