*.log
*.aux
*.fmt
+*.png
+*.toc
LATEX:=pdflatex
DOCUMENT:=report
+GRAPHS:=toy.png toy2.png toy3.png
.PHONY: all clean
-.SECONDARY: $(DOCUMENT).fmt
+.SECONDARY: $(DOCUMENT).fmt $(GRAPHS)
all: $(DOCUMENT).pdf
-%.pdf: %.tex %.fmt implementation.tex results.tex
+%.pdf: %.tex %.fmt implementation.tex results.tex $(GRAPHS)
$(LATEX) $<
$(LATEX) $<
+%.png: %.dot
+ dot -Tpng $< > $@
+
%.fmt: pre.tex
$(LATEX) -ini -shell-escape -jobname="$(basename $@)" "&$(LATEX) $<\dump"
clean:
- $(RM) -rv $(addprefix $(DOCUMENT).,fmt log aux pdf)
+ $(RM) -rv $(addprefix $(DOCUMENT).,fmt log aux pdf) *.png
\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}
\usepackage{a4wide}
\usepackage{amsmath}
\usepackage{amssymb}
+\usepackage{booktabs}
+\usepackage{graphicx}
\usepackage{listings}
\lstset{%
%&report
\begin{document}
\maketitle
+\tableofcontents
+
\input{implementation.tex}
\input{results.tex}
+\section{Results \& How-to}
+\subsection{Results}
+This approach is not very efficient yet. While it is a bit faster than the
+previous \textsc{NuSMV} approach it is not capable of handling bigger screens.
+
+\begin{tabular}{lll}
+ \toprule
+ Screen no. & \textsc{NuSMV} & This program\\
+ \midrule
+ $2000$ & $n$ & $n$\\
+ \bottomrule
+\end{tabular}
+
+\subsection{How-to}
+The program can be built by running \texttt{make}. \texttt{make} expects the
+sylvan headers to be located in \texttt{./sylvan/src} and the library archive
+in \texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
+makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.
+
+When the main program is executed with the \texttt{-h} flag the help is shown.
+Note that the program is very silent when the \texttt{-v} flag is not set.
+\begin{lstlisting}
+Usage:
+ ./main [opts] [FILE]
+
+Options:
+ -l LURD LURD verification strategy
+ -v enable verbose output
+ -h show this help
+
+Positional arguments:
+ FILE zero or one sokoban screens
+ when no file is specified stdin will be used
+\end{lstlisting}
--- /dev/null
+digraph "DD" {
+ rankdir=LR;
+ center = true;
+ graph [dpi = 300];
+ node [nodesep=0.75];
+ edge[weight=2, dir=forward];
+ "0" [shape=box, label="F", style=filled, shape=box, height=0.3, width=0.3];
+ "8000000000000000" [shape=box, label="T", style=filled, shape=box, height=0.3,
+ width=0.3];
+ root [style=invis];
+ root -> "19" [style=solid];
+ "19" [label="0"];
+ "19" -> "0" [style=dashed];
+ "19" -> "18" [style=solid];
+ "18" [label="2"];
+ "18" -> "17" [style=dashed];
+ "18" -> "0" [style=solid];
+ "17" [label="4"];
+ "17" -> "0" [style=dashed];
+ "17" -> "16" [style=solid];
+ "16" [label="6"];
+ "16" -> "15" [style=dashed];
+ "16" -> "0" [style=solid];
+ "15" [label="8"];
+ "15" -> "0" [style=dashed];
+ "15" -> "14" [style=solid];
+ "14" [label="10"];
+ "14" -> "13" [style=dashed];
+ "14" -> "0" [style=solid];
+ "13" [label="12"];
+ "13" -> "4" [style=dashed];
+ "13" -> "0" [style=solid];
+ "4" [label="14"];
+ "4" -> "0" [style=dashed];
+ "4" -> "2" [style=solid];
+ "2" [label="16"];
+ "2" -> "0" [style=dashed];
+ "2" -> "8000000000000000" [style=solid];
+ { rank=same; "19"; }
+ { rank=same; "18"; }
+ { rank=same; "17"; }
+ { rank=same; "16"; }
+ { rank=same; "15"; }
+ { rank=same; "14"; }
+ { rank=same; "13"; }
+ { rank=same; "4"; }
+ { rank=same; "2"; }
+}
--- /dev/null
+ ###
+#@$.#
+ ###
--- /dev/null
+digraph "DD" {
+ rankdir=LR;
+ center = true;
+ graph [dpi = 300];
+ node [nodesep=0.75];
+ edge[weight=2, dir=forward];
+ "0" [shape=box, label="F", style=filled, shape=box, height=0.3, width=0.3];
+ "8000000000000000" [shape=box, label="T", style=filled, shape=box, height=0.3,
+ width=0.3];
+ root [style=invis];
+ root -> "1b" [style=solid];
+ "1b" [label="12"];
+ "1b" -> "0" [style=dashed];
+ "1b" -> "800000000000001a" [style=solid];
+ "800000000000001a" [label="14"];
+ "800000000000001a" -> "8000000000000002" [style=dashed];
+ "800000000000001a" -> "0" [style=solid];
+ "8000000000000002" [label="16"];
+ "8000000000000002" -> "8000000000000000" [style=dashed];
+ "8000000000000002" -> "0" [style=solid];
+ { rank=same; "1b"; }
+ { rank=same; "800000000000001a"; }
+ { rank=same; "8000000000000002"; }
+}
--- /dev/null
+digraph DD {
+ rankdir=LR;
+ center = true;
+ graph [dpi = 300];
+ node [nodesep=0.75];
+ edge[weight=2, dir=forward];
+ t [label="...", style=filled, shape=box, height=0.3, width=0.3];
+ f [label="F", style=filled, shape=box, height=0.3, width=0.3];
+ root [style=invis];
+ root -> "0" [style=solid];
+ "0" -> "1" [style=solid];
+ "0" -> f [style=dashed];
+ "1" -> "2" [style=dashed];
+ "1" -> f [style=solid];
+ "2" -> "3" [style=dashed];
+ "2" -> f [style=solid];
+ "3" -> "4" [style=dashed];
+ "3" -> f [style=solid];
+ "4" -> "5" [style=solid];
+ "4" -> f [style=dashed];
+ "5" -> t [style=solid];
+ "5" -> f [style=dashed];
+}
repositories / mc1516pa.git / commitdiff