1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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(";")
|
