%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% a minipage extending to end of line...
\newlength{\widthoflinefill}
\newcommand{\linefill}{\settowidth{\widthoflinefill}{\hbox to\linewidth{}}}
%\newcommand{\linefill}{\settowidth{\widthoflinefill}{\mbox{} \hfil \mbox{}}}

\newlength{\hswidthoflength}
\newcommand{\hswidthof}[1]{\settowidth{\hswidthoflength}{\mbox{#1}}\hspace*{\hswidthoflength}}

\newenvironment{fillminipage}%
{ %begin
  \linefill\noindent\begin{minipage}[t]{\widthoflinefill}%
  }
{ %end
  \end{minipage}%
}

\newcommand{\linewidthfill}{\makebox[\linewidth]{} \\[-2.5\baselineskip]}

\newlength{\textfragwidth}
\newcommand{\textfrag}[1]{%
  \settowidth{\textfragwidth}{#1}%
  #1%
  }

\newenvironment{indentpage}[1]%
  {\textfrag{#1}\begin{minipage}[t]{\linewidth-\textfragwidth}}
  {\end{minipage}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% a gray box
\newcommand{\graybox}[2][0.9]{\ignorespaces%
  \colorbox[gray]{#1}{%
%    \makebox[\widthoflinefill-4\fboxsep-2\fboxrule][l]{\strut\ignorespaces #2}}}
    \makebox[\widthoflinefill-2\fboxsep][l]{\strut\ignorespaces #2}}}

\newcommand{\headerbox}[1]{\ignorespaces%
%  \framebox[\widthoflinefill-2\fboxsep-2\fboxrule][l]{\strut\ignorespaces #1}}
  \framebox[\widthoflinefill][l]{\strut\ignorespaces #1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Shorthand
\newcommand{\tds}{Theory of Distributed Systems}
\newcommand{\TDS}{Theory of Distributed Systems}
\newcommand{\tdsg}{Theory of Distributed Systems Group}
\newcommand{\TDSG}{Theory of Distributed Systems Group}
\newcommand{\LCS}{Laboratory for Computer Science}
\newcommand{\lcs}{\LCS}
\newcommand{\EECS}{Electrical Engineering and Computer Science}
\newcommand{\MIT}{Massachusetts Institute of Technology}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Page format commands

\newcommand{\printlayout}{%
  \typeout{-----------------------------------------}%
  \typeout{LaTeX Page Layout Parameters}
  \typeout{\string\paperwidth\space\space\the\paperwidth}
  \typeout{\string\paperheight\space\the\paperheight}
  \typeout{\string\textwidth\space\space\the\textwidth}
  \typeout{\string\textheight\space\the\textheight}
  \typeout{\string\oddsidemargin\space\space\the\oddsidemargin}
  \typeout{\string\evensidemargin\space\the\evensidemargin}
  \typeout{\string\topmargin\space\space\the\topmargin}
  \typeout{\string\headheight\space\the\headheight}
  \typeout{\string\headsep\space\the\headsep}
  \typeout{\string\footskip\space\space\space\the\footskip}
  \typeout{\string\marginparwidth\space\the\marginparwidth}
  \typeout{\string\marginparsep\space\space\space\the\marginparsep}
  \typeout{\string\hoffset\space\the\hoffset}
  \typeout{\string\voffset\space\the\voffset}
  \typeout{(1in=72.27pt, 1cm=28.45pt)}
  \typeout{-----------------------------------------}%
}

\newlength{\footheight}
\newlength{\footsep}
\newlength{\bottommargin}

\newcommand{\setpagelayout}[2]{%
\normalsize
\raggedbottom 

\setlength{\parindent}{0in}                     % Paragraph Indentation
\setlength{\parskip}{0.3\baselineskip}          % Interparagraph Spacing

\hoffset        = -1.0in
\voffset        = -1.0in

\paperheight    = 11.0in
\paperwidth     =  8.5in

\topmargin      = #1
%\bottommargin   = 2\topmargin
\bottommargin   = \topmargin
\headheight     = \baselineskip
\headsep        = 2\parskip
\footsep        = \headsep
\footheight     = \baselineskip
\footskip       = \footheight
\addtolength{\footskip}{\footsep}

\textheight     = \paperheight
\addtolength{\textheight}{-\topmargin}
\addtolength{\textheight}{-\headheight}
\addtolength{\textheight}{-\headsep}
\addtolength{\textheight}{-\footskip}
\addtolength{\textheight}{-\bottommargin}

\textwidth      = \paperwidth
\oddsidemargin  = #2
\evensidemargin = \oddsidemargin
\addtolength{\textwidth}{-\oddsidemargin}
\addtolength{\textwidth}{-\evensidemargin}

\linewidth      = \textwidth

\printlayout
}

\makeatletter
\newcommand{\printfont}{%
  \typeout{}
  \typeout{Encoding     = \f@encoding}
  \typeout{Family       = \f@family}
  \typeout{Series       = \f@series}
  \typeout{Shape        = \f@shape}
  \typeout{Size         = \f@size}
  \typeout{Baselineskip = \f@baselineskip}
  \typeout{TF-size      = \tf@size}
  \typeout{SF-size      = \sf@size}
  \typeout{SSF-size     = \ssf@size}
  \typeout{}}
\makeatother

% Redefining the pagestyle 'myheadings'
\makeatletter%
\def\ps@myheadings{\let\@mkboth\markboth%
    \def\@oddfoot{\hfil \thepage \hfil}%
    \def\@evenfoot{\hfil \thepage \hfil}%
    \def\@evenhead{\usebox{\draft} \hfil}%
    \def\@oddhead{\hfil \usebox{\draft}}%
}%                                              
\makeatother%

% Redefining the footnote typesetting command
\makeatletter%
\renewcommand{\@makefntext}[1]{%
  \begin{list}{}{%
%      \settowidth{\labelwidth}{\@makefnmark}%
      \setlength{\labelwidth}{1.5em}%
      \setlength{\leftmargin}{\labelwidth}%
      \setlength{\labelsep}{3pt}%
      \setlength{\itemindent}{0pt}%
      \setlength{\itemsep}{0pt}%
      \setlength{\rightmargin}{0pt}%
      \footnotesize}%
    \item[\@makefnmark]#1%
  \end{list}}
\makeatother%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% packages

%\usepackage{theorem}
%\usepackage{fancyheadings}
%\usepackage[verbose]{geometry}
%\usepackage{multicol}
%\usepackage{doublespace}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{cite}                               % Citations
\usepackage{citesort}                           % Sorting citations
\usepackage{fancybox}                           % Fancy Boxes...
\usepackage{pifont}                             % Dingbats
\usepackage{colordvi}
\usepackage[dvips]{graphics,color}
\usepackage{rotating}
\usepackage{tabularx}                           % Wide tabular 
\usepackage{xspace}                             % Spacing
\usepackage{verbatim}
\usepackage{epic}
\usepackage{eepic}
\usepackage{calc}                               % Calculating
\usepackage{ifthen}                             % Calculating
\usepackage[dvips]{changebar}                   % Change Bars...
\usepackage{float}                              % Special Floats

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% float style
\floatstyle{ruled}
\restylefloat{figure}
\restylefloat{table}

\newlength{\figxdim}

% Multicolumn environment and settings

% use the multicolumn environment
\usepackage{multicol}
% \columnsep = 0pt

% removing the extra vertical spacing before/after multicol environments
\multicolsep = 0pt

% \typeout{-----------------------------------------}%
% \typeout{multicols parameters}
% \typeout{\string\premulticols\space\space\the\premulticols}
% \typeout{\string\postmulticols\space\the\postmulticols}
% \typeout{\string\multicolsep\space\space\the\multicolsep}
% \typeout{\string\columnsep\space\the\columnsep}
% \typeout{\string\columnseprule\space\space\the\columnseprule}
% \typeout{-----------------------------------------}%

% Nomenclature environment and settings

\usepackage[norefeq,norefpage]{nomencl} % Nomenclature
\renewcommand{\nomprefix}{r}
\renewcommand{\nomname}{\chapter*{Nomenclature}}
\newlength{\nomindent}
\setlength{\nomindent}{3ex}

\renewcommand{\nomgroup}[1]{
  \ifthenelse{\equal{#1}{A}}
  { \item[\hspace{-\nomindent}{\Large\textbf{Acronyms}}]}
  { \ifthenelse{\equal{#1}{G}}
    { \item[\hspace{-\nomindent}{\Large\textbf{Greek Letters}}]}
    { \ifthenelse{\equal{#1}{H}}
      { \item[\hspace{-\nomindent}{\Large\textbf{Hybrid I/O Automata Notation}}]}
      { \ifthenelse{\equal{#1}{L}}
        { \item[\hspace{-\nomindent}{\Large\textbf{Latin Abbreviations}}]}
        { \ifthenelse{\equal{#1}{M}}
          { \item[\hspace{-\nomindent}{\Large\textbf{Mathematical Notation}}]}
          { \ifthenelse{\equal{#1}{P}}
            { \item[\hspace{-\nomindent}{\Large\textbf{Physical Plant and Protector Notation}}]}
            { \ifthenelse{\equal{#1}{R}}
              { \item[\hspace{-\nomindent}{\Large\textbf{Roman Letters}}]}
              { \item[\hspace{-\nomindent}{\Large\textbf{Miscellaneous}}]}
            }
          } 
        }
      }
    }
  }
}

\newcommand{\entrylabel}[1]{\mbox{#1} \hfil}
\renewenvironment{theglossary}
{ \nomname
  \begin{list}{}{
      \renewcommand{\makelabel}{\entrylabel}
%      \setlength{\itemsep}{0ex}
      \setlength{\labelwidth}{12ex}
      \setlength{\leftmargin}{\labelwidth+\labelsep+\nomindent}
      \setlength{\rightmargin}{0ex}
      \setlength{\itemindent}{0ex}
      \setlength{\listparindent}{0ex}}}
{ \end{list}}
 
% Various environments (numbered separately)

\ifx\resetcounterwithin\undefined
\newtheorem{example}{Example}
\newtheorem{constraint}{Constraint}
\newtheorem{assumption}{Assumption}
\newtheorem{invariant}{Invariant}
\newtheorem{definition}{Definition}
\newtheorem{property}{Property}
\newtheorem{algorithm}{Algorithm}
\newtheorem{fact}{Fact}
\newtheorem{axiom}{Axiom}
\newtheorem{conaxiom}{Constraint Axiom}
\newtheorem{proposition}{Proposition}
\else
\newtheorem{example}{Example}[\resetcounterwithin]
\newtheorem{constraint}{Constraint}[\resetcounterwithin]
\newtheorem{assumption}{Assumption}[\resetcounterwithin]
\newtheorem{invariant}{Invariant}[\resetcounterwithin]
\newtheorem{definition}{Definition}[\resetcounterwithin]
\newtheorem{property}{Property}[\resetcounterwithin]
\newtheorem{algorithm}{Algorithm}[\resetcounterwithin]
\newtheorem{fact}{Fact}[\resetcounterwithin]
\newtheorem{axiom}{Axiom}[\resetcounterwithin]
\newtheorem{conaxiom}{Constraint Axiom}[\resetcounterwithin]
\newtheorem{proposition}{Proposition}[\resetcounterwithin]
\fi

% Propositions, Claims, Lemmas, Corollaries, Theorems, and Conjectures
% are all numbered sequencially...

\newtheorem{claim}[proposition]{Claim}
\newtheorem{lemma}[proposition]{Lemma}
\newtheorem{corollary}[proposition]{Corollary}
\newtheorem{theorem}[proposition]{Theorem}
\newtheorem{conjecture}[proposition]{Conjecture}

\newenvironment{mylist}%
{\begin{list}{\ding{114}}{%
      \setlength{\topsep}{0pt}
      \setlength{\partopsep}{0pt}
      \setlength{\itemindent}{0in}%
      \setlength{\rightmargin}{0in}%
      \settowidth{\labelwidth}{\ding{114}}%
      \setlength{\leftmargin}{\labelwidth+\labelsep}}}%
{\end{list}}

\newenvironment{invlist}%
{\begin{list}{\ding{114}}{%
      \setlength{\itemsep}{0pt}%
      \setlength{\topsep}{0pt}%
      \setlength{\partopsep}{0pt}%
      \setlength{\itemindent}{0in}%
      \setlength{\rightmargin}{0in}%
      \settowidth{\labelwidth}{\ding{114}}%
      \setlength{\leftmargin}{\labelwidth+\labelsep}}}%
{\end{list}}

%% trying something out... 

\newlength{\stretchlength}
\newcommand{\setstretchlength}{\settowidth{\stretchlength}{\hbox to\linewidth{}}}

% New Column types
%%%%%%%%%%%%%%%%%%

\newcolumntype{C}{>{$}c<{$}}
\newcolumntype{L}{>{$}l<{$}}
\newcolumntype{R}{>{$}r<{$}}

% Boolean true and false
%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\true}{{\sf T}}
%\newcommand{\false}{{\sf F}}
\newcommand{\true}{\textnormal{\texttt{true}}\xspace }
\newcommand{\false}{\textnormal{\texttt{false}}\xspace }
\newcommand{\True}{\textnormal{\texttt{True}}\xspace }
\newcommand{\False}{\textnormal{\texttt{False}}\xspace }
\newcommand{\Bool}{\textnormal{\texttt{Bool}}\xspace }
\newcommand{\bool}{\textnormal{\texttt{Bool}}\xspace }

% Citations
%%%%%%%%%%%

\renewcommand{\cite}[1]{[\citen{#1}]}
\newcommand{\refcite}[1]{Ref.~\citen{#1}}
\newcommand{\refcites}[2]{Refs.~\citen{#1} and~\citen{#2}}
\newcommand{\refcitess}[3]{Refs.~\citen{#1},~\citen{#2}, and~\citen{#2}}

% References
%%%%%%%%%%%%

\newcommand{\refeqn}[1]{Equation~(\ref{#1})}
\newcommand{\refeqns}[2]{Equations~(\ref{#1}) and~(\ref{#2})}
\newcommand{\refeqnss}[3]{Equations~(\ref{#1}),~(\ref{#2}), and~(\ref{#3})}

\makeatletter
\newcount\listcount\newcount\tmpcount
%Carl Livadas 2001/11/19
%generate a list of references
% o the first arg is the type of refs in singular,
% o the second arg is the type of refs in plural, and
% o the third arg is a comma separated list of labels.
\def\reflist#1#2#3{%
%  \colorbox[gray]{0.9}{%
    \listcount = 0%
    \tmpcount  = 0%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    % CL - 040326; this is the earlier version that i had and that
    % worked with earlier versions of latex
    % \xdef\no@sp@reflist{\expandafter\@ignsp#3 \! }%
    %
    % CL - 040326; redefined the spaceless reflist as suggested at
    % http://www.tug.org/tex-archive/macros/latex/contrib/cite/cite.sty
    % seems to work with the latext version of latex but break earlier
    % versions 
    \begingroup\let\protect\string% normalize active chars
    \xdef\no@sp@reflist{\expandafter\@ignsp#3 \: }\endgroup% and remove ALL spaces
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \@for \reflistitem:=\no@sp@reflist\do {\advance\listcount by 1}%
    \ifx#1\empty\else\ifnum\listcount>1 #2~\else #1~\fi\fi%
    \@for \reflistitem:=\no@sp@reflist\do {%
      \advance\tmpcount by 1\relax%
      \ifnum\tmpcount<\listcount%
      {\ref{\reflistitem}\ifnum\listcount>2{,}\fi{ }}%
      \else%
      {\ifnum\listcount>1{and~}\fi\ref{\reflistitem}}%
      \fi%
    }%
%  }% this corresponds to the gray box
}
%%%%%
% remove spaces from the argument; taken from cite.sty
%
% CL - 040326; earlier version for earlier latex versions
%\def\@ignsp#1 {\ifx\!#1\@empty\else #1\expandafter\@ignsp\fi}
% CL - 040326
% for ignoring *ALL* spaces in the input.  This presumes there are no
% \outer tokens and no \if-\fi constructs in the parameter.  Spaces inside
% braces are retained.
\def\@ignsp#1 {\ifx\:#1\@empty\else #1\expandafter\@ignsp\fi}
\makeatother

%\newcommand{\reflist}[2][]{\texreflist{#1}{#2}}

\newcommand{\reffig}[1]{\reflist{Figure}{Figures}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\reffigs}[2]{Figures~\ref{#1} and~\ref{#2}}
\newcommand{\reffigss}[3]{Figures~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\reftbl}[1]{\reflist{Table}{Tables}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\reftbls}[2]{Tables~\ref{#1} and~\ref{#2}}
\newcommand{\reftblss}[3]{Tables~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refsec}[1]{\reflist{Section}{Sections}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refsecs}[2]{Sections~\ref{#1} and~\ref{#2}}
\newcommand{\refsecss}[3]{Sections~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refch}[1]{\reflist{Chapter}{Chapters}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refchs}[2]{Chapters~\ref{#1} and~\ref{#2}}
\newcommand{\refchss}[3]{Chapters~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refinv}[1]{\reflist{Invariant}{Invariants}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refinvs}[2]{Invariants~\ref{#1} and~\ref{#2}}
\newcommand{\refinvss}[3]{Invariants~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refthm}[1]{\reflist{Theorem}{Theorems}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refthms}[2]{Theorem~\ref{#1} and~\ref{#2}}
\newcommand{\refthmss}[3]{Theorem~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refpro}[1]{\reflist{Proposition}{Propositions}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refpros}[2]{Propositions~\ref{#1} and~\ref{#2}}
\newcommand{\refpross}[3]{Propositions~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\reflem}[1]{\reflist{Lemma}{Lemmas}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\reflems}[2]{Lemmas~\ref{#1} and~\ref{#2}}
\newcommand{\reflemss}[3]{Lemmas~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refdef}[1]{\reflist{Definition}{Definitions}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refdefs}[2]{Definitions~\ref{#1} and~\ref{#2}}
\newcommand{\refdefss}[3]{Definitions~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refaxm}[1]{\reflist{Axiom}{Axioms}{#1}}
% I am keeping these so as to be backward compatible...
\newcommand{\refaxms}[2]{Axioms~\ref{#1} and~\ref{#2}}
\newcommand{\refaxmss}[3]{Axioms~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refass}[1]{\reflist{Assumption}{Assumptions}{#1}}
\newcommand{\refcon}[1]{\reflist{Constraint}{Constraints}{#1}}

\newcommand{\refcor}[1]{\reflist{Corollary}{Corollaries}{#1}}
\newcommand{\refcors}[2]{Corollaries~\ref{#1} and~\ref{#2}}
\newcommand{\refcorss}[3]{Corollaries~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refprop}[1]{\reflist{Property}{Properties}{#1}}
\newcommand{\refprops}[2]{Properties~\ref{#1} and~\ref{#2}}
\newcommand{\refpropss}[3]{Properties~\ref{#1},~\ref{#2}, and~\ref{#3}}

\newcommand{\refapp}[1]{\reflist{Appendix}{Appendixes}{#1}}
\newcommand{\refapps}[2]{Appendixes~\ref{#1} and~\ref{#2}}
\newcommand{\refappss}[3]{Appendixes~\ref{#1},~\ref{#2}, and~\ref{#3}}

% Lingo Shorthand
%%%%%%%%%%%%%%%%%

\newcommand{\apriori}{\textit{a~priori}\@\xspace}
\newcommand{\aposter}{\textit{a~posteriori}\@\xspace}
\newcommand{\etal}{\textit{et~al}.\@\xspace}
\newcommand{\ie}{\textit{i.e.}\xspace,\xspace}
\newcommand{\eg}{\textit{e.g.}\xspace,\xspace}
\newcommand{\etc}{\textit{etc}\@\xspace}
\newcommand{\comma}{\:\:,}
\newcommand{\period}{\:\:.}
\newcommand{\wrt}{with respect to}
\newcommand{\unit}[1]{\,\textit{#1}}
% Spacing
%%%%%%%%%

\newcommand{\qqquad}{\quad\quad\quad}
\newcommand{\qqqquad}{\quad\quad\quad\quad}

% Blank Page
%%%%%%%%%%%%

\newcommand{\clearemptydoublepage}{\newpage{\pagestyle{empty}\cleardoublepage}}
\newcommand{\cleardoublepageempty}{\newpage{\pagestyle{empty}\cleardoublepage}}

\newcommand{\blankpageempty}{%
\newpage    
\thispagestyle{empty}
\mbox{}    % skips a page for two-sided printing
}

\newcommand{\blankpage}{%
\newpage    
\mbox{}    % skips a page for two-sided printing
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% proof environment...

\newcommand{\qed}{\rule{3mm}{3mm}}
%\newcommand{\qed}{\mbox{}\hfill{\rule{3mm}{3mm}}\medskip}

\makeatletter
\@ifundefined{proof}{%
  % black font with black box qed
  \newenvironment{proof}%
  {\par\noindent\textnormal{\textbf{Proof:}}~}%
  {\nopagebreak[3]~\hrulefill{\qed}\medskip}%
  % gray font instead of black
  \renewenvironment{proof}%
  {\color{gray}\par\noindent\textnormal{\textbf{Proof:}}~}%
  {\nopagebreak[3]~\hfill{\qed}\medskip\color{black}}%
  % black font with shadowed qed
  \renewenvironment{proof}%
  {\par\noindent\textnormal{\textbf{Proof:}}~}%
  {\nopagebreak[3]~\hfill{\ding{114}}\medskip}%
}{}
\makeatother

% Math Notation
%%%%%%%%%%%%%%%

% SETS

\newcommand{\Reals}{\mathbb{R}}         % Real Numbers
\newcommand{\reals}{\mathbb{R}}         % Real Numbers
\newcommand{\Imags}{\mathbb{C}}         % Complex Numbers
\newcommand{\imags}{\mathbb{C}}         % Complex Numbers
\newcommand{\Nats}{\mathbb{N}}          % Natural Numbers
\newcommand{\Rats}{\mathbb{Q}}          % Rational Numbers

\newcommand{\setR}[1][]{\ensuremath{{\mathbb{R}}^{#1}} }   % Real Numbers
\newcommand{\nnr}{{\setR[\geq 0]}}                         % Non-negative Real Numbers
\newcommand{\nnR}{{\setR[\geq 0]}}                         % Non-negative Real Numbers
\newcommand{\nnri}{{\setR[\geq 0] \Union \infty}}          % Non-negative Real Numbers
\newcommand{\posr}{{\setR[+]}}                             % Positive Real Numbers
\newcommand{\posR}{{\setR[+]}}                             % Positive Real Numbers

\newcommand{\setI}[1][]{\ensuremath{{\mathbb{I}}^{#1}} }   % Imaginary Numbers
\newcommand{\setC}[1][]{\ensuremath{{\mathbb{C}}^{#1}} }   % Complex Numbers
\newcommand{\setN}[1][]{\ensuremath{{\mathbb{N}}^{#1}} }   % Natural Numbers
\newcommand{\posN}[1][]{{\setN[+]}}                        % Positive Natural Numbers
\newcommand{\nat}{{\sf N}}
\newcommand{\posnat}{{\sf N}^+}

\newcommand{\setQ}[1][]{\ensuremath{{\mathbb{Q}}^{#1}} }   % Rational Numbers
\newcommand{\setZ}[1][]{\ensuremath{{\mathbb{Z}}^{#1}} }   % Integer Numbers

\newcommand{\nnt}{T^{\geq 0}}           % Non-negative elements in time axis

% Math Notation...

\newcommand{\ubar}[1]{\underline{#1}}
\newcommand{\obar}[1]{\overline{#1}}
\newcommand{\set}[1]{\{ #1 \}}
\newcommand{\series}[3]{\{ #1 \}_{#2}^{#3}}
\newcommand{\abs}[1]{\left| #1 \right|}
\newcommand{\card}[1]{\left| #1\right|}
\newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\ceil}[1]{\left\lceil #1 \right\rceil}
\newcommand{\parens}[1]{\left( #1 \right)}
\newcommand{\bracks}[1]{\left[ #1 \right]}
\newcommand{\doublebracks}[1]{\left[\!\left[ #1 \right]\!\right]}
\newcommand{\braces}[1]{\left{ #1 \right}}
\newcommand{\ang}[1]{%
  \ifmmode{\left\langle{#1}\right\rangle}%
  \else{$\left\langle${#1}$\right\rangle$}%
  \fi%
}
\newcommand{\tpl}[1]{\ang{#1}}
\newcommand{\settpl}[1]{\set{\ang{#1}}}
        % the \if allows use outside mathmode,
        % but will swallow following space there!
\newcommand{\prob}[2][]{{\Pr}_{{#1}}\left[ #2 \right]}
\newcommand{\Var}{\mathop{\rm Var}\nolimits}
\newcommand{\expect}[1]{{\rm E}\left[ #1 \right]}
\newcommand{\expectsq}[1]{{\rm E}^2\left[ #1 \right]}
\newcommand{\variance}[1]{{\rm Var}\left[ #1 \right]}
\newcommand{\varsq}[1]{{\rm Var}^2\left[ #1 \right]}

\newcommand{\Choose}[2]{{{#1}\atopwithdelims(){#2}}}

\newcommand{\pardt}[3][]{\frac{\partial^{#1} {#2}}{\partial {#3}^{#1}}}

\newcommand{\dt}{\ms{dt}}

% Script math symbol name
%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ms}[1]{\textnormal{\emph{\/#1\/}\xspace }\xspace }
\newcommand{\msbf}[1]{\textnormal{\textbf{\emph{#1}}\xspace }\xspace }

%\newcommand{\ms}[1]{\ensuremath{\text{\normalfont{\textit{#1}}} }}
%\newcommand{\ms}[1]{\ifmmode%
%\mathord{\mathcode`-="702D\it #1\mathcode`\-="2200}\else%
%$\mathord{\mathcode`-="702D\it #1\mathcode`\-="2200}$\fi}

% Operations/Relations on Sets
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\sqlt}{\sqsubset}
\newcommand{\sqleq}{\sqsubseteq}
\newcommand{\setlt}{\subset}
\newcommand{\setleq}{\subseteq}

% LOGIC + MATH
\newcommand{\mathdef}[1]{\relax\ifmmode #1\else $#1$\fi}
\newcommand{\mathify}[1]{\ifmmode{#1}\else\mbox{$#1$}\fi}
\newcommand{\primevar}[1]{\stackrel{.}{#1}}

% SEQUENCES
\newcommand{\first}[1]{\ms{first}{(#1)}}
\newcommand{\tail}[1]{\ms{tail}{(#1)}}
\newcommand{\last}[1]{\ms{last}{(#1)}}

% SETS, RELATIONS AND FUNCTIONS
% \pow{X} : powerset of set X
% \nes{X} : set of nonempty subsets of set X
\newcommand{\pow}[1]{{\cal P}(#1)}
\newcommand{\nes}[1]{{\cal N}(#1)}
\newcommand{\inverse}[1]{#1^{-1}}
\newcommand{\range}[1]{\ms{range}{(#1)}}
\newcommand{\domain}[1]{\ms{dom}{(#1)}}
\newcommand{\restr}{\lceil}

\newcommand{\expec}{\ensuremath{\mathbb{E}}}    % Expected Value
\renewcommand{\And}{\wedge}
\newcommand{\Or}{\vee}
\newcommand{\AND}{\bigwedge}
\newcommand{\OR}{\bigvee}
\newcommand{\andrm}{\mbox{ and }}
\newcommand{\orrm}{\mbox{ or }}
\newcommand{\hand}{\wedge}
\newcommand{\hor}{\vee}

\newcommand{\Union}{\cup}
\newcommand{\union}{\cup}

\newcommand{\inter}{\cap}

\newcommand{\setor}{\cup}
\newcommand{\setand}{\cap}

\newcommand{\minus}{\backslash}
\newcommand{\cross}{\times}

\newcommand{\argmax}{\mathop{\textnormal{argmax}}}

\newcommand{\unionassign}{\,\union\negmedspace=}
\newcommand{\minusassign}{\,\backslash\negmedspace=}

\newcommand{\emptyqueue}{\emptyset}

% IMPLICATIONS
\renewcommand{\implies}{\mathopen{}\:\Rightarrow\:\mathclose{}}
\newcommand{\Implies}{\mathopen{}\:\Rightarrow\:\mathopen{}}
%\newcommand{\Implies}{\Longrightarrow}
\newcommand{\ImpliedBy}{\Longleftarrow}
\newcommand{\Iff}{\Longleftrightarrow}
\newcommand{\iffarrow}{\Leftrightarrow}
\newcommand{\iffequiv}{\Leftrightarrow}

\newcommand{\IMplies}{\mathrel{\longRightarrow}}

\newcommand{\impliesrm}{\mbox{ implies }}
%\newcommand{\Iff}{\mathify{\mathrel{\Leftrightarrow}}}

\newcommand{\Inf}{\sqcap}
\newcommand{\Sup}{\sqcup}
\newcommand{\Exists}{\:\exists\:}
\newcommand{\Forall}{\:\forall\:}
\newcommand{\In}{\:\in\:}
\newcommand{\NotIn}{\:\not \in\:}
\newcommand{\from}{:\in}
% \deq          == equals by definition
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\newcommand{\st}{\;|\;}

% Special Symbols
%%%%%%%%%%%%%%%%%

\newcommand{\trademark}{\ensuremath{^{\text{\tiny TM}}}\xspace} % Trade Mark
\newcommand{\atsymbol}{\symbol{64}}                             % at symbol
\newcommand{\onehalf}{\mbox{\small $\frac{1}{2}$}}              % 1/2

% Other symbols or macros from HB
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\onto}{\rightarrow}
%\newcommand{\implies}{\Rightarrow}
%\newcommand{\hlf}{\mbox{\tiny $\frac{1}{2}$}}

\newcommand{\hop}[1]{\;\mbox{\bf \tt #1}\;}
\newcommand{\twohigh}[2]{\left[ \begin{array}{c} #1 \\ #2 \end{array} \right]}
\newcommand{\functo}{\rightarrow}
\newcommand{\derives}{\longrightarrow}
\newcommand{\lra}[1]{\langle #1 \rangle}
\newcommand{\lratext}[1]{\lra{\mbox{#1}}}
\newcommand{\db}[1]{[\![ #1 ]\!]}
\newcommand{\mfunc}[2]{{\cal #1}\db{#2}}
\newcommand{\dl}{\sqsubseteq}
\newcommand{\BPsi}{\mathbf{\Psi}}

% Arrow definitions

% \arrow{a}     ==        a
%                        ---->
%
% \sarrow{a}{A} ==        a
%                        ---->
%                             A
\newcommand{\arrow}[1]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{\!\!\!#1}{\raisebox{0ex}[0.6ex][0ex]{$
                  \negthinspace-\!\!\!\rightarrow\:$}}$}}
%\newcommand{\sarrow}[2]{
%                  \raisebox{0ex}[2.1ex][0ex]{
%                  $\stackrel{\!\!\!#1\:}{\raisebox{0ex}[0.6ex][0ex]{$
%                  \negthinspace-\!\!\!\rightarrow_{#2}\;$}}$}}

\newcommand{\sarrow}[2]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1}{\raisebox{0ex}[0.6ex][0ex]
                  {$\negthinspace-\!\!\!\rightarrow$}   }_{_{#2}}\;$}}

% \darrow{a}    ==        a
%                        ====>
%
% \sdarrow{a}{A}==        a
%                        ====>
%                             A
\newcommand{\darrow}[1]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1 ~~}{\raisebox{0ex}[0.6ex][0ex]{$
                  \negthinspace=\!\!\!\Rightarrow\:$}}$}}
\newcommand{\sdarrow}[2]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1}{\raisebox{0ex}[0.6ex][0ex]
                  {$\negthinspace=\!\!\!\Rightarrow$}   }_{_{#2}}$}}

% Arrow definitions

% \arrow{a}     ==        a
%                        ---->
%
% \sarrow{a}{A} ==        a
%                        ---->
%                             A

\newcommand{\longarrow}[1]{\ensuremath{@>#1>>}}
\newcommand{\longsarrow}[2]{\ensuremath{@>#1>>_{_{#2}}}}

% \darrow{a}    ==        a
%                        ====>
%
% \sdarrow{a}{A}==        a
%                        ====>
%                             A
\newcommand{\newdarrow}[1]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1 ~~}{\raisebox{0ex}[0.6ex][0ex]{$
                  \negthinspace=\!\!\!\Rightarrow\:$}}$}}
\newcommand{\newsdarrow}[2]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1}{\raisebox{0ex}[0.6ex][0ex]
                  {$\negthinspace=\!\!\!\Rightarrow$}   }_{_{#2}}$}}

% These are macros to generate well alligned if-then-else 
% clauses.  

\newlength{\ifwidth}
\newlength{\thenwidth}
\newlength{\tablewidth}

%\newcommand{\myifthenelse}[3]{%
%\settowidth{\ifwidth}{if #1}%
%\settowidth{\thenwidth}{then}%
%\setlength{\tablewidth}{0.9\linewidth}%
%\begin{tabular*}{\tablewidth}[t]{@{}l@{\hspace{1ex}}l@{\hspace{1ex}}l@{}}
%if #1   & then &
%\begin{minipage}[t]{\tablewidth-\ifwidth-\thenwidth-2ex}#2\end{minipage} \\
%        & else & 
%\begin{minipage}[t]{\tablewidth-\ifwidth-\thenwidth-2ex}#3\end{minipage}
%\end{tabular*}}

\newcommand{\myifthenelse}[3]{%
\begin{tabular}[t]{@{}l@{\hspace{1ex}}l@{\hspace{1ex}}l@{}}
if #1   & then &
\begin{tabular}[t]{@{}l@{}}
#2
\end{tabular} \\
        & else & 
\begin{tabular}[t]{@{}l@{}}
#3
\end{tabular}
\end{tabular}}

%\newcommand{\myifthen}[2]{%
%\settowidth{\ifwidth}{if #1}\settowidth{\thenwidth}{then}%
%\setlength{\tablewidth}{0.9\linewidth}%
%\begin{tabular*}{\tablewidth}[t]{@{}l@{\hspace{1ex}}l@{\hspace{1ex}}l@{}}
%if #1   & then & 
%\begin{minipage}[t]{\tablewidth-\ifwidth-\thenwidth-2ex}#2\end{minipage}
%\end{tabular*}}

\newcommand{\myifthen}[2]{%
\begin{tabular}[t]{@{}l@{\hspace{1ex}}l@{\hspace{1ex}}l@{}}
if #1   & then & 
\begin{tabular}[t]{@{}l@{}}
#2
\end{tabular}
\end{tabular}}

%\newcommand{\IfThenElse}[3]{%
%\settowidth{\ifwidth}{\quad}\settowidth{\thenwidth}{\quad}%
%\setlength{\tablewidth}{0.9\linewidth}%
%\begin{tabular*}{\tablewidth}[t]{@{\quad}l@{}}
%\multicolumn{1}{@{}l@{}}{if #1 then} \\
%  \begin{minipage}[t]{\tablewidth-\thenwidth}#2\end{minipage}\\
%\multicolumn{1}{@{}l@{}}{else} \\
%  \begin{minipage}[t]{\tablewidth-\thenwidth}#3\end{minipage}
%\end{tabular*}}

\newcommand{\IfThenElse}[3]{%
\begin{tabular}[t]{@{}l@{}}
\textbf{if} #1 \textbf{then} \\
\begin{tabular}[t]{@{\quad}l@{}}
#2
\end{tabular} \\
\textbf{else} \\
\begin{tabular}[t]{@{\quad}l@{}}
#3
\end{tabular} \\
\textbf{fi}
\end{tabular}}

%\newcommand{\IfThen}[2]{%
%\settowidth{\ifwidth}{\quad}\settowidth{\thenwidth}{\quad}%
%\setlength{\tablewidth}{0.9\linewidth}%
%\begin{tabular*}{\tablewidth}[t]{@{\quad}l@{}}
%\multicolumn{1}{@{}l@{}}{if #1 then} \\
%\begin{minipage}[t]{\tablewidth-\thenwidth}#2\end{minipage}
%\end{tabular*}}

\newcommand{\iocase}{\textbf{case}~}
\newcommand{\ioforeach}{\+\textbf{foreach}~}
\newcommand{\iodo}{\textbf{do:}~}
\newcommand{\ioitem}{\+}
\newcommand{\ioif}{\+\textbf{if}~}
\newcommand{\iothen}{\textbf{then}~}
\newcommand{\bfthen}{\textbf{then}~}
\newcommand{\ioelse}{\<\textbf{else}~}
\newcommand{\bfelse}{\textbf{else}~}
\newcommand{\ioelseif}{\<\textbf{elseif}~}
\newcommand{\ioend}{\-}
\newcommand{\iochoose}{\textbf{choose}~}
\newcommand{\iowhere}{\textbf{where}~}
\newcommand{\iolet}{\textbf{let}\:}
\newcommand{\iost}{\textbf{such that}\:}
\newcommand{\ioow}{\textbf{otherwise}\:}
\newcommand{\ioin}{\textbf{input}~}
\newcommand{\ioint}{\textbf{internal}~}
\newcommand{\ioout}{\textbf{output}~}
\newcommand{\iotime}{\textbf{time-passage}~}

\newcommand{\IfThen}[2]{%
\begin{tabular}[t]{@{}l@{}}
\textbf{if} #1 \textbf{then} \\
\begin{tabular}[t]{@{\quad}l@{}}
#2
\end{tabular} \\
\textbf{fi}
\end{tabular}}

\newcommand{\myIfThenElse}[3]{%
\settowidth{\ifwidth}{\quad}\settowidth{\thenwidth}{then}%
\setlength{\tablewidth}{0.9\linewidth}%
\begin{tabular*}{\tablewidth}[t]{@{}l@{\hspace{1ex}}l@{}}
\multicolumn{2}{@{}l@{}}{if #1} \\
then & \begin{minipage}[t]{\tablewidth-\thenwidth}#2\end{minipage}\\
else & \begin{minipage}[t]{\tablewidth-\thenwidth}#3\end{minipage}
\end{tabular*}}

\newcommand{\myIfThen}[2]{%
\settowidth{\ifwidth}{\quad}\settowidth{\thenwidth}{\quad}%
\setlength{\tablewidth}{0.9\linewidth}%
\begin{tabular*}{\tablewidth}[t]{@{\quad}l@{}}
\multicolumn{1}{@{}l@{}}{if #1 then} \\
\begin{minipage}[t]{\tablewidth-\thenwidth}#2\end{minipage}
\end{tabular*}}

% Macro for correct placement of margin labels...

\newcommand{\marginlabel}[1]{\mbox{}\marginpar{\raggedleft\hspace{0pt}#1}}

% Macro for writting an end-of-line comment...

%\newcommand{\comm}[1]{{\bfseries\texttt{$\backslash *$ #1 $*\backslash$}}}
\newcommand{\comm}[1]{{\textbf{\texttt{$\backslash\!\backslash$ #1}}}}
\newcommand{\carl}[1]{\notemacro{Carl}{#1}}
\newcommand{\nancy}[1]{\notemacro{Nancy}{#1}}
\newcommand{\notemacro}[2]{%
\begin{bfseries}%
**~#1: #2~**
\end{bfseries}}

% Macro for placement of notes in the text...

\newlength{\commentwidth}
\newlength{\notewidth}
\newcommand{\Note}[2][]{%
\def\choosearg{#1}%
\ifx\choosearg\empty%
  \def\choosearg{Note}%
\fi
\setlength{\notewidth}{\linewidth-2\fboxsep-2\fboxrule}
\settowidth{\commentwidth}{{%
%\ding{46}~%
\textsc{\choosearg}: }}
\par\vspace{1ex}
\noindent\fbox{\begin{minipage}[t]{\notewidth}
{%
%\ding{46}~%
\textsc{\choosearg}: }
\begin{minipage}[t]{\linewidth-\commentwidth-2\fboxsep}#2\end{minipage}
\end{minipage}}\par\vspace{1ex}}

\newcommand{\note}[1]{\Note{#1}}

% This generates a note in the margin

\newcommand{\marginnote}[1]{\marginpar{\footnotesize{%
%\ding{46}~%
#1}}}

% This generates a visible ``Needs Doing!!!'' that stretches throughout
% the line at hand.

\newcommand{\todo}[1][To be done!!!]{\shadowbox{\textsc{#1}}}

% Generates a framed minipage with its width as an optional argument.
% If the width is not specified, \linewidth is used.

\newsavebox{\fminibox}
\newlength{\fminilength}
\newenvironment{fminipage}[1][\linewidth]%
{\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule}%
\begin{lrbox}{\fminibox}\begin{minipage}{\fminilength}}%
{\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}}

% Draw an rule of width equal \linewidth and height equal to the first
% argument: 

\newcommand{\ruleofheight}[1]{\noindent\rule{\linewidth}{#1}}

% Removing portion of text from the output but not the tex file:

\newcommand{\remove}[1]{}

% Widths of left and right columns

\newlength{\leftcolumnwidth}
\newlength{\rightcolumnwidth}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Print out the time

\newcounter{hrs}\newcounter{mins}\newcounter{hrsampm}
\newcommand{\printtime}{%
  \setcounter{hrs}{\time/60}%
  \setcounter{mins}{\time-\value{hrs}*60}%
  \ifthenelse{\value{hrs}<10}{0}{}{\thehrs}%
        :\ifthenelse{\value{mins}<10}{0}{}{\themins}}
\newcommand{\printtimeampm}{%
  \setcounter{hrs}{\time/60}%
  \setcounter{mins}{\time-\value{hrs}*60}%
  \ifthenelse{\value{hrs}>12}%
    {\setcounter{hrsampm}{\value{hrs}-12}}%
    {\setcounter{hrsampm}{\value{hrs}}}%
  {\thehrsampm}%
        :\ifthenelse{\value{mins}<10}{0}{}{\themins}%
        \ifthenelse{\value{hrs}>11}{pm}{am}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Box designating the draft time...
\newsavebox{\draft}
\sbox{\draft}{{\textsc{Draft~--~{\number\year/\number\month/\number\day}~--~\printtime}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\brule#1{\vrule width#1 height -1.1pt depth 1.5pt\relax}

% leave white space that is as wide as the argument

\newlength{\whitespacewidth}
\newcommand{\whitespace}[1]{%
\settowidth{\whitespacewidth}{#1}%
\hspace{\whitespacewidth}}

% Some Macros Used for HIOA

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

\newenvironment{tabenv}{%
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill}%
{%
\end{tabbing}}

\newcommand{\ioi}[3]{\bgroup\ioisize \begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
Input:\+ \\        
  #1 \-  \\
Output:\+ \\
  #2 \- \\
Internal:\+ \\
  #3 \-
\end{tabbing} \egroup} 

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

\newcommand{\io}[2]{\footnotesize \begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
Input:\+ \\                              
  #1 \-  \\
Output: \+ \\
  #2 \- 
\end{tabbing} \normalsize } 

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

\newcommand{\ioidouble}[3]{\footnotesize
\begin{minipage}[t]{3in}
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
Input:\+ \\        
  #1 \-  \\
Output:\+ \\
  #2 \- \\
\end{tabbing}
\end{minipage}
\hspace{.25in}
\begin{minipage}[t]{3in}
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
Internal:\+ \\
  #3 \-
\end{tabbing}
\end{minipage}}

\newcommand{\iocodeonecol}[1]{\vspace{-20pt}\begin{center}\iocodesize
\begin{minipage}[t]{.95\linewidth}
\hbox to\linewidth{}
#1
\end{minipage}
\end{center}}

\newcommand{\iocode}[2]{\begin{center}\footnotesize
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#1
\end{minipage}
\hspace{.05\linewidth} 
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#2
\end{minipage}
\end{center}}

\newcommand{\ef}[2]{%
\begin{fillminipage}
\begin{tabbing}       
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
\protect #1\\
Eff:\+\+ \>\> #2 \-\-
\end{tabbing}
\end{fillminipage}
}

\newcommand{\prcef}[3]{%
\begin{fillminipage}
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
\protect #1 \\
Pre: \+\+ \>\> #2 \-\- \\ 
Eff: \+\+ \>\> #3 \-\-
\end{tabbing}
\end{fillminipage}
}

% Simulation

\newcommand{\simitem}{\item[$\square$]}

% Variables

\newcommand{\type}[1]{\ms{type}{(#1)}}

% (UNTIMED) AUTOMATA
\newcommand{\states}[1]{\ms{states}{(#1)}}
\newcommand{\start}[1]{\ms{start}{(#1)}}
\newcommand{\acts}[1]{\ms{acts}{(#1)}}
\newcommand{\outacts}[1]{\ms{out}{(#1)}}
\newcommand{\trans}[1]{\ms{trans}{(#1)}}
\newcommand{\steps}[1]{\ms{steps}{(#1)}}
\newcommand{\ext}[1]{\ms{ext}{(#1)}}
\newcommand{\proj}{\lceil} % projects a hybrid execution onto components
% \extproj projects a sequence of actions on the actions in \ext{A}
\newcommand{\extproj}[1]{\widehat{#1}}
\newcommand{\concat}{\mathbin{^{\frown}}} % concatenation of executions and
                                                %trajectories

% The sets of finite, infinite, resp. all executions of A:
\newcommand{\ffrag}[1]{\ms{frag}^{\ast}(#1)}
\newcommand{\ifrag}[1]{\ms{frag}^{\omega}(#1)}
\newcommand{\frag}[1]{\ms{frag}(#1)}
\newcommand{\fexecs}[1]{\ms{execs}^{\ast}(#1)}
\newcommand{\iexecs}[1]{\ms{execs}^{\omega}(#1)}
\newcommand{\execs}[1]{\ms{execs}(#1)}

\newcommand{\aexecs}[1]{\ms{aexecs}(#1)}
\newcommand{\dexecs}[1]{\ms{dexecs}(#1)}
\newcommand{\adexecs}[1]{\ms{adexecs}(#1)}

\newcommand{\fexec}[1]{\ms{execs}^{\ast}(#1)}
\newcommand{\iexec}[1]{\ms{execs}^{\omega}(#1)}
\newcommand{\exec}[1]{\ms{execs}(#1)}
\newcommand{\ffragm}[1]{\ms{frag}^{\ast}(#1)}
\newcommand{\ifragm}[1]{\ms{frag}^{\omega}(#1)}
\newcommand{\fragm}[1]{\ms{frag}(#1)}

\newcommand{\trace}[1]{\ms{trace}{(#1)}}

% The sets of finite, infinite, resp. all traces of A:
\newcommand{\ftraces}[1]{\ms{traces}^{\ast}(#1)}
\newcommand{\itraces}[1]{\ms{traces}^{\omega}(#1)}
\newcommand{\traces}[1]{\ms{traces}(#1)}

% (TRACE) PREORDERS
\newcommand{\pre}[1]{\leq_{{\rm #1}}}
\newcommand{\erp}[1]{\geq_{{\rm #1}}}
\newcommand{\kernel}[1]{\equiv_{{\rm #1}}}
\newcommand{\preft}{\pre{\ast T}}
\newcommand{\preit}{\pre{\omega T}}
\newcommand{\pret}{\pre{T}}
\newcommand{\kernelft}{\kernel{\ast T}}
\newcommand{\kernelit}{\kernel{\omega T}}
\newcommand{\kernelt}{\kernel{T}}

\newcommand{\after}[1]{\ms{after}{(#1)}}
\newcommand{\past}[1]{\ms{past}{(#1)}}

% TRACE PROPERTIES
\newcommand{\beh}[1]{\ms{beh}{(#1)}}
\newcommand{\sort}[1]{\ms{sort}{(#1)}}
\newcommand{\cano}[1]{\ms{can}{(#1)}}

% MORE PREORDERS
\newcommand{\prer}{\pre{R}}
\newcommand{\pref}{\pre{F}}
\newcommand{\preb}{\pre{B}}
\newcommand{\preifb}{\pre{iB}}
\newcommand{\prefb}{\pre{FB}}
\newcommand{\preiffb}{\pre{iFB}}
\newcommand{\prebf}{\pre{BF}}
\newcommand{\preifbf}{\pre{iBF}}
\newcommand{\preh}{\pre{H}}
\newcommand{\prep}{\pre{P}}
\newcommand{\preifp}{\pre{iP}}
\newcommand{\prebp}{\pre{iP}}

% STILL MORE PREORDERS / REACHABILITY STUFF
\def\aproperty{$\Box$-property }
\def\aproperties{$\Box$-properties }
\def\aProperties{$\Box$-Properties }

% \newcommand{\restrict}[2]{#1 / #2}

\newcommand{\prewr}{\pre{wR}}
\newcommand{\prewf}{\pre{wF}}
\newcommand{\prewb}{\pre{wB}}
\newcommand{\prewifb}{\pre{wiB}}
\newcommand{\prewfb}{\pre{wFB}}
\newcommand{\prewiffb}{\pre{wiFB}}
\newcommand{\prewbf}{\pre{wBF}}
\newcommand{\prewifbf}{\pre{wiBF}}
\newcommand{\prewh}{\pre{wH}}
\newcommand{\prewp}{\pre{wP}}
\newcommand{\prewifp}{\pre{wiP}}
\newcommand{\prewbp}{\pre{wiP}}

% CONSTRUCTIONS ON AUTOMATA
\newcommand{\unfold}[1]{\ms{unfold}{(#1)}}
\newcommand{\guess}[1]{\ms{guess}{(#1)}}
\newcommand{\interp}[3]{\ms{int}{(#1,#2,#3)}}
\newcommand{\fbinterp}[3]{\ms{fb-int}{(#1,#2,#3)}}
\newcommand{\bfinterp}[3]{\ms{bf-int}{(#1,#2,#3)}}
\newcommand{\superp}[3]{\ms{sup}{(#1,#3,#2)}}

% INVARIANTS

\newcommand{\reach}[1]{R(#1)}
\newcommand{\reachstates}[1]{\ms{rstates}(#1)}

% TIMED AUTOMATA

\newcommand{\dacts}[1]{\ms{dacts}{(#1)}}
\newcommand{\dsteps}[1]{\ms{dsteps}{(#1)}}
\newcommand{\trajs}[1]{\ms{trajs}{(#1)}}

\def\Sone{{\bf S1}}
\def\Stwo{{\bf S2}}
\def\Sthree{{\bf S3}}
\def\Sfour{{\bf S4}}
\def\trajax{{\bf S5}}
\def\wangax{{\bf S5'}}
\newcommand{\timec}[1]{#1.\ms{now}}
\newcommand{\stimec}[2]{#1.\ms{now}_{#2}}
%\newcommand{\now}[1]{#1.\ms{now}}
\newcommand{\snow}[2]{#1.\ms{now}_{#2}}

\newcommand{\vis}[1]{\ms{vis}{(#1)}}

\newcommand{\ftimec}[1]{#1.\ms{ftime}}
\newcommand{\ltimec}[1]{#1.\ms{ltime}}
\newcommand{\ltime}[1]{#1.\ms{ltime}}
\newcommand{\fstatec}[1]{#1.\ms{fstate}}
\newcommand{\fstate}[1]{#1.\ms{fstate}}
\newcommand{\lstatec}[1]{#1.\ms{lstate}}
\newcommand{\lstate}[1]{#1.\ms{lstate}}
\newcommand{\seqc}[1]{#1.\ms{seq}}
\newcommand{\tsp}[1]{\ms{tsp}{(#1)}}
\newcommand{\append}{\cdot}

% TIMED EXECUTIONS
\newcommand{\tprefix}{\preceq}
\newcommand{\stricttprefix}{\prec}
\newcommand{\ftfrag}[1]{\ms{t-frag}^{\ast}(#1)}
\newcommand{\atfrag}[1]{\ms{t-frag}^{\infty}(#1)}
\newcommand{\tfrag}[1]{\ms{t-frag}(#1)}
\newcommand{\ftexecs}[1]{\ms{t-execs}^{\ast}(#1)}
\newcommand{\atexecs}[1]{\ms{t-execs}^{\infty}(#1)}
\newcommand{\texecs}[1]{\ms{t-execs}(#1)}

% TIMED TRACES
% The timed trace associated to an execution fragment
\newcommand{\ttrace}[1]{\ms{ttrace}{(#1)}}

% The sets of all, the finite and the infinite timed traces
% of a (semi) timed automaton, together with the induced preorders:
\newcommand{\fhtraces}[1]{\ms{h-traces}^{\ast}{(#1)}}
\newcommand{\ahtraces}[1]{\ms{h-traces}^{\infty}{(#1)}}
\newcommand{\tpre}[1]{\leq^{\rm t}_{{\rm #1}}}
\newcommand{\terp}[1]{\geq^{\rm t}_{{\rm #1}}}
\newcommand{\tkernel}[1]{\equiv^{\rm t}_{{\rm #1}}}
\newcommand{\tpret}{\tpre{T}}
\newcommand{\tpreft}{\tpre{\ast T}}
\newcommand{\tpreat}{\tpre{\infty T}}
\newcommand{\tkernelt}{\tkernel{T}}
\newcommand{\tkernelft}{\tkernel{\ast T}}
\newcommand{\tkernelat}{\tkernel{\infty T}}

\newcommand{\tmove}[1]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1}{\raisebox{0ex}[0.6ex][0ex]{$
                  \leadsto \,$}}$}}
\newcommand{\stmove}[2]{
                  \raisebox{0ex}[2.1ex][0ex]{
                  $\stackrel{#1}{\raisebox{0ex}[0.6ex][0ex]
                  {$\leadsto$}}_{#2}\,$}}

\newcommand{\tafter}[1]{\ms{t-after}{(#1)}}
\newcommand{\tpast}[1]{\ms{t-past}{(#1)}}

% HYBRID TRACES
% The hybrid trace associated to an execution fragment

\newcommand{\htrace}[2][]{\ms{h-trace}_{#1}{(#2)}}
\newcommand{\htraces}[2][]{\ms{h-traces}_{#1}{(#2)}}

% Algebra macros

\newenvironment{algebra}{\small \renewcommand{\arraystretch}{1.5}
\begin{tabular}{rcp{3.5in}|p{2in}}
}{\end{tabular}}

\newenvironment{algebra2}{\small \renewcommand{\arraystretch}{1.5}
\begin{tabular}{rcp{2.5in}|p{2in}}
}{\end{tabular}}

\newenvironment{algebra3}{\small \renewcommand{\arraystretch}{1.5}
\begin{tabular*}{\linewidth}{RCL!{\extracolsep{\fill}}p{2in}}
}{\end{tabular*}}

\newenvironment{mydisp}{
\begin{equation*}
\begin{split}
}{
\end{split}
\end{equation*}
}

% AUTOMATA

\newcommand{\hfrag}[1]{\ms{h-frag}(#1)}
\newcommand{\hfrags}[1]{\ms{h-frags}(#1)}
\newcommand{\VarHide}[2]{{\sf VarHide} ( #1 , #2 )}
\newcommand{\ActHide}[2]{{\sf ActHide} ( #1 , #2 )}

% HYBRID AUTOMATA

\newcommand{\Ftrajs}[1]{\ms{{\cal F}-trajs}{(#1)}}
\newcommand{\traj}{w}
\newcommand{\fctrajs}[1]{\ms{fctrajs}{(#1)}}
\newcommand{\ldacts}[1]{\ms{local-dacts}{(#1)}}

\newcommand{\Val}[1]{\boldsymbol{#1}}
\newcommand{\point}[1]{\wp(#1)}
\newcommand{\Pref}[1]{{\it Pref}(#1)}
\newcommand{\Max}[1]{{\it Max}(#1)}
\newcommand{\Closed}[1]{\ms{Closed}{(#1)}}
\newcommand{\Full}[1]{\ms{Full}{(#1)}}

\newcommand{\execbef}{\triangleleft} % execution before time t
\newcommand{\execafter}{\triangleright} % execution after time t

% TIMED EXECUTIONS
\newcommand{\fhexecs}[1]{\ms{h-execs}^{\ast}(#1)}
\newcommand{\ahexecs}[1]{\ms{h-execs}^{\infty}(#1)}
\newcommand{\hexecs}[1]{\ms{h-execs}(#1)}
\newcommand{\actfhexecs}[1]{\ms{act-h-execs}^{\ast}(#1)}

% PROCESSES
\newcommand{\Magic}{{\cal M}}
\newcommand{\Aut}[1]{\ms{Aut}{(#1)}}

% Some new length variables

\renewcommand{\topfraction}{1}
\renewcommand{\textfraction}{0}
\newcommand{\AutoSize}{\small}
\newcommand{\IOSize}{\small}

\ifx\iotabsize\undefined
\def\iotabsize{\normalsize}
\fi

\newenvironment{myiotab}{\iotabsize\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
}{\end{tabbing}\normalsize}

\newenvironment{iotab}[1][\iotabsize]%
{% \begin
\begin{fillminipage}#1%
\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill}
{% \end
 \end{tabbing}%
 \end{fillminipage}%
}

\newenvironment{myfundesc}{\IOSize\begin{description}}{\end{description}\normalsize}
\newenvironment{funcdesc}%
{% \begin
\par\vspace{1ex}\begin{fminipage}\begin{description}}
{% \end 
\end{description}\end{fminipage}\vspace{1ex}\par}

% Notational Macros

\newcommand{\var}[1]{\textnormal{\textit{#1}}\xspace}
\newcommand{\action}[1]{\textnormal{\texttt{#1}}\xspace}
\newcommand{\act}[1]{\textnormal{\texttt{#1}}\xspace}
\newcommand{\automat}[1]{\textnormal{\textsc{#1}}\xspace}
\newcommand{\aut}[1]{\textnormal{\textsc{#1}}\xspace}
\newcommand{\func}[1]{\textnormal{\texttt{#1}}\xspace}
\newcommand{\param}[1]{\textnormal{\texttt{#1}}}
\newcommand{\val}[1]{\textnormal{\texttt{#1}}}

% graphics and color packages...

%\definecolor{gray}{gray}{0.5}
\definecolor{lightgray}{cmyk}{0,0,0,0.1}
\definecolor{textgray}{cmyk}{0,0,0,0.6}
\definecolor{gray}{cmyk}{0,0,0,0.6}
\newcommand{\textgray}{\color{textgray}}

\newcommand{\grayregion}[1]{}
\newcommand{\grayiotab}[1]{}
\newcommand{\grayline}{}

\newcommand{\showgray}{%
  \renewcommand{\grayregion}[1]{\color{gray}\begin{minipage}[t]{\linewidth}##1\end{minipage}\color{black}}
  \renewcommand{\grayiotab}[1]{\color{gray}\begin{iotab}##1\end{iotab}\color{black}}
  \renewcommand{\grayline}{\color{gray}}}

\newcommand{\omitgray}{%
  \renewcommand{\grayregion}[1]{}
  \renewcommand{\grayline}{}}

\endinput

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paper"
%%% End: 
