From c5f75f950c9b965242f43067ff619139fcbbd42e Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 21 Apr 2016 16:38:13 +0200 Subject: [PATCH] big report update with examples --- report2/.gitignore | 2 ++ report2/Makefile | 10 +++++--- report2/implementation.tex | 47 ++++++++++++++++++++++++++++++++++++- report2/pre.tex | 2 ++ report2/report.tex | 2 ++ report2/results.tex | 34 +++++++++++++++++++++++++++ report2/toy.dot | 48 ++++++++++++++++++++++++++++++++++++++ report2/toy.screen | 3 +++ report2/toy2.dot | 24 +++++++++++++++++++ report2/toy2.screen | 1 + report2/toy3.dot | 23 ++++++++++++++++++ 11 files changed, 192 insertions(+), 4 deletions(-) create mode 100644 report2/toy.dot create mode 100644 report2/toy.screen create mode 100644 report2/toy2.dot create mode 100644 report2/toy2.screen create mode 100644 report2/toy3.dot diff --git a/report2/.gitignore b/report2/.gitignore index d8b763f..f336c9b 100644 --- a/report2/.gitignore +++ b/report2/.gitignore @@ -2,3 +2,5 @@ *.log *.aux *.fmt +*.png +*.toc diff --git a/report2/Makefile b/report2/Makefile index 66efe76..5a22879 100644 --- a/report2/Makefile +++ b/report2/Makefile @@ -1,17 +1,21 @@ 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 diff --git a/report2/implementation.tex b/report2/implementation.tex index 1aa2322..d223227 100644 --- 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} diff --git a/report2/pre.tex b/report2/pre.tex index 0320a7f..06b1825 100644 --- a/report2/pre.tex +++ b/report2/pre.tex @@ -3,6 +3,8 @@ \usepackage{a4wide} \usepackage{amsmath} \usepackage{amssymb} +\usepackage{booktabs} +\usepackage{graphicx} \usepackage{listings} \lstset{% diff --git a/report2/report.tex b/report2/report.tex index 7f2ce0f..4d5f181 100644 --- a/report2/report.tex +++ b/report2/report.tex @@ -1,6 +1,8 @@ %&report \begin{document} \maketitle +\tableofcontents + \input{implementation.tex} \input{results.tex} diff --git a/report2/results.tex b/report2/results.tex index e69de29..e8b29e7 100644 --- a/report2/results.tex +++ b/report2/results.tex @@ -0,0 +1,34 @@ +\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} diff --git a/report2/toy.dot b/report2/toy.dot new file mode 100644 index 0000000..907f199 --- /dev/null +++ b/report2/toy.dot @@ -0,0 +1,48 @@ +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"; } +} diff --git a/report2/toy.screen b/report2/toy.screen new file mode 100644 index 0000000..e02031d --- /dev/null +++ b/report2/toy.screen @@ -0,0 +1,3 @@ + ### +#@$.# + ### diff --git a/report2/toy2.dot b/report2/toy2.dot new file mode 100644 index 0000000..7c94229 --- /dev/null +++ b/report2/toy2.dot @@ -0,0 +1,24 @@ +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"; } +} diff --git a/report2/toy2.screen b/report2/toy2.screen new file mode 100644 index 0000000..8d4f16e --- /dev/null +++ b/report2/toy2.screen @@ -0,0 +1 @@ +@$. diff --git a/report2/toy3.dot b/report2/toy3.dot new file mode 100644 index 0000000..0905394 --- /dev/null +++ b/report2/toy3.dot @@ -0,0 +1,23 @@ +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]; +} -- 2.20.1