Processus CCS pour un distributeur de boissons avec deux prix différents

Un distributeur de boissons oblige l'utilisateur à insérer une pièce de monnaie ( ), puis appuyez sur l'un des trois boutons: demande une tasse de thé , idem pour le café, et demande un remboursement (c'est-à-dire que la machine rend le pièce: ). Ce distributeur peut être modélisé par le processus CCS suivant : $\bar c$ $\bar d_{\text{tea}}$ $e_{\text{tea}}$ $\bar r$ $\bar b$

M \overset{d e f}{=} c . (d_{tea} . {\bar{e}}_{tea} . M + d_{coffee} . {\bar{e}}_{coffee} . M + r . \bar{b} . M)

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

Une guerre civile fait monter le prix du café à deux pièces, tandis que le prix du thé reste une pièce. Nous voulons une machine modifiée qui ne livre du café qu'après deux pièces et accepte un remboursement après une ou deux pièces. Comment modéliser la machine modifiée avec un processus CCS?

logic concurrency modelling process-algebras ccs Gilles 'SO- arrête d'être méchant'
la source

Qu'est-ce qu'un modèle / processus CCS? Sont-ils équivalents aux systèmes de transition étiquetés (LTS)?

Raphael

@Raphael CCS est un calcul de processus, un précurseur du calcul pi. Un modèle CCS n'est qu'un modèle dans CCS. J'ai ajouté un lien Wikipédia et un wiki de balises.

Gilles 'SO- arrête d'être méchant'

Je pense que la logique et les langages de programmation sont appropriés pour cette question. Les algèbres de processus sont étudiées dans ces domaines, et pour cette question, la logique semble plus appropriée, par exemple, veuillez vérifier les balises de zone ici .

Kaveh

Réponses:

Vous pouvez facilement profiter de la guerre de cette façon:

M \overset{d e f}{=} c . (d_{tea} . {\bar{e}}_{tea} . M + r . \bar{b} . M + c . (d_{coffee} . {\bar{e}}_{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 + r.\bar b.\bar b.M ) )$

notez que vous devez appuyer sur le remboursement pour obtenir un thé si vous mettez trop de pièces. Si vous ne le souhaitez pas, vous pouvez l'adapter (ou peut-être mettre en place un compteur (fini est suffisant)):

M \overset{d e f}{=} c . (d_{tea} . {\bar{e}}_{tea} . M + r . \bar{b} . M + c . (d_{coffee} . {\bar{e}}_{coffee} . M + d_{tea} . \bar{b} . {\bar{e}}_{tea} . 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 ) )$

jmad
la source

Je ne comprends pas ta réponse. Le premier processus que vous montrez a le prix du café à une pièce et la machine oblige d'une manière ou d'une autre l'utilisateur à insérer une pièce. Je ne vois aucun lien avec la question. Le deuxième processus semble sur la bonne voie, mais qu'est-ce que

censé faire ??

\bar{c}

$\bar c$

Gilles 'SO- arrête d'être méchant'

@ Gilles:

rend l'argent, mais il vaudrait mieux que vous nous

un autre nom pour renvoyer l'argent.

\bar{c}

$\bar c$

Stéphane Gimenez

@ StéphaneGimenez Tu as raison, j'ai ajouté ça.

Gilles 'SO- arrête d'être méchant'

@Gilles et Stéphane: vous avez raison,

est un très mauvais choix pour le remboursement. (Par exemple, vous pourriez exiger que la machine soit asynchrone:

, puis la machine pourrait la prendre elle-même, vous devrez donc être rapide pour attraper votre argent!)

\bar{c}

$\bar c$

r . (\bar{c} ∣ M)

$r.(\bar c\mid M)$

jmad

@ Gilles: J'ai aussi choisi

, indépendamment de toi. Je suppose que c'est le choix canonique :-)

\bar{b}

$\bar b$

jmad

$M_0$

M_{0} := c . M_{1}

$M_0 := c.M_1$

M_{1} := d_{tea} . {\bar{e}}_{tea} . M_{1} + r . \bar{b} . M_{0} + c . M_{2}

$M_1 := d_{\text{tea}}.\bar e_{\text{tea}}.M_1 + r.\bar b.M_0 + c.M_2$

M_{n} := d_{tea} . {\bar{e}}_{tea} . M_{n - 1} + {ré}_{café} . {\bar{e}}_{café} . M_{n - 2} + r . \underset{n}{\underset{⏟}{\bar{b} . \dots \bar{b} .}} M_{0} + c . M_{n + 1}

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

(Mais utiliser des processus infinis, c'est comme tricher).

Stéphane Gimenez
la source

J'aime l'aspect compositionnel ici. Cependant, je suppose que c'est bien pour l'automate de ne pas autoriser plus de deux pièces?

Raphael

Eh bien, cela donne également une idée de la façon de traiter les pièces de monnaie ayant des valeurs différentes :-)

Stéphane Gimenez