Merge branch 'master' of https://github.com/dopefishh/mc1516pa

diff --git a/modelchecker/benchmark.sh b/modelchecker/benchmark.sh
index 05808dd..189dfd5 100644 (file)
--- 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 539f5a6..0f84b72 100644 (file)
--- a/report2/implementation.tex
+++ b/report2/implementation.tex
@@ -94,7 +94,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..f35556c 100644 (file)
--- a/report2/results.tex
+++ b/report2/results.tex
@@ -1,13 +1,19 @@
 \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}
+\begin{tabular}{llll}
        \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$\\
+       $101$ & $3$ & $20$ & $1.49s$\\
+       $102$ & & $0.66s$\\
+       $103$ & & $1.02s$\\
+       $104$ & & $1.39s$\\
+       $105$ & & $1.70s$\\
        \bottomrule
 \end{tabular}