From b8a410cd79ea64cd9fb3a2efa9d50c28ba1b785a Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 21 Apr 2016 21:14:40 +0200 Subject: [PATCH] up --- modelchecker/benchmark.sh | 4 ++-- report2/implementation.tex | 2 +- report2/results.tex | 9 +++++---- 3 files changed, 8 insertions(+), 7 deletions(-) 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} -- 2.20.1