From 283cfa7801e2f4d9882dbc462c2ec1133ca1515b Mon Sep 17 00:00:00 2001
From: Joeri Exelmans <joeri.exelmans@gmail.com>
Date: Thu, 21 Nov 2024 15:57:14 +0100
Subject: [PATCH] enhance petri net renderer

---
 concrete_syntax/graphviz/make_url.py   |  5 +++++
 examples/model_transformation/woods.py |  6 +++---
 examples/petrinet/renderer.py          | 26 ++++++++++++++++++++------
 3 files changed, 28 insertions(+), 9 deletions(-)

diff --git a/concrete_syntax/graphviz/make_url.py b/concrete_syntax/graphviz/make_url.py
index e9618aa..e8e338b 100644
--- a/concrete_syntax/graphviz/make_url.py
+++ b/concrete_syntax/graphviz/make_url.py
@@ -1,5 +1,6 @@
 from concrete_syntax.common import indent
 import urllib.parse
+import webbrowser
 
 def make_url(graphviz_txt: str, engine="dot") -> str:
 
@@ -10,3 +11,7 @@ def make_url(graphviz_txt: str, engine="dot") -> str:
 
     # Keeping this one here just in case:
     # return "https://dreampuf.github.io/GraphvizOnline/#"+urllib.parse.quote(graphviz)
+
+
+def show_graphviz(graphviz_txt: str, engine="dot"):
+    return webbrowser.open(make_url(graphviz_txt, engine))
diff --git a/examples/model_transformation/woods.py b/examples/model_transformation/woods.py
index 55c61a6..f321037 100644
--- a/examples/model_transformation/woods.py
+++ b/examples/model_transformation/woods.py
@@ -6,7 +6,7 @@ from uuid import UUID
 from services.scd import SCD
 from framework.conformance import Conformance
 from services.od import OD
-from transformation.matcher import mvs_adapter
+from transformation.matcher import match_od
 from transformation.ramify import ramify
 from transformation.cloner import clone_od
 from transformation import rewriter
@@ -188,7 +188,7 @@ def main():
         uml += plantuml.render_trace_conformance(state, dsl_m_id, dsl_mm_id)
 
         print("matching...")
-        generator = mvs_adapter.match_od(state, dsl_m_id, dsl_mm_id, lhs_id, ramified_mm_id)
+        generator = match_od(state, dsl_m_id, dsl_mm_id, lhs_id, ramified_mm_id)
         for match, color in zip(generator, ["red", "orange"]):
             print("\nMATCH:\n", match)
 
@@ -206,7 +206,7 @@ def main():
         # Render conformance
         uml += plantuml.render_trace_conformance(state, dsl_m_id, dsl_mm_id)
 
-        generator = mvs_adapter.match_od(state, dsl_m_id, dsl_mm_id, lhs_id, ramified_mm_id)
+        generator = match_od(state, dsl_m_id, dsl_mm_id, lhs_id, ramified_mm_id)
         for i, (match, color) in enumerate(zip(generator, ["red", "orange"])):
             uml += plantuml.render_trace_match(state, match, lhs_id, dsl_m_id, color)
 
diff --git a/examples/petrinet/renderer.py b/examples/petrinet/renderer.py
index 360626d..66eb630 100644
--- a/examples/petrinet/renderer.py
+++ b/examples/petrinet/renderer.py
@@ -1,5 +1,18 @@
 from api.od import ODAPI
-from concrete_syntax.graphviz.make_url import make_url
+from concrete_syntax.graphviz.make_url import show_graphviz
+
+try:
+    import graphviz
+    HAVE_GRAPHVIZ = True
+except ImportError:
+    HAVE_GRAPHVIZ = False
+
+def render_tokens(num_tokens: int):
+    if 0 <= num_tokens <= 3:
+        return '●'*num_tokens
+    if num_tokens == 4:
+        return '●●\\n●●'
+    return str(num_tokens)
 
 def render_petri_net(od: ODAPI):
     dot = ""
@@ -10,20 +23,21 @@ def render_petri_net(od: ODAPI):
     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];"
+    dot += "  node [shape=circle,fixedsize=true,label=\"\", height=.35,width=.35];"
     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 += f"  {place_name} [label=\"{place_name}\\n\\n{render_tokens(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"
+    dot += "  node [shape=rect,fixedsize=true,height=.3,width=.12,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 += f"  {transition_name} [label=\"{transition_name}\\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")
+    show_graphviz(dot, engine="circo")
+    return ""