NeighbourSum: added NuSMV

4 files changed, 228 insertions, 11 deletions

diff --git a/integer_sum_from_neighbours/NeighbourSum.java b/integer_sum_from_neighbours/NeighbourSum.java
deleted file mode 100644
index 364a3dd..0000000
--- a/integer_sum_from_neighbours/NeighbourSum.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package PACKAGE_NAME;
-
-/**
- * Created by koen on 12/11/16.
- */
-public class NeighbourSum {
-}
diff --git a/integer_sum_from_neighbours/generate-neighborsum.py b/integer_sum_from_neighbours/generate-neighborsum.py
index 14a8d23..d0b1950 100755
--- a/integer_sum_from_neighbours/generate-neighborsum.py
+++ b/integer_sum_from_neighbours/generate-neighborsum.py
@@ -2,7 +2,7 @@
 # Usage for 4a (where 7 is the number of steps to run):
 #   $0 7 | z3 -smt -in
 # Usage for 4b:
-#   $0 7 b | z3 -smt -in
+#   $0 17 b | z3 -smt -in
 import sys
 
 # i = 1..8
diff --git a/integer_sum_from_neighbours/generate-neighborsumsmv.py b/integer_sum_from_neighbours/generate-neighborsumsmv.py
new file mode 100755
index 0000000..5337219
--- /dev/null
+++ b/integer_sum_from_neighbours/generate-neighborsumsmv.py
@@ -0,0 +1,77 @@
+#!/usr/bin/env python
+# Usage for 4b (where 100 is the maximum value for the values):
+#   $0 100 | nusmv /dev/stdin
+
+import sys
+
+n = 8
+maxValue = int(sys.argv[1])
+is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
+
+def fillin(cases, template_vars):
+    if type(cases) == str:
+        return cases.format(**template_vars)
+    return [template.format(**template_vars) for template in cases]
+
+variables = ["a%d" % i for i in range(1, n+1)]
+
+# vars: a_1 .. a_n
+varDefs = " ".join("%s : 0..%d;" % (x, maxValue) for x in variables)
+
+# initial values: a_i = i
+initVals = ""
+initVals += " & ".join("%s = %d" % (var, i + 1) for i, var in enumerate(variables))
+
+# Transitions:
+# - any of the alternatives: sum one, keep others.
+trans = "next(a1) = a1 & next(a{n}) = a{n} & (\n".format(n=n)
+# The first and last one cannot be changed. In a step, one can choose to
+# change a_i for any i, leaving all other j (i != j) intact.
+altpreds = []
+for i in range(2, n):
+    prev = i - 1
+    next = i + 1
+
+    # Require a'_i = a_{i-1} + a_{i+1}
+    statepreds = fillin([
+        "next(a{i}) = a{prev} + a{next}"
+    ], vars())
+
+    # Require a'_j = a_j for i != j
+    for j in range(2, n):
+        if i == j:
+            continue
+        statepreds += fillin([
+            "next(a{j}) = a{j}"
+        ], vars())
+    altpreds += [
+        "(%s)" % " & ".join(statepreds)
+    ]
+trans += "|\n".join(altpreds)
+trans += ")"
+
+# Desired condition
+if not is_b:
+    spec = "! (a3 = a7)"
+else:
+    spec = "! (a3 = a5 & a5 = a7)"
+
+# Begin generator
+s = """MODULE main
+VAR
+{varDefs}
+INIT
+{initVals}
+TRANS
+{trans}
+LTLSPEC G {spec}
+""".format(**vars())
+
+try:
+    import sys
+    print(s)
+    # Hack to avoid printing a ugly error in case stdin of next pipe is closed.
+    sys.stdout.flush()
+    sys.stdout.close()
+except BrokenPipeError:
+    pass
diff --git a/part1.tex b/part1.tex
index 382baaf..2fa9400 100644
--- a/part1.tex
+++ b/part1.tex
@@ -450,8 +450,8 @@ unchanged.
 \begin{itemize}
 \item[(a)] Show how it is possible that $a_3 = a_7$ after a number of steps.
 \item[(b)] Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps.
-For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.
 \end{itemize}
+For this problem both try to use an SMT solver and NuSMV, and discuss how they perform.
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
@@ -530,7 +530,7 @@ in each step are highlighted. Indeed, $a_3=a_7=20$ after some steps.}
 \end{table}
 
 \begin{lstlisting}[
-    caption={Generated SMT output for $n=8, m=7$ that satisfies $a_3=a_7$},
+    caption={Generated SMT program for $n=8, m=7$ that satisfies $a_3=a_7$},
     label={lst:sumA},language=lisp,basicstyle=\scriptsize
 ]
 (benchmark test.smt
@@ -562,7 +562,6 @@ in each step are highlighted. Indeed, $a_3=a_7=20$ after some steps.}
        (= a1_7 a1_6) ...  (= a8_7 a8_6))
   )
 ))
-
 \end{lstlisting}
 
 \textbf{Remark}: we observed that for some larger choices of $m$ (say $m=20$),
@@ -572,6 +571,149 @@ previous value is already the sum of the neighbors, then the new sum will be
 equal to the previous one. As the other variables remain unchanged, the whole
 state will have the same values as the previous state.
 
+The same problem was also solved with NuSMV. Here we do not model every possible
+transition between state $s-1$ and $s$ (for all $1 \leq s < m$). Instead, we
+describe the form of a transition in terms of the begin state and the next
+state for $n$ variables (and no $m$ parameter is necessary). Again, only one of
+the variables are updated while all others stay unchanged, this can be expressed
+in NuSMV as follows:
+\begin{align*}
+\bigvee_{1 < i < n}
+next(a_i) = a_{i-1} + a_{i+1}
+\land
+(\bigwedge_{1 \leq j \leq n, i \neq j} next(a_j) = a_j)
+\end{align*}
+
+In the given problem, the first and last elements are unchanged (as before), so
+$next(a_1)=a_1 \land next(a_n) = a_n$ can be moved outside the large
+disjunction.
+
+As for the initialization, the range $0..100$ was chosen arbitrarily, but given
+the answer from the SMT solver, we know that it should be sufficient.
+
+To find out when the desired condition ($a_3=a_7$) is satisfied for the first
+time, we add a $\lnot (a_3=a_7)$ as global formula. When a counter example is
+found, then we know that this particular run exhibits the desired condition.
+
+Listing~\ref{lst:sumAsmv} shows the full implementation for $n=8$. NuSMV found a
+counterexample (shown in Listing~\ref{lst:sumAsmvOutput}) and took 51 seconds.
+This is much longer than the SMT solver (which solved this setting in 5
+seconds). Interestingly, by reducing the maximum values of $a_i$ from 100 to 20,
+the running time dropped to less than a second. Reducing the maximum to 19
+yields no counterexample and also completed in a fraction of a second.
+For a maximum of 50, the running time is 6 seconds. Indeed, increasing the
+maximum value also results in larger trees with more nodes to check. Choosing
+the maximum too small might fail to find a satisfying assignment while a too
+large value incurs a performance hit.
+
+\begin{lstlisting}[
+    caption={Generated NuSMV program for $n=8$ that searches for $a_3=a_7$.},
+    label={lst:sumAsmv},basicstyle=\tiny
+]
+MODULE main
+VAR
+a1 : 0..100; a2 : 0..100; a3 : 0..100; a4 : 0..100; a5 : 0..100; a6 : 0..100; a7 : 0..100; a8 : 0..100;
+INIT
+a1 = 1 & a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & a7 = 7 & a8 = 8
+TRANS
+next(a1) = a1 & next(a8) = a8 & (
+(next(a2) = a1 + a3 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
+(next(a3) = a2 + a4 & next(a2) = a2 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
+(next(a4) = a3 + a5 & next(a2) = a2 & next(a3) = a3 & next(a5) = a5 & next(a6) = a6 & next(a7) = a7)|
+(next(a5) = a4 + a6 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a6) = a6 & next(a7) = a7)|
+(next(a6) = a5 + a7 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a7) = a7)|
+(next(a7) = a6 + a8 & next(a2) = a2 & next(a3) = a3 & next(a4) = a4 & next(a5) = a5 & next(a6) = a6))
+LTLSPEC G ! (a3 = a7)
+\end{lstlisting}
+
+\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}
+\end{minipage}
+\hfill
+\begin{minipage}{.45\textwidth}
+\begin{lstlisting}[
+    caption={NuSMV program for $n=8$ and maximum value 100 that satisfies
+    $a_3=a_5=a_7=46$ after 17 rounds.},
+    label={lst:sumAsmvOutput2},basicstyle=\tiny
+]
+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 <-
+    a4 = 8
+  -> State: 1.3 <-
+    a3 = 10
+  -> State: 1.4 <-
+    a2 = 11
+  -> State: 1.5 <-
+    a3 = 19
+  -> State: 1.6 <-
+    a2 = 20
+  -> State: 1.7 <-
+    a3 = 28
+  -> State: 1.8 <-
+    a2 = 29
+  -> State: 1.9 <-
+    a3 = 37
+  -> State: 1.10 <-
+    a6 = 12
+  -> State: 1.11 <-
+    a7 = 20
+  -> State: 1.12 <-
+    a6 = 25
+  -> State: 1.13 <-
+    a7 = 33
+  -> State: 1.14 <-
+    a6 = 38
+  -> State: 1.15 <-
+    a7 = 46
+  -> State: 1.16 <-
+    a5 = 46
+  -> State: 1.17 <-
+    a2 = 38
+  -> State: 1.18 <-
+    a3 = 46
+\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:
@@ -616,4 +758,9 @@ seconds and shown in Table~\ref{tbl:sumB}.
 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}