\def\ioisize{\footnotesize}

\newcommand{\remove}[1]{}

\newcommand{\iio}[3]{\bgroup\ioisize {\bf Signature} \begin{tabbing} 
XX\=XX\=    \kill           %%Signature:
{\bf Inputs:}\+ \\                 %%Input, Output, Internal
  #1 \-  \\ \ \newline
{\bf Internals:} \+ \\
  #2 \- \\ \ \newline
{\bf Outputs:} \+\\
  #3 \-
\end{tabbing} \egroup} 

\newcommand{\states}[1]{\bgroup\ioisize {\bf State} \begin{tabbing} 
#1
\end{tabbing} \egroup}

\newcommand{\ioti}[4]{\bgroup\ioisize \begin{tabbing}
XX\=XX\=    \kill           %%Signature:
Input:\+ \\ 		    %%Input, Output, Time-passing, Internal
  #1 \-  \\
Output: \+ \\
  #2 \- \\
Time-passing: \+ \\
  #3 \- \\
Internal: \+\\
  #4 \-
\end{tabbing} \egroup} 

\newcommand{\ei}[2]{\bgroup\ioisize \begin{tabbing}
XX\=XX\=    \kill           %%Signature:
External:\+ \\ 		    %%External, Internal
  #1 \-  \\
Internal: \+\\
  #2 \-
\end{tabbing} \egroup} 

\newcommand{\io}[2]{\bgroup\ioisize \begin{tabbing}
XX\=XX\=    \kill           %%Signature:
{\bf Signature}\\
{\bf Input}:\+ \\ 		    %%Input, Output
  #1 \-  \\
{\bf Output}: \+\\
  #2 \-
\end{tabbing} \egroup} 

\newcommand{\on}[1]{\bgroup\ioisize \begin{tabbing}
XX\=XX\=    \kill           %%Signature:
{\bf Signature}\\
{\bf Output}:\+ \\ 		    %%Output
  #1 \-  \\
\end{tabbing} \egroup} 



\def\iocodesize{\footnotesize}
 
\newcommand{\iocodeonecol}[1]{\begin{center}\iocodesize
\begin{minipage}[t]{.95\linewidth}
\hbox to\linewidth{}
#1
%\vspace{.15in}
\end{minipage}
\end{center}}

\newcommand{\iocode}[2]{\vspace{-15pt}\begin{center}\iocodesize
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#1
%\vspace{.15in}
\end{minipage}
\hspace{.05\linewidth} 
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#2
%\vspace{.15in}
\end{minipage}
\end{center}}

\newcommand{\ef}[2]{%\iocodesize 
\begin{tabbing}         %%Effect
XX\= XXX\=XX\=XX\=XX\=XX\=   \kill
\protect #1\\
\>Eff: \+ \+ \>
   #2  \- \-
\end{tabbing}}

\newcommand{\prcef}[3]{\begin{tabbing}        %%Precondition: 
							    %%& Effect:
XX\= XXX\=XX\=XX\=XX\=  \kill
\protect #1\\
\>Pre: \+ \+ \>
  #2  \-  \- \\ 
\>Eff: \+  \+ \>
  #3 \- \- 
\end{tabbing}} 


%% Environment (statedef) for defining the state of an I/O-automaton
\newlength\Mwidth
\newlength\jsawidth

% Parameter: something that is printed below the definition
\def\statedef#1{\def\auxstatedef{#1}%
\def\auxempty{}%
\settowidth{\Mwidth}{M}
\jsawidth=\textwidth
\advance\jsawidth by -7cm
\advance\jsawidth by -\Mwidth
\advance\jsawidth by -10\tabcolsep
\advance\jsawidth by -6\arrayrulewidth
\begin{trivlist}\item[]%
\begin{tabular}{|p{2.5cm}|c|p{2.2cm}|p{2.3cm}|p{\jsawidth}|}
\hline
{\bf Variable} & \phantom{M} & {\bf Type} & {\bf Initially} & {\bf Description}\\
\hline\hline}
\def\endstatedef{\\ 
\ifx\auxstatedef\auxempty
  \hline
\else%
  \hline\hline
   \multicolumn{5}{|l|}{\auxstatedef}\\\hline
 \fi
\end{tabular}%
\end{trivlist}}

\def\statetext{\begin{minipage}[t]{\linewidth}}
\def\endstatetext{\end{minipage}\vspace{2pt}}





