NFA: initial solution

Python code is not cleaned up, it is working now... Generated LaTeX code
was not positioned correctly, so just use GraphViz then.

2 files changed, 246 insertions, 0 deletions

diff --git a/nfa/generate-nfa.py b/nfa/generate-nfa.py
new file mode 100755
index 0000000..6255bca
--- /dev/null
+++ b/nfa/generate-nfa.py
@@ -0,0 +1,118 @@
+#!/usr/bin/env python
+# Usage:
+#   $0 [number-of-states] | z3 -smt -in
+# Examples:
+#   $0 25
+
+import itertools
+import sys
+
+# Number of steps
+m = 25 if len(sys.argv) <= 1 else int(sys.argv[1])
+
+# all possible strings
+lang = [
+    "aa",
+    "bb",
+    "aba",
+    "baa",
+    "abab",
+    "babb",
+    "bbba",
+]
+
+# sledgehammer approach: specify all bad words
+fulllang = []
+for n in range(1, 4 + 1):
+    fulllang += [
+        "".join(x)
+        for x in itertools.product(*["ab"] * n)
+    ]
+# Remove good words.
+badlang = [word for word in fulllang if word not in lang]
+
+literals = []
+preds = []
+extrafuns = []
+
+# Populate Q = { q0, q1, ..., q_(m-1) } with unique values.
+literals += ["q%d" % i for i in range(m)]
+preds += ["(= q%d %d)" % (i, i) for i in range(m)]
+
+def mks(word_index, letter_index):
+    """Return variable for a state of a word after some transitions."""
+    return "s%d_%d" % (word_index, letter_index)
+
+# Assuming a single initial state (which may or may not be the final state),
+# add states for every letter j in each word i.
+for i, word in enumerate(lang):
+    for j, letter in enumerate(word):
+        v = mks(i, j)
+        literals += [v]
+        # Each of the states must be assigned to any of the states in Q
+        #preds += ["(>= %s 0)" % v, "(< %s %d)" % (v, m)]
+
+# Transition Δ: Q × Σ -> P(Q). For Σ = {a,b}, we assume this range:
+# transitions (0..; 1..2; 0..)
+extrafuns += ["(trans Int Int Int)"]
+# final states F \subset Q
+extrafuns += ["(final Int Bool)"]
+# Require a transition between each letter
+for i, word in enumerate(lang):
+    state_prev = "q0"
+    for j, letter in enumerate(word):
+        state_next = mks(i, j)
+        label = "ab".index(letter)
+        preds += ["(= (trans %s %d) %s)" % (state_prev, label, state_next)]
+        state_prev = state_next
+    preds += ["(final %s)" % state_prev]
+
+# "a" and "b" are not allowed to accept (length 1)
+#preds += ["(not (final (trans q0 %d)))" % label for label in range(2)]
+for i, word in enumerate(badlang):
+    state_prev = "q0"
+    move = "q0"
+    preconds = []
+    for j, letter in enumerate(word):
+        label = "ab".index(letter)
+        move = "(trans %s %d)" % (move, label)
+        # Ensure result is within range.
+        preconds += ["(>= %s 0)" % move, "(< %s %d)" % (move, m)]
+    preds += ["(=> (and %s) (not (final %s)))" % (" ".join(preconds), move)]
+    #preds += ["(not (final %s))" % move]
+    #valid = "(>= {move} 0) (< {move} {m})".format(**vars())
+    #preds += ["(=> (and %s) (not (final %s)))" % (valid, move)]
+
+# Try to fit any of the letter states with any state from Q
+for i, word in enumerate(lang):
+    for j, letter in enumerate(word):
+        alts = []
+        for qi in range(m):
+            state = "q%d" % qi
+            alts += ["(= %s %s)" % (state, mks(i, j))]
+        preds += ["(or %s)" % " ".join(alts)]
+
+# Begin generator
+s = """(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns (
+"""
+s += "\n".join("(%s Int)" % x for x in literals)
+s += "\n" + "\n".join(extrafuns)
+s += """
+)
+:formula (and
+"""
+s += "\n".join(preds)
+s += """
+))
+"""
+
+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/nfa/nfa-to-latex.py b/nfa/nfa-to-latex.py
new file mode 100755
index 0000000..fb3a540
--- /dev/null
+++ b/nfa/nfa-to-latex.py
@@ -0,0 +1,128 @@
+#!/usr/bin/env python
+# Usage:
+#   <z3-output.txt ./nfa-to-latex.py dot |
+#   dot -Txdot /dev/stdin | dot2tex -f tikz --figonly | sed s/ellipse/circle/ > some.tex
+import sys
+
+draw_dot = False if len(sys.argv) <= 1 else sys.argv[1] == "dot"
+
+in_block = None
+transitions = {}
+finals = []
+
+for line in sys.stdin:
+    line = line.strip()
+    if line == "unsat":
+        sys.exit('unsat!')
+    if line == "sat":
+        continue
+
+    # End of array
+    if line == "}":
+        in_block = None
+        continue
+
+    key, val = line.split(" -> ")
+    if key[0] in "sq":
+        # Skip the internal, non-optimized states that were used for tracking
+        # the letters. Skip also the state variables (just used for tracking).
+        continue
+
+    # Enter block
+    if key in ("trans", "final"):
+        in_block = key
+        continue
+
+    # Do not care
+    if key == "else":
+        continue
+
+    # Skip garbage like "(- 5905) 0 -> (- 2998)"
+    if "(-" in line:
+        continue
+
+    if in_block == "trans":
+        # Example input:
+        # trans -> {
+        #   0 0 -> 1
+        #   2 0 -> 1
+        #   else -> 1
+        # }
+        state_prev, letter_number = map(int, key.split())
+        state_next = int(val)
+        letter = "ab"[letter_number]
+        if (state_prev, state_next) not in transitions:
+            transitions[state_prev, state_next] = ""
+        transitions[state_prev, state_next] += letter
+    elif in_block == "final":
+        # Example input:
+        # final -> {
+        #   2 -> true
+        #   3 -> false
+        #   else -> false
+        # }
+        state = int(key)
+        is_final = val == "true"
+        while len(finals) <= state:
+            finals.append(None)
+        finals[state] = is_final
+    else:
+        raise RuntimeError("Unexpected reading state at line: %s" % line)
+
+m = len(finals)
+
+if draw_dot:
+    nodes = ""
+    edges = ""
+    # Nodes
+    for i in range(m):
+        line = "node [shape=%scircle];" % ("double" if finals[i] else "")
+        line += " q%d;" % i
+        nodes += "    %s\n" % line
+    # Transitions
+    for (state_prev, state_next), label in transitions.items():
+        line = "q%d -> q%d" % (state_prev, state_next)
+        line += " [label=\"%s\"];" % ", ".join(label)
+        edges += "    %s\n" % line
+    dot_source = """digraph nfa {{
+    rankdir=LR;
+    size="8,5";
+
+    # Incoming arrow
+    node [shape=point]; qi;
+    {nodes}
+
+    qi -> q0;
+    {edges}
+}}""".format(nodes=nodes, edges=edges)
+    print(dot_source)
+else:
+    # See http://tex.stackexchange.com/a/20786
+    # \usetikzlibrary{automata,positioning}
+    # \begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto]
+    # Draw nodes
+    for i in range(m):
+        line = r"\node[state"
+        if i == 0:
+            line += ",initial"
+        if finals[i]:
+            line += ",accepting"
+        line += "]"
+        line = line.ljust(24)
+        line += " (q%d)" % i
+        # XXX autopositioning is not working! Need things like "[right of=q0]"
+        # below/above left/right
+        if i > 0:
+            line += " [right of=q0]"
+        line = line.ljust(52)
+        line += " {$q_%s$}" % i
+        line += ";"
+        print(line)
+
+    print(r"\path[->]")
+
+    # Draw edges with labels
+    for (state_prev, state_next), label in transitions.items():
+        line = "(q%d) edge node {%s} (q%d)" % (state_prev, label, state_next)
+        print(line)
+    print(";")