From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 21 Apr 2016 19:14:40 +0000 (+0200)
Subject: up
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=b8a410cd79ea64cd9fb3a2efa9d50c28ba1b785a;p=mc1516pa.git

up
---

diff --git a/modelchecker/benchmark.sh b/modelchecker/benchmark.sh
index 05808dd..189dfd5 100644
--- a/modelchecker/benchmark.sh
+++ b/modelchecker/benchmark.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 make
-for i in 2000 107 1001 387 372 792 747 38 754 2; do
+for i in 2000 107; do
 	echo "Problem: $i"
-	time ./main -v ../sokobanzip/screens/screen.$i
+	time ./main ../sokobanzip/screens/screen.$i
 done
diff --git a/report2/implementation.tex b/report2/implementation.tex
index c69d4a1..5835f08 100644
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -93,7 +93,7 @@ solution.
 		\ForEach{$R_i$}{
 			$V_{new}\leftarrow BDDapply(\vee, V_{new}, BDDrelprod(V_{new}, R_i)$\;
 		}
-		\lIf{$BDDsatcount(BDDand(G, new))>0$}{$break$}
+		\lIf{$BDDsatcount(BDDand(G, V_{new}))>0$}{$break$}
 	}
 \end{algorithm}
 
diff --git a/report2/results.tex b/report2/results.tex
index 78331bb..5bd0ba1 100644
--- a/report2/results.tex
+++ b/report2/results.tex
@@ -1,13 +1,14 @@
 \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.
+This approach is not very efficient yet. Below are some execution times for
+several screens:
 
 \begin{tabular}{lll}
 	\toprule
-	Screen no. & \textsc{NuSMV} & This program\\
+	Screen no. & Boxes & Size & Time\\
 	\midrule
-	$2000$ & $n$ & $n$\\
+	$2000$ & $1$ & $12$ & $0.05s$\\
+	$107$ & $3$ & $16$ & $1.19s$\\
 	\bottomrule
 \end{tabular}