\documentclass[12pt]{article}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EDIT THESE TWO COMMANDS TO BE YOUR ANDREW ID AND NAME
\newcommand*{\stulogin}{}
\newcommand*{\stuname}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\usepackage{fancyheadings}
\usepackage{fancyhdr}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{fullpage-old}
\usepackage{graphics}
\usepackage{epsfig}
\usepackage{url}

\newcommand*{\assignmentnumb}{1}
%---------------------------------------------------------------------------

%\lhead[{\bfseries 15-414\quad HW \assignmentnumb\ \ \ \stulogin}]{{\bfseries 15-414\quad HW \assignmentnumb\ \ \ \stulogin}}
\lhead{}
\cfoot[]{Page \thepage{} of 2}
\pagestyle{fancy} \renewcommand{\headrulewidth}{0pt}
\fancypagestyle{plain}{ \renewcommand{\headrulewidth}{0pt} }
\parskip 1ex
\parindent 0mm

%-----------Formating Macros-------------

\newcommand{\problem}[1]{\section{#1}\vspace{-1em}}
\newcounter{partnumber}
\newenvironment{parts}{\begin{list}{
%     \arabic{problemnumber}\alph{partnumber}:}{
     (\alph{partnumber})}{
     \usecounter{partnumber} \setlength{\rightmargin}{\leftmargin}}
     \setlength{\itemsep}{.0 in}}{
     \end{list} \vspace*{.0 in}}
\newenvironment{solution}{\par{\bf Solution:}\ }{\hfill $\diamond$}

%-----------Useful Macros-------------

\newcommand*{\imp}{\rightarrow}
\newcommand*{\biimp}{\leftrightarrow}
\newcommand*{\true}{\mathsf{T}}
\newcommand*{\false}{\mathsf{F}}
\newcommand*{\nand}{\otimes}
\newcommand*{\code}[1]{\ensuremath{\text{\texttt{{#1}}}}}
\newcommand*{\union}{\cup}

\newcommand*{\DIMACS}{{\sc dimacs}}
\newcommand*{\watch}[1]{\fbox{${#1}$}}

\newcommand*{\E}{\mathbf{E}}
\newcommand*{\A}{\mathbf{A}}
\newcommand*{\G}{\mathbf{G\,}}
\newcommand*{\F}{\mathbf{F\,}}
\newcommand*{\U}{\,\mathbf{U}\,}

%---------------------------------------
\begin{document}

%\centerline{Instructor: Edmund M. Clarke \hfill Teaching Assistant: Michael Carl Tschantz}
\vspace{0.5ex}
\centerline{\Large\bf 15-817: Assignment \assignmentnumb}
%\vspace{0.5ex}
\centerline{\Large\bf \stuname}

%---------------------------------------------------------------------------
\textbf{\textit{\Large Please do Parts 1 and 2 ASAP!}}

\vspace{2ex}
\textbf{Part 1.} Sign up for the course mailing list.  Email the TA 
({\tt wkl\makebox[0em][l]{\i}ieber\,@\,cs.cmu.edu})
with ``{\tt [15-817] Subscribe {\it YourEmailAddress}}'' as the subject line;
leave the body blank.  If there are corrections or clarifications to this
assignment, you will be notified by email and the updates will also be posted
on the course website.

\vspace{4ex}
\textbf{Part 2.} Run Cadence SMV on {\tt simple-01.smv} (the file is on the
Assignments page of the course website).  Please do this ASAP so that we can
help you if you encounter difficulties in getting SMV to work.  (You can
download Cadence SMV and run it on your computer, or you can run Cadence on the
Andrew Unix servers.  See the Assignments page for more info.)  (You don't need to turn
in any work for Part 2.)

\vspace{4ex}
\textbf{Part 3.} 
Express the following properties in ${\rm CTL}$:
\begin{enumerate}
\item[A.] ``It is invariantly true that: We will necessarily eventually receive a request.''
\item[B1.] ``It is invariantly true that: If we receive a request, then we will possibly eventually send an acknowledgement.''
\item[B2.] ``It is invariantly true that: If we receive a request, then we will necessarily eventually send an acknowledgement.''
\item[C.] ``It is invariantly true that: If we receive a request, then we will necessarily send an acknowledgement in at most two clock cycles (state transititions).''
\item[D.] ``Infinitely many requests will occur during the operation of the system.'' (This is not directly translatable into CTL, but you can write a CTL property that entails it.)
\item[E.] ``From any state it is possible to get to a {\it restart\/} state.''
\item[F.] ``From any state it is possible to get to a {\it restart\/} state in exactly two steps.''
\item[G.] ``After $p$ is true, $q$ is never true.''  (Interpret this as a property for the current state, not as a global invariant.)
\end{enumerate}
Use the following atomic propositions: \vspace{-1ex}
\begin{itemize}
\item {\tt req} : We receive a request, \vspace{-1ex}
\item {\tt ack} : We send an acknowledgement, \vspace{-1ex}
\item {\tt restart} : We are in a {\it restart\/} state, 
\end{itemize}

\newpage
\textbf{Part 4.} Consider the automaton given below:
\begin{center}
\ \psfig{file=fsm-bin.eps}
\end{center}
and the following CTL formulas:
\begin{enumerate}
\item $\E\G d$
\item $\E\F \;\E\G d$
\item $\E\F \;\A\G d$
\item $\A\G \;\E\F d$
\item $\A[b \U c]$
\item $\A[b \U d]$
\end{enumerate}

Encode the above automaton as an SMV model.  Use one variable to
represent the current state.  Have this variable range over the four possible
states ({\tt Sab}, {\tt Sb}, {\tt Sd}, {\tt Scd}). Define the individual propositional
variables ($a$, $b$, $c$, $d$) in terms of the one state variable.
Encode the CTL
formulas as specifications to be checked of the model.  (Please keep them
in order.)  

Name your file ``{\tt {\it
Username}-hw1-p4.smv}'' and submit it using a method to be explained on the
course website.  Also run SMV on your file and print out the results of whether
each property is true or false.  (Don't include the traces or stats, just the final
answers for each property.)

\def\andl{\wedge}
\def\orl{\vee}
\def\xorl{\oplus}
\def\notl{\neg}

\vspace{4ex}
\def\mi{\mathit}
\def\A{\mathbf{A}}
\def\E{\mathbf{E}}
\def\F{\mathbf{F}}
\def\G{\mathbf{G}}
\def\U{\mathbf{U}}
\def\W{\mathbf{W}}
\textbf{Part 5.} Show that\,\, 
${\bf A}[f\; {\bf U}\; g] \;\equiv\; \notl {\bf E}[\notl g\;\; {\bf U}\;\; \notl f \andl \notl g]
\; \andl \; \notl {\bf EG}\; \notl g$

At some points, you may need to justify something by 
giving an informal explanation in terms of the semantics of
$\textrm{CTL}^*$.  Try to be as clear and rigorous as possible.

Hints:\vspace{-1ex}
\begin{itemize}
\item It may be useful to rewrite \,$[f\; \U\; g]$\, as $[(f \;\W\; g) \;\andl\; \F\; g]$, where $\W$ is the \textit{weak until} operator.  ``$f \;\W\; g$'' has the same semantics as ``$f \;\U\; g$'' except that $g$ is not required to eventually be true.
%\item One way to prove \,$\mi{foo} \equiv \mi{bar}$\, is to prove 
%$\;\mi{foo} \!\implies\! \mi{bar}\;$ and 
% $\;\mi{bar} \!\implies\! \mi{foo}$.
\item\vspace{-1ex} ``$\notl g\;\; {\bf U}\;\; \notl f \andl \notl g$'' means that we eventually reach a point in time where $f$ and $g$ are both false, and that $g$ cannot be true before we reach such a point.
\item\vspace{-1ex}Try to establish that  $\;(f \;\W\; g) \equiv \notl (\notl g\;\; {\bf U}\;\; \notl f \andl \notl g)\;$ using an informal argument, being as clear and rigorous as possible. 
\end{itemize}


\end{document}