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  LURD verification strategy
  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}