From 7eef4433fdea705038cbc504005ea74d502b7d53 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Wed, 14 Dec 2016 15:13:55 +0100 Subject: NeighborSum: move NuSMV result next to SMT solver, add explanation --- part1.tex | 168 ++++++++++++++++++++++++++++++++------------------------------ 1 file 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} -- cgit v1.2.1