NeighborSum: move NuSMV result next to SMT solver, add explanation

1 files changed, 87 insertions, 81 deletions

diff --git a/part1.tex b/part1.tex
index 2fa9400..a54e186 100644
--- a/part1.tex
+++ b/part1.tex
@@ -511,6 +511,7 @@ The annotated, generated input for \texttt{z3} is shown in
 Listing~\ref{lst:sumA} while the z3 output is formatted into
 Table~\ref{tbl:sumA}.
 
+\begin{minipage}{.45\textwidth}
 \begin{table}[H]
 \centering
 \begin{tabular}{r|rrrrrrrr}
@@ -528,6 +529,40 @@ Table~\ref{tbl:sumA}.
 \caption{\label{tbl:sumA}The values of each variable where the modified values
 in each step are highlighted. Indeed, $a_3=a_7=20$ after some steps.}
 \end{table}
+\end{minipage}
+\hfill
+\begin{minipage}{.45\textwidth}
+\begin{lstlisting}[
+    caption={NuSMV output for $n=8$ and maximum value 100 that satisfies
+    $a_3=a_7=20$ after 8 rounds.},
+    label={lst:sumAsmvOutput},basicstyle=\scriptsize
+]
+Trace Type: Counterexample
+  -> State: 1.1 <-
+    a1 = 1
+    a2 = 2
+    a3 = 3
+    a4 = 4
+    a5 = 5
+    a6 = 6
+    a7 = 7
+    a8 = 8
+  -> State: 1.2 <-
+    a3 = 6
+  -> State: 1.3 <-
+    a4 = 11
+  -> State: 1.4 <-
+    a3 = 13
+  -> State: 1.5 <-
+    a6 = 12
+  -> State: 1.6 <-
+    a7 = 20
+  -> State: 1.7 <-
+    a4 = 18
+  -> State: 1.8 <-
+    a3 = 20
+\end{lstlisting}
+\end{minipage}
 
 \begin{lstlisting}[
     caption={Generated SMT program for $n=8, m=7$ that satisfies $a_3=a_7$},
@@ -626,38 +661,59 @@ next(a1) = a1 & next(a8) = a8 & (
 LTLSPEC G ! (a3 = a7)
 \end{lstlisting}
 
+
+
+\subsubsection*{(b)}
+The generic approach from (a) can be adopted for this solution with a minor
+modification. Simply replace the second ingredient by:
+\begin{align}
+\label{eq:sum2new}
+\bigvee_{s=0}^m a_{3,s} = a_{5,s} \land a_{5,s} = a_{7,s}
+\end{align}
+
+Interestingly, the runtime of the SMT solver varies. For $m=25$, a solution was
+found in 9 seconds. For $m=22$, it took 5 seconds to find one. For $m=10, 15,
+16$, no satisfying assignment was found in respectively 1, 82 and 286 seconds.
+$m=17$ is apparently the minimal satisfying solution which was found in 3.5
+seconds and shown in Table~\ref{tbl:sumB}.
+(Also interesting was that $m=18, 19, 20$ also found satisfying solutions in
+3.2, 5.9 and 3.0 seconds (in that order).)
+
+The NuSMV program needs a similar modification to the \texttt{LTLSPEC} line, its
+output is shown in in Listing~\ref{lst:sumAsmvOutput2}. This also took 51
+seconds, just like (a). Lowering the maximum from 100 to 46 reduced the running
+time to about 2.2 seconds while a maximum value of 50 took 3.5 seconds. The
+explanation from (a) about the relation between the maximum value and the
+running time is still valid.
+
 \begin{minipage}{.45\textwidth}
-\begin{lstlisting}[
-    caption={NuSMV program for $n=8$ and maximum value 100 that satisfies
-    $a_3=a_7=20$ after 8 rounds (State 1.1 is the initial state, State 1.8 is
-    the seventh step).},
-    label={lst:sumAsmvOutput},basicstyle=\scriptsize
-]
-Trace Type: Counterexample
-  -> State: 1.1 <-
-    a1 = 1
-    a2 = 2
-    a3 = 3
-    a4 = 4
-    a5 = 5
-    a6 = 6
-    a7 = 7
-    a8 = 8
-  -> State: 1.2 <-
-    a3 = 6
-  -> State: 1.3 <-
-    a4 = 11
-  -> State: 1.4 <-
-    a3 = 13
-  -> State: 1.5 <-
-    a6 = 12
-  -> State: 1.6 <-
-    a7 = 20
-  -> State: 1.7 <-
-    a4 = 18
-  -> State: 1.8 <-
-    a3 = 20
-\end{lstlisting}
+\begin{table}[H]
+\centering
+\begin{tabular}{r|rrrrrrrr}
+   & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\
+\hline
+ 0 &     1 &     2 &     3 &     4 &     5 &     6 &     7 &     8 \\
+ 1 &     1 &     2 &     3 & \bf 8 &     5 &     6 &     7 &     8 \\
+ 2 &     1 &     2 &     3 &     8 &     5 & \bf12 &     7 &     8 \\
+ 3 &     1 & \bf 4 &     3 &     8 &     5 &    12 &     7 &     8 \\
+ 4 &     1 &     4 &     3 &     8 &     5 &    12 & \bf20 &     8 \\
+ 5 &     1 &     4 & \bf12 &     8 &     5 &    12 &    20 &     8 \\
+ 6 &     1 & \bf13 &    12 &     8 &     5 &    12 &    20 &     8 \\
+ 7 &     1 &    13 &    12 &     8 & \bf20 &    12 &    20 &     8 \\
+ 8 &     1 &    13 & \bf21 &     8 &    20 &    12 &    20 &     8 \\
+ 9 &     1 &    13 &    21 &     8 &    20 & \bf40 &    20 &     8 \\
+10 &     1 & \bf22 &    21 &     8 &    20 &    40 &    20 &     8 \\
+11 &     1 &    22 &    21 &     8 &    20 &    40 & \bf48 &     8 \\
+12 &     1 &    22 & \bf30 &     8 &    20 &    40 &    48 &     8 \\
+13 &     1 & \bf31 &    30 &     8 &    20 &    40 &    48 &     8 \\
+14 &     1 &    31 &    30 &     8 & \bf48 &    40 &    48 &     8 \\
+15 &     1 &    31 & \bf39 &     8 &    48 &    40 &    48 &     8 \\
+16 &     1 & \bf40 &    39 &     8 &    48 &    40 &    48 &     8 \\
+17 &     1 &    40 & \bf48 &     8 &    48 &    40 &    48 &     8 \\
+\end{tabular}
+\caption{\label{tbl:sumB}The values of each variable where modified values in
+each step are highlighted. Indeed, $a_3=a_5=a_7=48$ after some steps.}
+\end{table}
 \end{minipage}
 \hfill
 \begin{minipage}{.45\textwidth}
@@ -713,54 +769,4 @@ Trace Type: Counterexample
 \end{lstlisting}
 \end{minipage}
 
-
-\subsubsection*{(b)}
-The generic approach from (a) can be adopted for this solution with a minor
-modification. Simply replace the second ingredient by:
-\begin{align}
-\label{eq:sum2new}
-\bigvee_{s=0}^m a_{3,s} = a_{5,s} \land a_{5,s} = a_{7,s}
-\end{align}
-
-Interestingly, the runtime of the SMT solver varies. For $m=25$, a solution was
-found in 9 seconds. For $m=22$, it took 5 seconds to find one. For $m=10, 15,
-16$, no satisfying assignment was found in respectively 1, 82 and 286 seconds.
-$m=17$ is apparently the minimal satisfying solution which was found in 3.5
-seconds and shown in Table~\ref{tbl:sumB}.
-(Also interesting was that $m=18, 19, 20$ also found satisfying solutions in
-3.2, 5.9 and 3.0 seconds (in that order).)
-
-\begin{table}[H]
-\centering
-\begin{tabular}{r|rrrrrrrr}
-   & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\
-\hline
- 0 &     1 &     2 &     3 &     4 &     5 &     6 &     7 &     8 \\
- 1 &     1 &     2 &     3 & \bf 8 &     5 &     6 &     7 &     8 \\
- 2 &     1 &     2 &     3 &     8 &     5 & \bf12 &     7 &     8 \\
- 3 &     1 & \bf 4 &     3 &     8 &     5 &    12 &     7 &     8 \\
- 4 &     1 &     4 &     3 &     8 &     5 &    12 & \bf20 &     8 \\
- 5 &     1 &     4 & \bf12 &     8 &     5 &    12 &    20 &     8 \\
- 6 &     1 & \bf13 &    12 &     8 &     5 &    12 &    20 &     8 \\
- 7 &     1 &    13 &    12 &     8 & \bf20 &    12 &    20 &     8 \\
- 8 &     1 &    13 & \bf21 &     8 &    20 &    12 &    20 &     8 \\
- 9 &     1 &    13 &    21 &     8 &    20 & \bf40 &    20 &     8 \\
-10 &     1 & \bf22 &    21 &     8 &    20 &    40 &    20 &     8 \\
-11 &     1 &    22 &    21 &     8 &    20 &    40 & \bf48 &     8 \\
-12 &     1 &    22 & \bf30 &     8 &    20 &    40 &    48 &     8 \\
-13 &     1 & \bf31 &    30 &     8 &    20 &    40 &    48 &     8 \\
-14 &     1 &    31 &    30 &     8 & \bf48 &    40 &    48 &     8 \\
-15 &     1 &    31 & \bf39 &     8 &    48 &    40 &    48 &     8 \\
-16 &     1 & \bf40 &    39 &     8 &    48 &    40 &    48 &     8 \\
-17 &     1 &    40 & \bf48 &     8 &    48 &    40 &    48 &     8 \\
-\end{tabular}
-\caption{\label{tbl:sumB}The values of each variable where the modified values
-in each step are highlighted. Indeed, $a_3=a_5=a_7=48$ after some steps.}
-\end{table}
-
-The NuSMV program needs a similar modification to the \texttt{LTLSPEC} line, its
-output is shown in in Listing~\ref{lst:sumAsmvOutput2}. This also took 51
-seconds, just like (a). Lowering the maximum from 100 to 46 reduced the running
-time to about 2.2 seconds while a maximum value of 50 took 3.5 seconds.
-
 \end{document}