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 program can be built by running \texttt{make}. \texttt{make} expects the
  16 sylvan headers to be located in \texttt{./sylvan/src} and the library archive
  17 in \texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
  18 makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.
  19
  20 When the main program is executed with the \texttt{-h} flag the help is shown.
  21 Note that the program is very silent when the \texttt{-v} flag is not set.
  22 \begin{lstlisting}
  23 Usage:
  24     ./main [opts] [FILE]
  25
  26 Options:
  27     -l LURD  initial LURD
  28     -v       enable verbose output
  29     -h       show this help
  30
  31 Positional arguments:
  32     FILE     zero or one sokoban screens
  33              when no file is specified stdin will be used
  34 \end{lstlisting}
  35
  36 \subsection{Extra 1: Initial LURD}
  37 Using the \texttt{-l} option the user can give a initial LURD to the program.
  38 LURD stands for Left, Up, Right, Down sequence and is a string consisting only
  39 of $l,u,r,d$ characters and it specifies the initial moves to be taken by the
  40 agent. To achieve this we simple for every character in the lurd update the
  41 initial state with the relative product of the transitions belonging to the
  42 correct direction. After that the problem is solved as usual and thus notifying
  43 the user wether the LURD leads to a solvable state. Note that when the LURD is
  44 empty the program behaves like there was no LURD given.