big report update with examples

[mc1516pa.git] / report2 / results.tex

diff --git a/report2/results.tex b/report2/results.tex
index e69de29..e8b29e7 100644 (file)
--- a/report2/results.tex
+++ b/report2/results.tex
@@ -0,0 +1,34 @@
+\section{Results \& How-to}
+\subsection{Results}
+This approach is not very efficient yet. While it is a bit faster than the
+previous \textsc{NuSMV} approach it is not capable of handling bigger screens.
+
+\begin{tabular}{lll}
+       \toprule
+       Screen no. & \textsc{NuSMV} & This program\\
+       \midrule
+       $2000$ & $n$ & $n$\\
+       \bottomrule
+\end{tabular}
+
+\subsection{How-to}
+The program can be built by running \texttt{make}. \texttt{make} expects the
+sylvan headers to be located in \texttt{./sylvan/src} and the library archive
+in \texttt{./sylvan/src/libsylvan.a}. If this is not the case one can adapt the
+makefile or set the appropriate \texttt{CFLAGS} and \texttt{LDFLAGS}.
+
+When the main program is executed with the \texttt{-h} flag the help is shown.
+Note that the program is very silent when the \texttt{-v} flag is not set.
+\begin{lstlisting}
+Usage:
+    ./main [opts] [FILE]
+
+Options:
+    -l LURD  LURD verification strategy
+    -v       enable verbose output
+    -h       show this help
+
+Positional arguments:
+    FILE     zero or one sokoban screens
+             when no file is specified stdin will be used
+\end{lstlisting}