Proces CCS dla dystrybutora napojów w dwóch różnych cenach

Dozownik napojów wymaga od użytkownika włożenia monety ( $\bar c$ ), a następnie naciśnięcia jednego z trzech przycisków: prosi o filiżankę herbaty , to samo na kawę, i prosi o zwrot pieniędzy (tzn. maszyna zwraca monetę: ). Dozownik można modelować za pomocą następującego procesu CCS :eherbaty ˉ R ˉ $\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)$$

Wojna domowa podnosi cenę kawy do dwóch monet, podczas gdy cena herbaty pozostaje jedną monetą. Chcemy zmodyfikowanego urządzenia, które dostarcza kawę dopiero po dwóch monetach, i przyznaje zwrot pieniędzy po jednej lub dwóch monetach. Jak możemy modelować zmodyfikowaną maszynę za pomocą procesu CCS?

W ten sposób możesz łatwo czerpać zyski z działań wojennych:

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

pamiętaj, że musisz wcisnąć zwrot, aby dostać herbatę, jeśli włożysz zbyt wiele monet. Jeśli tego nie chcesz, możesz go dostosować (lub może skonfigurować licznik (wystarczy skończonego)):

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

Ta maszyna jest wygodniejsza niż ta, którą proponujesz:$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}$$

(Ale używanie nieskończonych procesów jest jak oszustwo).