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]:

where *x* is a variable that can assume values in
(we usually write ).
*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 one for each value . Similarly becomes a family
of prefixes. So the single definition for *C*' becomes the
following family of definitions:

Now consider the prefix *in*(*x*) . To reflect the fact that it can accept any
input value, binding variable *x* , we translate it into . So the definition becomes:

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:

where the variables , the value expressions and 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:
where *E* is a VSPA agent which may
contain no free variables
except , 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
, becomes the set of labels 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.