% -*- Mode:TeX -*-

%% The documentstyle options along with the pagestyle can be used to generate
%% a technical report, a draft copy, or a regular thesis.  You may need to
%% re-specify the pagestyle after you \include  cover.tex.  For more
%% information, see the first few lines of mitthesis.sty. 

\documentstyle[12pt,vi,fleqn,psbox,amstex,twoside]{mitthesis}
\pagestyle{plain}

%% This bit allows you to either specify only the files which you wish to
%% process, or `all' to process all files which you \include.
%% Krishna Sethuraman (1990).

%%% MY DEFINITIONS

%\numberwithin{equation}{chapter}

%\usepackage{theorem}

\newtheorem{theorem}{Theorem}[chapter]
%\newtheorem{theorem}{Theorem}

\newtheorem{lemma}[theorem]{Lemma}

\newcommand{\pf}{\par\noindent{\bf Proof:}~}

\newcounter{automatonCounter}
\newenvironment{automaton}[1]{\refstepcounter{automatonCounter}
\par\noindent{\bf Automaton \theautomatonCounter  (#1):}}{}

\newcounter{definitionCounter}
\newenvironment{definition}[1]{\refstepcounter{definitionCounter}
\par\noindent{\bf Definition \thedefinitionCounter  (#1):}}{}

%\newtheorem{corollary}[theorem]{Corollary}

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

\newenvironment{proof}{\pf}{\qed}

%\newtheorem{proposition}[theorem]{Proposition}  

%\newtheorem{remark}[theorem]{Remark}

%\newenvironment{example}

%{\refstepcounter{theorem}{\vspace{2ex}\par\noindent \bf

%Example~\thetheorem~}}{\vskip 1pt}



\newcommand{\nat}{{\sf N}}

\newcommand{\posnat}{{\sf N}^+}

\newcommand{\nnr}{{\sf R}^{\geq 0}}

\newcommand{\posr}{{\sf R}^+}

\newcommand{\negr}{{\sf R}^-}
\newcommand{\reals}{{\sf R}}

\newcommand{\atA}{{\em Init-Vehicles}}
\newcommand{\atAA}{{\em Vehicles}}
\newcommand{\atB}{$\mathit{Controller}_j$}
\newcommand{\atC}{$\mathit{Controller}_1$}
\newcommand{\atD}{$\mathit{Controller}_2$}
\newcommand{\atE}{{\em Controlled-Vehicles}}
\newcommand{\atF}{{\em Safe-Vehicles}}
\newcommand{\atG}{$C_2$}
\newcommand{\atH}{{\em Bad Controller}$_1$}
\newcommand{\atI}{{\em Bad Controller}$_2$}
\newcommand{\atJ}{{\em Necessary-C}$_2$}
\newcommand{\atK}{{\em D-Buffer}}
\newcommand{\atL}{$D_i$}
\newcommand{\atM}{$D_o$}
\newcommand{\atN}{$D_2$}
\newcommand{\atO}{{\em Delayed-Controller}$_2$}
\newcommand{\atP}{{\em Bad-Delayed-Controller}$_2$}
\newcommand{\atQ}{{\em U-Buffer}}
\newcommand{\atR}{$U_i$}
\newcommand{\atS}{$U_o$}
\newcommand{\atT}{$U_2$}
\newcommand{\atU}{{\em Uncertain-Controller}$_2$}
\newcommand{\atV}{{\em Necessary-D}$_2$}
\newcommand{\atW}{{\em Spec-D}$_2$}

\newcommand{\atsA}{{\em Init-Vehicles }}
\newcommand{\atsAA}{{\em Vehicles }}
\newcommand{\atsB}{$\mathit{Controller}_j$ }
\newcommand{\atsC}{$\mathit{Controller}_1$ }
\newcommand{\atsD}{$\mathit{Controller}_2$ }
\newcommand{\atsE}{{\em Controlled-Vehicles }}
\newcommand{\atsF}{{\em Safe-Vehicles }}
\newcommand{\atsG}{$C_2$ }
\newcommand{\atsH}{{\em Bad Controller}$_1$ }
\newcommand{\atsI}{{\em Bad Controller}$_2$ }
\newcommand{\atsJ}{{\em Necessary-C}$_2$ }
\newcommand{\atsK}{{\em D-Buffer }}
\newcommand{\atsL}{$D_i$ }
\newcommand{\atsM}{$D_o$ }
\newcommand{\atsN}{$D_2$ }
\newcommand{\atsO}{{\em Delayed-Controller}$_2$ }
\newcommand{\atsP}{{\em Bad-Delayed-Controller}$_2$ }
\newcommand{\atsQ}{{\em U-Buffer }}
\newcommand{\atsR}{$U_i$ }
\newcommand{\atsS}{$U_o$ }
\newcommand{\atsT}{$U_2$ }
\newcommand{\atsU}{{\em Uncertain-Controller}$_2$ }
\newcommand{\atsV}{{\em Necessary-D}$_2$ }
\newcommand{\atsW}{{\em Spec-D}$_2$ }

\newcommand{\aatA}{Init-Vehicles}
\newcommand{\aatAA}{Vehicles}
\newcommand{\aatB}{$\mathit{Controller}_j$}
\newcommand{\aatC}{$\mathit{Controller}_1$}
\newcommand{\aatD}{$\mathit{Controller}_2$}
\newcommand{\aatE}{Controlled-Vehicles}
\newcommand{\aatF}{Safe-Vehicles}
\newcommand{\aatG}{$C_2$}
\newcommand{\aatH}{Bad Controller$_1$}
\newcommand{\aatI}{Bad Controller$_2$}
\newcommand{\aatJ}{Necessary-C$_2$ }
\newcommand{\aatK}{D-Buffer}
\newcommand{\aatL}{$D_i$}
\newcommand{\aatM}{$D_o$}
\newcommand{\aatN}{$D_2$}
\newcommand{\aatO}{Delayed-Controller$_2$}
\newcommand{\aatP}{Bad-Delayed-Controller$_2$}
\newcommand{\aatQ}{U-Buffer}
\newcommand{\aatR}{$U_i$ }
\newcommand{\aatS}{$U_o$ }
\newcommand{\aatT}{$U_2$ }
\newcommand{\aatU}{Uncertain-Controller$_2$}
\newcommand{\aatV}{Necessary-D$_2$ }
\newcommand{\aatW}{Spec-D$_2$}

\newcommand{\sm}{$\mathit{safe}\text{-}\mathit{measure}$ }
\newcommand{\ssm}{\mathit{safe}\text{-}\mathit{measure}}
\newcommand{\smd}{$\mathit{safe}\text{-}\mathit{measure}_d$ }
\newcommand{\ssmd}{\mathit{safe}\text{-}\mathit{measure}_d}
\newcommand{\smu}{$\mathit{safe}\text{-}\mathit{measure}_u$ }
\newcommand{\ssmu}{\mathit{safe}\text{-}\mathit{measure}_u}


\newcommand{\prcef}[3]{\begin{tabbing}       

XX\=  XX\=XX\=XX\=XX\=  \kill

\protect #1\\

\>Precondition: \+ \+ \\ 

  #2  \-  \- \\ 

\>Effect: \+  \+ \\

  #3 \- \- 

\end{tabbing}} 



\newcommand{\hioa}[8]{

\begin{tabular}{||l|l||} \hline

{\em Discrete Actions} & {\em Variables} \\ \hline

\begin{minipage}{3in}

        \ioi{#1}{#2}{#3}

\end{minipage} & 

\begin{minipage}{3in}

        \ioi{#4}{#5}{#6}

\end{minipage} \\ \hline

\multicolumn{2}{||c||}{{\em Trajectories}} \\ \hline

\multicolumn{2}{||c||}{For all nontrivial $I$-trajectories $w$, $\forall t \in I:$} \\

\multicolumn{2}{||l||}{#7} \\ \hline

\multicolumn{2}{||c||}{{\em Notes}} \\ \hline

\multicolumn{2}{||l||}{#8} \\ \hline

\end{tabular}

}



%io environment

\newenvironment{myiotab}{

\footnotesize

\begin{tabbing}

\hspace*{.25in}\=\hspace*{.25in}\=\hspace*{.25in}\=

\hspace*{.25in}\=\hspace*{.25in}\=\hspace*{.25in}\=

\hspace*{.25in}\=\hspace*{.25in}\=\hspace*{.25in}\=

\hspace*{.25in}\=\hspace*{.25in}\=\hspace*{.25in}\=\kill

}{

\end{tabbing}

\vspace{-0.9cm}

\normalsize}

\def\ioisize{\footnotesize}


%%% END OF MY DEFINTIONS


\typein [\files]{Enter file names to process, (chap1,chap2 ...), or `all' to
process all files:}
\def\all{all}
\ifx\files\all \typeout{Including all files.} \else \typeout{Including only \files.} \includeonly{\files} \fi

\begin{document}

\include{cover}
\pagestyle{plain}
\include{contents}
\include{chapter1}
%\newpage \mbox{}
\include{chapter2}
\include{chapter3}
%\newpage \mbox{}
\include{chapter4}
%\newpage \mbox{}
\include{chapter5}
\include{chapter6}
\include{chapter8}
\appendix
%\include{appa}
%\include{appb}
\include{biblio}
\end{document}








