% I/O Automaton for IS Object

\begin{figure}
\begin{boxedminipage}{\textwidth}
$IS_D^{n+1}$ {\it object named} $IS_x$ \\ \ \newline
\iocodesize
% SIGNATURE
\iio{
XXXXXXXXXXXX\= \kill
\inv ,                 \> $v \in D$, $i \in \{0, \ldots, n\}$.
}
{
XXXXXXXXXXXX\= \kill
\update,              \> $\cU \subseteq \{0, \ldots, n\}$.
}
{
XXXXXXXXXXXX\= \kill
\ret ,                 \> $S \in \vartheta(D)$, $i \in \{0, \ldots, n\}$.
}
\states{
% STATE
XXXXXXXXXXXXXX\= \kill
\memory     \> $\in \vartheta(D)$, initially $(\bot, \ldots, \bot)$.\\
\ivalue     \> $\in \vartheta(D)$, initially $(\bot, \ldots, \bot)$.\\
\rvalue     \> $\in \vartheta^2(D)$, initially $(\bot, \ldots, \bot)$.\\
\interface  \> $\in \{inv,ret,\bot\}^{n+1}$, $(\bot, \ldots, \bot)$\\

}
% TRANSITIONS
{\bf Transitions}
\iocode{
\ef{{\bf input:} \inv }
{
\ivaluei\   := $v$\\
\interfacei\ := $inv$
}
%========================================
\prcef{{\bf internal:} \update}
{
${\cal U} \subseteq \{i \mid {\mathit interface[i]} = {\mathit inv}\}$
}
{
For all \= $i$ \= in ${\cal U}$ do\\
        \>  \memoryi\      := $v$\\
For all \= $i$ \= in ${\cal U}$ do\\
        \>  \rvaluei\    := $memory$\\
For all \= $i$ \= in ${\cal U}$ do\\
        \>  \interfacei\ := $ret$
}
}
{\prcef{{\bf output:} \ret }
{
\interfacei\ = $ret$\\
\rvaluei\   = $S$}
{
\interfacei\ := $\bot$\\
%\memoryi\    := $\bot$
}
}
\end{boxedminipage}
\caption{I/O Automaton for an $IS_D^{n+1}$ object with name $IS_x$.}
\label{ISspec}
\end{figure}

