report2/results.tex

   1 \section{Results \& How-to}
   2 \subsection{Results}
   3 This approach is not very efficient yet. Below are some execution times for
   4 several screens:
   5
   6 \begin{tabular}{lll}
   7         \toprule
   8         Screen no. & Boxes & Size & Time\\
   9         \midrule
  10         $2000$ & $1$ & $12$ & $0.05s$\\
  11         $107$ & $3$ & $16$ & $1.19s$\\
  12         \bottomrule
  13 \end{tabular}
  14
  15 \subsection{How-to}
  16 The latest version of the modelchecker can be obtained by cloning the
  17 repository, building sylvan and building the modelchecker with the following
  18 commands:
  19
  20 \begin{lstlisting}
  21 $ git clone --recursive https://github.com/dopefishh/mc1516pa.git
  22 $ cd mc1516pa/modelchecker/sylvan
  23 $ cmake .
  24 $ make
  25 $ cd ..
  26 $ make
  27 \end{lstlisting}
  28
  29 The makefile of the modelchecker expects the sylvan headers to be located in
  30 \texttt{./sylvan/src} and the library archive in
  31 \texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
  32 makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.
  33
  34 When the main program is executed with the \texttt{-h} flag the help is shown.
  35 Note that the program is very silent when the \texttt{-v} flag is not set.
  36 \begin{lstlisting}
  37 Usage:
  38     ./main [opts] [FILE]
  39
  40 Options:
  41     -l LURD  initial LURD
  42     -v       enable verbose output
  43     -h       show this help
  44
  45 Positional arguments:
  46     FILE     zero or one sokoban screens
  47              when no file is specified stdin will be used
  48 \end{lstlisting}
  49
  50 \subsection{Extra 1: Initial LURD}
  51 Using the \texttt{-l} option the user can give a initial LURD to the program.
  52 LURD stands for Left, Up, Right, Down sequence and is a string consisting only
  53 of $l,u,r,d$ characters and it specifies the initial moves to be taken by the
  54 agent. To achieve this we simple for every character in the lurd update the
  55 initial state with the relative product of the transitions belonging to the
  56 correct direction. After that the problem is solved as usual and thus notifying
  57 the user wether the LURD leads to a solvable state. Note that when the LURD is
  58 empty the program behaves like there was no LURD given.
  59
  60 \subsection{Evaluation}
  61 The assignment was a very interesting and challenging assignment. However, we
  62 feel that we could not get the most out of it due to several reasons.
  63
  64 First of all it was a hassle to get to know sylvan and to be able to use the
  65 package. There were some trivial errors in the sylvan package that made
  66 debugging a lot harder. One of those errors was malformed dot output for
  67 printing BDDs. In the meantime we have made a pullrequest to fix that.
  68
  69 Secondly, due to the relatively short introduction to BDDs the gap between our
  70 knowlegde and the knowledge required to build such a solver is quite big. This
  71 lead to startup problems.
  72
  73 % Maybe something about the complexity of the assignment