Value-Passing SPA

In this section we briefly present a value-passing extension of ``pure'' SPA (VSPA, for short). In all the examples reported in this paper will use such value passing calculus, because it leads to more readable specifications than those written in pure SPA.

As an example, consider the following buffer cell [Mil89]:

$$\begin{eqnarray*} C & \stackrel{\rm def}{=}& in(x).C'(x) \\ C'(x) & \stackrel{\rm def}{=}& \overline{out}(x).C \end{eqnarray*}$$

where x is a variable that can assume values in $\, {\rm N} \!\!\!\!\! {\rm I} \,\,\,$ (we usually write $x \in \, {\rm N} \!\!\!\!\! {\rm I} \,\,\,$). C reads a natural value n through action in and stores it in variable x . Then this value is passed to agent C' which can give n as output through action out moving again to C . So C represents a buffer which may hold a single data item.

Now we show how C can be translated into an SPA agent. The parametrized constant C' becomes a family of constants $C'_v$ one for each value $v \in \, {\rm N} \!\!\!\!\! {\rm I} \,\,\,$. Similarly $\overline{out}(x)$ becomes a family $\overline{out}_v$ of prefixes. So the single definition for C' becomes the following family of definitions:

$$\begin{eqnarray*} C'_v & \stackrel{\rm def}{=}& \overline{out}_v.C \ \ \ \ (v \in \, {\rm N} \!\!\!\!\! {\rm I} \,\,\,)\end{eqnarray*}$$

Now consider the prefix in(x) . To reflect the fact that it can accept any input value, binding variable x , we translate it into $\sum_{v\in \, {\rm N} \!\!\!\!\! {\rm I} \,\,\,}{in_v}$. So the definition becomes:

$$\begin{eqnarray*} C & \stackrel{\rm def}{=}& \sum_{v\in \, {\rm N} \!\!\!\!\! {\rm I} \,\,\,}{in_v}.C'_v\end{eqnarray*}$$

VSPA is very similar to the value-passing CCS introduced in [Mil89]. The main difference is that in VSPA we can have more than one parameter for actions and parameters are multi-sorted. The syntax of VSPA agents is defined as follows:

$$\begin{eqnarray*} E & ::= & \underline{0}\ \ \rule[-1ex]{0.25mm}{3ex}\ \ a(x_1, ... ... \mbox{\bf if } b\quad \mbox{\bf then } E\quad \mbox{\bf else } E\end{eqnarray*}$$

where the variables $x_1, \ldots, x_n$, the value expressions $e_1, \ldots, e_n$ and $e_1', \ldots, e_n'$ must be consistent with the arity of the action a and constant A , respectively (the arity specifies the sorts of the parameters), and b is a boolean expression.

It is also necessary to define constants as follows: $A(x_1,\ldots, x_m) \stackrel{\rm def}{=}E$ where E is a VSPA agent which may contain no free variables except $x_1, \ldots , x_m$, which must be distinct. As in [Mil89] the semantics of the value-passing calculus is given as a translation into the pure calculus. The translations rests upon the idea that a single label a of VSPA, with n parameters with sorts $S_1 \ldots S_n$, becomes the set of labels $\{ a_{v_1 \ldots v_n}: v_i \in S_i, \forall i \in [1,n]\}$ in SPA. We consider only agents without free variables because if an agent has a free variable then it becomes a family of agents, one for each value of the variable. The translation can be given inductively on the structure of agents (see [Mil89] for more details about this kind of translation).

Note that we do not partition the set of actions into two levels; we directly refer to the partition in the pure calculus. In this way it is possible for a certain action in VSPA to correspond, in the translation, to actions at different levels in SPA. This can be useful if we want a parameter representing the level of a certain action.