Processo CCS para um dispensador de bebidas com dois preços diferentes

Um dispensador de bebidas exige que o usuário insira uma moeda ( ) e pressione um dos três botões: solicita uma xícara de chá , o mesmo para café , e solicita um reembolso (ou seja, a máquina devolve a moeda: ). Este dispensador pode ser modelado pelo seguinte processo CCS :ˉ d cháechá ˉ r ˉ $\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)$$

Uma guerra civil aumenta o preço do café para duas moedas, enquanto o preço do chá permanece uma moeda. Queremos uma máquina modificada que entregue café somente após duas moedas e aceite um reembolso após uma ou duas moedas. Como podemos modelar a máquina modificada com um processo CCS?

Você pode facilmente lucrar com a guerra dessa maneira:

$$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 que você deve pressionar restituição para tomar um chá se colocar muitas moedas. Se você não quiser, pode adaptá-lo (ou talvez configurar um contador (finito é suficiente)):

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

Esta máquina é mais conveniente do que a que você propõe:$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}$$

(Mas usar processos infinitos é como trapacear).