diff options
Diffstat (limited to 'nfa/nfa-to-latex.py')
-rwxr-xr-x | nfa/nfa-to-latex.py | 128 |
1 files changed, 128 insertions, 0 deletions
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(";") |