From 995b06c4e9617c44429cc4d0ae3d0518384d6471 Mon Sep 17 00:00:00 2001 From: Peter Wu Date: Mon, 16 Jan 2017 04:51:23 +0100 Subject: 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. --- nfa/generate-nfa.py | 118 ++++++++++++++++++++++++++++++++++++++++++++++++ nfa/nfa-to-latex.py | 128 ++++++++++++++++++++++++++++++++++++++++++++++++++++ part2.tex | 43 ++++++++++++++++++ 3 files changed, 289 insertions(+) create mode 100755 nfa/generate-nfa.py create mode 100755 nfa/nfa-to-latex.py 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: +# 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 -- cgit v1.2.1