summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Wu <peter@lekensteyn.nl>2017-01-16 04:51:23 +0100
committerPeter Wu <peter@lekensteyn.nl>2017-01-16 04:51:23 +0100
commit995b06c4e9617c44429cc4d0ae3d0518384d6471 (patch)
treeb92f687f4f84116afb3ae8ebb7352f9189578edd
parent66dad01dd33494a885b5577d92dc4bc619c36cf9 (diff)
download2IMF25-AR-995b06c4e9617c44429cc4d0ae3d0518384d6471.tar.gz
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.
-rwxr-xr-xnfa/generate-nfa.py118
-rwxr-xr-xnfa/nfa-to-latex.py128
-rw-r--r--part2.tex43
3 files changed, 289 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(";")
diff --git a/part2.tex b/part2.tex
index c30489c..9d925ed 100644
--- a/part2.tex
+++ b/part2.tex
@@ -8,6 +8,7 @@
\usepackage[table]{xcolor}
\usepackage{listings}
\usepackage{tikz}
+\usetikzlibrary{automata,positioning}
\usepackage{hyperref}
\usepackage{float}
\usepackage{enumitem}
@@ -290,6 +291,48 @@ $aba$, $baa$, $abab$, $babb$ and $bbba$.
\subsection*{Solution:}
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}[>=latex,line join=bevel,scale=.8]
+%%
+\node (q1) at (349.84bp,107.75bp) [draw,circle] {q1};
+ \node (q0) at (63.348bp,142.75bp) [draw,circle] {q0};
+ \node (q3) at (250.34bp,26.748bp) [draw,circle, double] {q3};
+ \node (q2) at (349.84bp,192.75bp) [draw,circle, double] {q2};
+ \node (q5) at (449.33bp,192.75bp) [draw,circle, double] {q5};
+ \node (q4) at (154.84bp,196.75bp) [draw,circle] {q4};
+ \node (q7) at (250.34bp,196.75bp) [draw,circle] {q7};
+ \node (q6) at (154.84bp,111.75bp) [draw,circle] {q6};
+ \node (qi) at (1.8bp,142.75bp) [draw,circle, fill] {};
+ \draw [->] (q4) ..controls (187.8bp,216.1bp) and (206.11bp,224.89bp) .. (223.59bp,228.75bp) .. controls (289.99bp,243.41bp) and (310.37bp,244.23bp) .. (376.58bp,228.75bp) .. controls (390.8bp,225.42bp) and (405.42bp,218.89bp) .. (q5);
+ \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+ \pgfsetstrokecolor{strokecol}
+ \draw (300.09bp,247.25bp) node {a};
+ \draw [->] (q6) ..controls (183.11bp,118.1bp) and (189.56bp,119.16bp) .. (195.59bp,119.75bp) .. controls (220.94bp,122.21bp) and (121.7bp,141.89bp) .. (305.09bp,118.75bp) .. controls (309.28bp,118.22bp) and (313.66bp,117.44bp) .. (q1);
+ \draw (250.34bp,136.25bp) node {a};
+ \draw [->] (q3) ..controls (283.88bp,45.478bp) and (295.45bp,52.911bp) .. (305.09bp,60.748bp) .. controls (313.05bp,67.222bp) and (321.01bp,75.037bp) .. (q1);
+ \draw (300.09bp,68.248bp) node {b};
+ \draw [->] (q4) ..controls (189.69bp,196.75bp) and (204.15bp,196.75bp) .. (q7);
+ \draw (200.59bp,204.25bp) node {b};
+ \draw [->] (q0) ..controls (96.456bp,131.53bp) and (110.68bp,126.71bp) .. (q6);
+ \draw (109.1bp,136.25bp) node {b};
+ \draw [->] (q1) ..controls (301.72bp,103.92bp) and (259.71bp,101.65bp) .. (223.59bp,103.75bp) .. controls (211.74bp,104.44bp) and (198.81bp,105.78bp) .. (q6);
+ \draw (250.34bp,111.25bp) node {b};
+ \draw [->] (q7) ..controls (285.1bp,195.35bp) and (299.58bp,194.77bp) .. (q2);
+ \draw (300.09bp,203.25bp) node {a};
+ \draw [->] (q0) ..controls (95.791bp,161.9bp) and (112.28bp,171.63bp) .. (q4);
+ \draw (109.1bp,179.25bp) node {a};
+ \draw [->] (q1) ..controls (382.04bp,135.26bp) and (403.75bp,153.81bp) .. (q5);
+ \draw (399.58bp,161.25bp) node {a};
+ \draw [->] (qi) ..controls (8.2235bp,142.75bp) and (19.002bp,142.75bp) .. (q0);
+ \draw [->] (q2) ..controls (387.71bp,192.75bp) and (400.54bp,192.75bp) .. (q5);
+ \draw (399.58bp,200.25bp) node {b};
+ \draw [->] (q6) ..controls (175.2bp,82.337bp) and (185.08bp,70.08bp) .. (195.59bp,60.748bp) .. controls (202.27bp,54.82bp) and (210.1bp,49.285bp) .. (q3);
+ \draw (200.59bp,68.248bp) node {b};
+%
+\end{tikzpicture}
+\end{figure}
+
\section*{Problem: }
The goal of this problem is to exploit the power of the recommended tools rather