NeighbourSum: added NuSMV

3 files changed, 78 insertions, 8 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