From 03640bc04e209d703de8c206d433685c763c30b2 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 21 Apr 2016 20:39:06 +0200
Subject: [PATCH] Update report

---
 report2/implementation.tex | 23 +++++++++++++++++++++--
 report2/pre.tex            |  1 +
 report2/results.tex        | 19 ++++++++++++++++---
 3 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/report2/implementation.tex b/report2/implementation.tex
index b4a1d77..c69d4a1 100644
--- 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
--- 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
--- 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.
-- 
2.20.1