big report update with examples

[mc1516pa.git] / report2 / implementation.tex

diff --git a/report2/implementation.tex b/report2/implementation.tex
index 1aa2322..d223227 100644 (file)
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -70,4 +70,49 @@ $$next(i_1, i_2, i_3)=\left\{\begin{array}{lll}
 \end{array}\right.$$
 
 \subsection{Example}
-For example, take the toy screen \texttt{\_\@\$} will be encoded as follows:
+For example, take the toy screen shown in Listing~\ref{lst:toy}. When the
+screen is parsed the unreachable space is first removed by detecting reachable
+space with the flood fill algorithm. This results in the minimized screen
+listed in Listing~\ref{lst:toy2}.
+
+\lstinputlisting[label={lst:toy},caption={Example screen}]{toy.screen}
+\lstinputlisting[label={lst:toy2},caption={Example screen}]{toy2.screen}
+
+\subsubsection{Encoding}
+To encode the screen the tiles are numbered from left to right from top to
+bottom. Thus resulting in $i_1=agent, i_2=box, i_3=target$. When we translate
+these numbers to sylvan-sane variables we get the following bdd shown in
+Figure~\ref{fig:toy}. Variables $0, 2, 4$ represent $i_1$, $6, 8, 10$ represent
+$i_2$ and lastly $12, 14, 16$ represents $i_3$.
+\begin{figure}[p]
+       \centering
+       \includegraphics[scale=0.1]{toy.png}
+       \caption{Initial state encoding of the example~\label{fig:toy}}
+\end{figure}
+
+Encoding the goal state happens in a similar way. The algorithm basically
+states that all $target$ positions should be $boxtarget$. This is results in
+the BDD shown in Figure~\ref{fig:toy2}.
+
+\begin{figure}[p]
+       \centering
+       \includegraphics[scale=0.1]{toy2.png}
+       \caption{Goal state encoding of the example~\label{fig:toy2}}
+\end{figure}
+
+Finally encoding the transitions already results in a long list of complicated
+BDDs that each encode a possible move in all possible directions. In this
+example there is only one move possible in the first state, thus all moves
+except for the one move result in a relative product that is empty. For example
+the sub-BDD that encodes the first position only looks is visualized in
+Figure~\ref{fig:toy3}. The only satisfying assignment is that $0, 2, 4$ hold
+the values $1, 0, 1$ thus encoding man and the variables $1, 3, 5$ holding the
+values $0, 0, 1$ thus encoding free.
+
+\begin{figure}[p]
+       \centering
+       \includegraphics[scale=0.1]{toy3.png}
+       \caption{Sub-BDD of a move~\label{fig:toy3}}
+\end{figure}
+
+\subsubsection{Results}