vm.fail
Alpha equivalence checker for arbitrary lambda terms
1#!/usr/bin/env python3
2import argparse
3import json
4import shutil
5import subprocess
6import sys
7from pathlib import Path
8
9
10def q(s):
11 return json.dumps(str(s), ensure_ascii=False)
12
13
14def attrs(items):
15 xs = [(k, v) for k, v in items if v is not None]
16 if not xs:
17 return ""
18 return " [" + ", ".join(f"{k}={q(v)}" for k, v in xs) + "]"
19
20
21def load(path):
22 with open(path, "r", encoding="utf-8") as f:
23 spec = json.load(f)
24 if "states" not in spec:
25 raise ValueError("missing required field: states")
26 if "transitions" not in spec:
27 raise ValueError("missing required field: transitions")
28 return spec
29
30
31def transition_label(t):
32 if "label" in t:
33 return t["label"]
34 read = t.get("read")
35 write = t.get("write")
36 action = t.get("action")
37 parts = []
38 if read is not None:
39 parts.append(str(read))
40 if write is not None:
41 parts.append("→ " + str(write))
42 if action is not None:
43 parts.append(str(action))
44 return " ".join(parts)
45
46
47def to_dot(spec):
48 name = spec.get("name", "automaton")
49 rankdir = spec.get("rankdir", "LR")
50 accepting = set(spec.get("accepting", []))
51 start = spec.get("start")
52
53 lines = [
54 f"digraph {q(name)} {{",
55 f" rankdir={q(rankdir)};",
56 ' graph [pad="0.25", nodesep="0.7", ranksep="0.9"];',
57 ' node [shape=circle, fontname="Times New Roman", fontsize=16];',
58 ' edge [fontname="Times New Roman", fontsize=14, arrowsize=0.8];',
59 ]
60
61 if start is not None:
62 lines.append(' "__start" [shape=point, label="", width=0.08];')
63
64 for state in spec["states"]:
65 if isinstance(state, str):
66 sid = state
67 label = state
68 final = sid in accepting
69 else:
70 sid = state["id"]
71 label = state.get("label", sid)
72 final = state.get("accepting", sid in accepting)
73 shape = "doublecircle" if final else "circle"
74 lines.append(f" {q(sid)}{attrs([('label', label), ('shape', shape)])};")
75
76 if start is not None:
77 lines.append(f" \"__start\" -> {q(start)}{attrs([('label', spec.get('start_label', 'start'))])};")
78
79 for t in spec["transitions"]:
80 src = t["from"]
81 dst = t["to"]
82 label = transition_label(t)
83 lines.append(
84 f" {q(src)} -> {q(dst)}"
85 f"{attrs([('label', label), ('xlabel', t.get('xlabel'))])};"
86 )
87
88 lines.append("}")
89 return "\n".join(lines) + "\n"
90
91
92def render(dot_path, out_path, fmt):
93 dot = shutil.which("dot")
94 if dot is None:
95 raise RuntimeError("graphviz 'dot' executable not found")
96 subprocess.run([dot, f"-T{fmt}", str(dot_path), "-o", str(out_path)], check=True)
97
98
99def main(argv):
100 parser = argparse.ArgumentParser(
101 description="Render finite automata/transducers from JSON using Graphviz."
102 )
103 parser.add_argument("input", help="automaton JSON file")
104 parser.add_argument("-o", "--output", help="output image path; extension selects format")
105 parser.add_argument("--dot", help="write DOT to this path")
106 parser.add_argument(
107 "--format",
108 choices=["svg", "png", "pdf", "dot"],
109 help="render format; defaults to output extension, or dot when no output is given",
110 )
111 args = parser.parse_args(argv)
112
113 spec = load(args.input)
114 dot_text = to_dot(spec)
115 fmt = args.format
116 if fmt is None:
117 fmt = Path(args.output).suffix.lstrip(".") if args.output else "dot"
118 if fmt == "":
119 raise ValueError("cannot infer output format from path without extension")
120
121 dot_path = Path(args.dot) if args.dot else None
122 if dot_path is not None:
123 dot_path.write_text(dot_text, encoding="utf-8")
124
125 if fmt == "dot" and args.output is None:
126 sys.stdout.write(dot_text)
127 return 0
128
129 if args.output is None:
130 raise ValueError("rendering requires --output unless --format dot is used")
131
132 out_path = Path(args.output)
133 if fmt == "dot":
134 out_path.write_text(dot_text, encoding="utf-8")
135 return 0
136
137 tmp_dot = dot_path if dot_path is not None else out_path.with_suffix(out_path.suffix + ".dot")
138 if dot_path is None:
139 tmp_dot.write_text(dot_text, encoding="utf-8")
140 try:
141 render(tmp_dot, out_path, fmt)
142 finally:
143 if dot_path is None:
144 tmp_dot.unlink(missing_ok=True)
145 return 0
146
147
148if __name__ == "__main__":
149 raise SystemExit(main(sys.argv[1:]))