report2/results.tex

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