Update report

diff --git a/report2/implementation.tex b/report2/implementation.tex
index b4a1d77..c69d4a1 100644 (file)
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -75,8 +75,27 @@ $$next(i_1, i_2, i_3)=\left\{\begin{array}{lp{2pt}l}
 Encoding the goal state is very trivial. Just make sure all $target$ tiles are
 $targetbox$ tiles.
 
-\subsection{Lurd extraction}
-%TODO
+\subsection{Algorithm}
+We use the standard optimized reachability algorithm to solve a screen but
+added a goal condition that breaks the loop. When the loop breaks prematurely
+it means a solution is found. If the full loop continues until the entire state
+space is search and the break condition is not met it means there is no
+solution.
+
+\begin{algorithm}[H]
+       \KwIn{I, Initial state BDD}
+       \KwIn{$R_i$, List of transition BDDs}
+       \KwIn{G, Goal BDD}
+       $V_{old}\leftarrow BDDempty$\;
+       $V_{new}\leftarrow I$\;
+       \While{$V_{new}\neq V_{old}$}{
+               $V_{old}\leftarrow V_{new}$\;
+               \ForEach{$R_i$}{
+                       $V_{new}\leftarrow BDDapply(\vee, V_{new}, BDDrelprod(V_{new}, R_i)$\;
+               }
+               \lIf{$BDDsatcount(BDDand(G, new))>0$}{$break$}
+       }
+\end{algorithm}
 
 \subsection{Example}
 For example, take the toy screen shown as the first representation in

diff --git a/report2/pre.tex b/report2/pre.tex
index 7662be6..4ab2d42 100644 (file)
--- a/report2/pre.tex
+++ b/report2/pre.tex
@@ -2,6 +2,7 @@
 
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{algorithm2e}
 \usepackage{booktabs}
 \usepackage[a4paper]{geometry}
 \usepackage{graphicx}

diff --git a/report2/results.tex b/report2/results.tex
index c152f71..d9ba68c 100644 (file)
--- a/report2/results.tex
+++ b/report2/results.tex
@@ -12,9 +12,22 @@ previous \textsc{NuSMV} approach it is not capable of handling bigger screens.
 \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
+The latest version of the modelchecker can be obtained by cloning the
+repository, building sylvan and building the modelchecker with the following
+commands:
+
+\begin{lstlisting}
+$ git clone --recursive https://github.com/dopefishh/mc1516pa.git
+$ cd mc1516pa/modelchecker/sylvan
+$ cmake .
+$ make
+$ cd ..
+$ make
+\end{lstlisting}
+
+The makefile of the modelchecker 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.