Relabelling

Data la funzione $\:f:Act_{\tau} \rightarrow Act_{\tau}\:$ (quindi associa un'etichetta di azione con un'altra) si ottiene l'operatore statico $[f]$ chiamato relabelling (relabelling o renaming). Con esso si possono rinominare le azioni di un sistema in modo da gestire meglio la sincronizzazione e l'interleaving.

La f rispetta le seguenti regole:

$$f(\tau) = \tau$$   perché non si può rinominare l'azione interna$$$$

$$f(\overline{\alpha}) = \overline{f(\alpha)}$$   quindi si rietichettano anche i complementari

L'unica regola di transizione è molto semplice:

$$\renewcommand {\arraystretch}{1.2} \begin{array}{c}E \stackrel{\... ... \hline E[f] \: \stackrel{f(\alpha)}{\longrightarrow} \: E'[f] \end{array}$$

quindi $E[f]$ esegue le stesse transizioni di E eventualmente rinominate.

Le coppie della funzione possono anche essere scritte esplicitamente sotto la forma $[l_1'/l_1 , \cdots ,l_n'/l_n]$ assumendo che, per tutte le azioni $\alpha$ che non sono espresse dagli $l_i$, si abbia $\: f(\alpha) = \alpha \:$.

Il relabelling viene solitamente fatto per assicurare che i processi composti si sincronizzino sulle azioni desiderate. Per esempio vediamo come si comporta un processo Server che fornisce un servizio invocato dal Client:

$$\textsc{Client} \: \stackrel{{def}}{{=}}\: \overline{call}.wait.continue.\textsc{Client}$$

$$\textsc{Server} \: \stackrel{{def}}{{=}}\: request.service.\overline{reply}.\textsc{Server}$$

$$\textsc{Client\_Server} \: \stackrel{{def}}{{=}}\: (\textsc{Client}\:\vert\:\textsc{Server} \: [call/request,reply/wait])$$

Qui il relabelling sul processo Server permette la sincronizzazione con il Client quando si incontrano le azioni call e reply come si vede dalle seguenti derivazioni:

• $\textsc{Server} \: [f] \: \stackrel{f(request)}{\longrightarrow} \: service.\overline{reply}. \textsc{Server} \:[f] \qquad$ con f(request) = call
• $\textsc{Client} \: \stackrel{\overline{call}}{\longrightarrow} \: wait.continue.\textsc{Client} \qquad$ perciò si ottiene la sincronizzazione
• $(\textsc{Client}\:\vert\:\textsc{Server} \: [f]) \: \stackrel{\tau}{\longrigh... .... \textsc{Client} \:\vert\: service.\overline{reply}.\textsc{Server} \: [f])$

Dopo la transizione $service$, in modo analogo al precedente si ha la comunicazione sulla porta $reply$ (per il relabelling eseguito su $wait$). Infine, con la derivazione di $continue$, si torna al sistema iniziale:

$$(wait.continue.\textsc{Client} \:\vert\: service.\overline{reply}.\textsc{Server} \: [f]) \stackrel{service}{\longrightarrow}$$

$$\stackrel{service}{\longrightarrow}(wait.continue.\textsc{Client}... ...t\: \overline{reply}.\textsc{Server} \: [f]) \stackrel{\tau}{\longrightarrow}$$

$$\stackrel{\tau}{\longrightarrow}(continue.\textsc{Client} \:\vert... ...{Server} \: [f]) \stackrel{continue}{\longrightarrow} \textsc{Client\_Server}$$

Esempio Bill-Ben 8: Se vogliamo rinominare le azioni di output in italiano basta semplicemente aggiungere il relabelling ai due processi:

$$\textsc{Bill}[gioca/play,incontro/meet] \qquad\qquad \textsc{Ben}[lavora/work, incontro/meet]$$