% I/O Automaton for process i running $k$-shot IIS protocol

\begin{figure}
\begin{boxedminipage}{\textwidth}
{\it Process i} \\ \ \newline
\iocodesize
% SIGNATURE
\iio{
XXXXXXXXXXXX\= \kill
\ret    \> $S \in \bigcup_{l = 1}^k \vartheta^l(D)$.\\
\starti  \> $v \in D$.
}
{
}
{
XXXXXXXXXXXX\= \kill
\inv    \> $v \in \bigcup_{l = 0}^k \vartheta^l(D)$.\\
\finishi\> $S \in \bigcup_{l = 0}^k \vartheta^l(D)$.
}
\states{
% STATE
XXXXXXXXXXXXXX\= \kill
\ls         \> $\in (\bigcup_{l = 0}^k \vartheta^l(D)) \cup \{\bot\}$, initially in the fresh state $\bot$.\\  
%\counter    \> $\in \Bbb{Z}$, initially $1$.\\
%\status     \> $\in \{ready, waiting, decided\}$, initially $ready$.
}
% TRANSITIONS
{\bf Transitions}
\iocode{
%%%%%%%%%%%%%%%%%%%% ret_writeread
\ef{{\bf input:} \ret}
{
\ls\ := $S$\\
%\counter\ := \counter+1\\
}

%%%%%%%%%%%%%%%%%%%% inv_writeread
\prcef{{\bf output:} \inv}
{
$\tau$(\ls)\ = {\tt false} \\
\ls\ = $v \neq \bot$
}
{
}
}
%%%%%%%%%%%%%%%%%% starti
{\ef{{\bf input:} \starti}
{
\ls\ := $v$\\
}
%%%%%%%%%%%%%%%%%% finish
\prcef{{\bf output:} \finishi}
{
$\tau$(\ls)\ = {\tt true}\\
$\mu$(\ls)\ = $S$\\
}
{

} 
}
\end{boxedminipage}
\caption{I/O Automaton for process $i$ running NIIS protocol.}
\label{fig: NIISprotocol}
\end{figure}

