#!/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(";")