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}{llll}
   7         \toprule
   8         Screen no. & Boxes & Size & Time\\
   9         \midrule
  10         $2000$ & $1$ & $12$ & $0.05s$\\
  11         $107$ & $3$ & $16$ & $1.19s$\\
  12         $101$ & $3$ & $20$ & $1.49s$\\
  13         $102$ & & $0.66s$\\
  14         $103$ & & $1.02s$\\
  15         $104$ & & $1.39s$\\
  16         $105$ & & $1.70s$\\
  17         \bottomrule
  18 \end{tabular}
  19
  20 \subsection{How-to}
  21 The latest version of the modelchecker can be obtained by cloning the
  22 repository, building sylvan and building the modelchecker with the following
  23 commands:
  24
  25 \begin{lstlisting}
  26 $ git clone --recursive https://github.com/dopefishh/mc1516pa.git
  27 $ cd mc1516pa/modelchecker/sylvan
  28 $ cmake .
  29 $ make
  30 $ cd ..
  31 $ make
  32 \end{lstlisting}
  33
  34 The makefile of the modelchecker expects the sylvan headers to be located in
  35 \texttt{./sylvan/src} and the library archive in
  36 \texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
  37 makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.
  38
  39 When the main program is executed with the \texttt{-h} flag the help is shown.
  40 Note that the program is very silent when the \texttt{-v} flag is not set.
  41 \begin{lstlisting}
  42 Usage:
  43     ./main [opts] [FILE]
  44
  45 Options:
  46     -l LURD  initial LURD
  47     -v       enable verbose output
  48     -h       show this help
  49
  50 Positional arguments:
  51     FILE     zero or one sokoban screens
  52              when no file is specified stdin will be used
  53 \end{lstlisting}
  54
  55 \subsection{Extra 1: Initial LURD}
  56 Using the \texttt{-l} option the user can give a initial LURD to the program.
  57 LURD stands for Left, Up, Right, Down sequence and is a string consisting only
  58 of $l,u,r,d$ characters and it specifies the initial moves to be taken by the
  59 agent. To achieve this we simple for every character in the lurd update the
  60 initial state with the relative product of the transitions belonging to the
  61 correct direction. After that the problem is solved as usual and thus notifying
  62 the user wether the LURD leads to a solvable state. Note that when the LURD is
  63 empty the program behaves like there was no LURD given.
  64
  65 \subsection{Evaluation}
  66 The assignment was a very interesting and challenging assignment. However, we
  67 feel that we could not get the most out of it due to several reasons.
  68
  69 First of all it was a hassle to get to know sylvan and to be able to use the
  70 package. The most problematic was to understand how can we work with state transitions efficiently. The way it works with sylvan was not evident neither from the introductory lectures, nor from the available documentation. Also, there were some trivial errors in the sylvan package that made
  71 debugging a lot harder. One of those errors was malformed dot output for
  72 printing BDDs. In the meantime we have made a pullrequest to fix that.
  73
  74 Secondly, due to the relatively short introduction to BDDs the gap between our
  75 knowlegde and the knowledge required to build such a solver is quite big. This
  76 lead to startup problems (which we managed to solve, but lost too much time to it).
  77
  78 Finally, we feel a bit frustrated that we only finished and tested the reachability of a goal state checking, but did not finish the extraction of solving sequences.
  79
  80 % Maybe something about the complexity of the assignment