From 3aec288e372f8bce6695c4ef2defc4e35913b6cc Mon Sep 17 00:00:00 2001
From: Joeri Exelmans <joeri.exelmans@gmail.com>
Date: Thu, 21 Nov 2024 14:58:32 +0100
Subject: [PATCH] add petri net renderer (graphviz-based)

---
 concrete_syntax/graphviz/make_url.py |  4 ++--
 examples/petrinet/renderer.py        | 29 ++++++++++++++++++++++++++++
 examples/petrinet/runner.py          |  2 ++
 3 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 examples/petrinet/renderer.py

diff --git a/concrete_syntax/graphviz/make_url.py b/concrete_syntax/graphviz/make_url.py
index 9630c67..e9618aa 100644
--- a/concrete_syntax/graphviz/make_url.py
+++ b/concrete_syntax/graphviz/make_url.py
@@ -1,12 +1,12 @@
 from concrete_syntax.common import indent
 import urllib.parse
 
-def make_url(graphviz_txt: str) -> str:
+def make_url(graphviz_txt: str, engine="dot") -> str:
 
     as_digraph = f"digraph {{\n{indent(graphviz_txt, 2)}\n}}"
 
     # This one seems much faster:
-    return "https://edotor.net/?engine=dot#"+urllib.parse.quote(as_digraph)
+    return f"https://edotor.net/?engine={engine}#{urllib.parse.quote(as_digraph)}"
 
     # Keeping this one here just in case:
     # return "https://dreampuf.github.io/GraphvizOnline/#"+urllib.parse.quote(graphviz)
diff --git a/examples/petrinet/renderer.py b/examples/petrinet/renderer.py
new file mode 100644
index 0000000..360626d
--- /dev/null
+++ b/examples/petrinet/renderer.py
@@ -0,0 +1,29 @@
+from api.od import ODAPI
+from concrete_syntax.graphviz.make_url import make_url
+
+def render_petri_net(od: ODAPI):
+    dot = ""
+    dot += "rankdir=LR;"
+    dot += "center=true;"
+    dot += "margin=1;"
+    dot += "nodesep=1;"
+    dot += "edge [arrowhead=vee];"
+    dot += "node[fontname=Arial,fontsize=10];\n"
+    dot += "subgraph places {"
+    dot += "  node [shape=circle,fixedsize=true,label=\"\", height=.3,width=.3];"
+    for _, place_state in od.get_all_instances("PlaceState"):
+        place = od.get_target(od.get_outgoing(place_state, "of")[0])
+        place_name = od.get_name(place)
+        num_tokens = od.get_slot_value(place_state, "numTokens")
+        dot += f"  {place_name} [label=\"{place_name}\\n\\n{'●'*num_tokens}\\n\\n­\"];\n"
+    dot += "}\n"
+    dot += "subgraph transitions {"
+    dot += "  node [shape=rect,fixedsize=true,height=.4,width=.15,style=filled,fillcolor=black,color=white];\n"
+    for transition_name, _ in od.get_all_instances("Transition"):
+        dot += f"  {transition_name} [label=\"{transition_name}\\n\\n\\n\\n­\"];\n"
+    dot += "}\n"
+    for _, arc in od.get_all_instances("arc"):
+        src_name = od.get_name(od.get_source(arc))
+        tgt_name = od.get_name(od.get_target(arc))
+        dot += f"{src_name} -> {tgt_name};"
+    return make_url(dot, engine="circo")
diff --git a/examples/petrinet/runner.py b/examples/petrinet/runner.py
index ece1e9e..e913271 100644
--- a/examples/petrinet/runner.py
+++ b/examples/petrinet/runner.py
@@ -5,6 +5,7 @@ from util import loader
 from transformation.rule import RuleMatcherRewriter, ActionGenerator
 from transformation.ramify import ramify
 from examples.semantics.operational import simulator
+from examples.petrinet.renderer import render_petri_net
 
 
 if __name__ == "__main__":
@@ -49,6 +50,7 @@ if __name__ == "__main__":
         action_generator=action_generator,
         decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False),
         # decision_maker=simulator.RandomDecisionMaker(seed=0),
+        renderer=render_petri_net,
     )
 
     sim.run(ODAPI(state, m_rt_initial, mm_rt))
\ No newline at end of file