CCS процесс для диспенсера для напитков с двумя разными ценами

Диспенсер для напитков требует, чтобы пользователь вставил монету ( ), а затем нажмите одну из трех кнопок: запрашивает чашку чая , то же самое для кофе , и запрашивает возврат (т. е. автомат возвращает монету: ). Этот дозатор может быть смоделирован следующим процессом CCS :$\bar c$$\bar d_{\text{tea}}$$e_{\text{tea}}$$\bar r$$\bar b$

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

Гражданская война поднимает цену на кофе до двух монет, а цена чая остается одной монетой. Мы хотим модифицированную машину, которая доставляет кофе только после двух монет и соглашается на возврат денег после одной или двух монет. Как мы можем смоделировать модифицированную машину с процессом CCS?

Вы можете легко получить прибыль от войны таким образом:

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

обратите внимание, что вы должны нажать возврат, чтобы получить чай, если вы положили слишком много монет. Если вы не хотите этого, вы можете адаптировать его (или, возможно, настроить счетчик (достаточно конечного)):

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

Эта машина более удобна, чем та, которую вы предлагаете:$M_0$

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

(Но использование бесконечных процессов похоже на обман).