\problemdata                                                             
        {Leia and Han Solo} % latex-friendly label for the prob.
        {state machines, invariants, termination} % The topic(s) of the problem content.  
        {Fall 2000 Problem Set 5} % Source (if known)                                          
        {S01 Quiz 1, 7} % Usage (list ones you are aware of). 
        {Tina Wang, S02} % Last revision info (author, date).   
                                                                         
                                                                         
\begin{problem}           
A long time ago, in a 2-dimensional galaxy far, far away, everything
was laid out in a 1000 by 1000 meter square.  Han Solo lived at grid
point $(0,0)$ of the square, and Princess Leia lived at grid point
$(0,1000)$.  Of course, Han and Leia wanted to meet, at {\em
exactly\/} the same point in the square.  However, both were
restricted by their rather strange space ships to move according to
very particular rules: Han could only move $3$ units parallel to the
$x$ axis, or 3 units parallel to the $y$ axis, or $3$ units parallel
to the $x$ axis and 3 units parallel to the $y$ axis (all at once,
making a diagonal move).  Leia could only move $3$ units, and only
parallel to either the $x$ axis or $y$ axis.  They do not have to move
at the same time, nor alternating.

\begin{problemparts}
\problempart

Model Han and Leia and their possible moves as a (single) state
machine.  That is, define the states $Q$, the start state $Q_0$, and the
transitions $\delta$.

\solution{
\begin{description}
\item $Q = \{ (H_x, H_y, L_x, L_y) \mid H_x, H_y, L_x, L_y \in \{ 0,
\ldots, 1000 \} \}$, where $(H_x, H_y)$ and $(L_x, L_y)$ are the
positions of Han and Leia, respectively.
\item $Q_0 = \{ (0, 0, 0, 1000) \}$
\item $\delta: (H_x, H_y, L_x, L_y) \mapsto (H_x + 3a, H_y + 3b, L_x + 3c,
L_y + 3d)$, where \\
$(a, b, c, d) \in \{
(1,0,0,0),(-1,0,0,0),(0,1,0,0),(0,-1,0,0),(1,1,0,0),(1,-1,0,0),$\\
$(-1,1,0,0),(-1,-1,0,0),(0,0,1,0),(0,0,-1,0),(0,0,0,1),(0,0,0,-1) \}$
\end{description}
(A common error here was to say that $Q = \{ (a, b, c, d) \mid a, b,
c, d \in \{ 0, \ldots, 1000 \} \}$, without saying what the four
numbers in a state actually correspond to.)}

\problempart 
Prove formally (using an invariant) that no sequence of moves can
yield a meeting between Han and Leia.

\solution{
Our invariant is: ``For any reachable state $q = (H_x, H_y, L_x, L_y)$, 
$H_x + H_y - L_x - L_y \equiv 2 \pmod{3}$.''

For notational convenience, let $r(q) = H_x + H_y - L_x - L_y$.  For
the only possible initial state~$q_0$, $r(q_0) = -1000$, so $r(q_0)
\equiv 2 \pmod{3}$.  For any $(q,q') \in \delta$, we note that
$r(q')-r(q)$ is always a multiple of~$3$. Hence, for any $(q,q') \in
\delta$, $r(q) \equiv 2 \pmod{3}$ implies $r(q') \equiv 2 \pmod{3}$.
By the Invariant Theorem, this implies that $r(q) \equiv 2 \pmod{3}$
for every reachable state~$q$.

We now prove that the invariant implies that Han and Leia can never
meet. Suppose, for a contradiction, that Han and Leia can meet in some
state~$q$. That would imply that $r(q) = 0$. However, we just showed
that $r(q)$ can never be~$0$ in a reachable state, which yields a
contradiction.

(Common errors in this problem: Using the Invariant Theorem without
saying so; Not proving that the invariant implies that Han and Leia
scan never meet.)}

\end{problemparts}
\end{problem}
                                 