enhance petri net renderer

This commit is contained in:
Joeri Exelmans 2024-11-21 15:57:14 +01:00
parent 3aec288e37
commit 283cfa7801
3 changed files with 28 additions and 9 deletions

View file

@ -1,5 +1,6 @@
from concrete_syntax.common import indent from concrete_syntax.common import indent
import urllib.parse import urllib.parse
import webbrowser
def make_url(graphviz_txt: str, engine="dot") -> str: 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: # Keeping this one here just in case:
# return "https://dreampuf.github.io/GraphvizOnline/#"+urllib.parse.quote(graphviz) # 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))

View file

@ -6,7 +6,7 @@ from uuid import UUID
from services.scd import SCD from services.scd import SCD
from framework.conformance import Conformance from framework.conformance import Conformance
from services.od import OD from services.od import OD
from transformation.matcher import mvs_adapter from transformation.matcher import match_od
from transformation.ramify import ramify from transformation.ramify import ramify
from transformation.cloner import clone_od from transformation.cloner import clone_od
from transformation import rewriter from transformation import rewriter
@ -188,7 +188,7 @@ def main():
uml += plantuml.render_trace_conformance(state, dsl_m_id, dsl_mm_id) uml += plantuml.render_trace_conformance(state, dsl_m_id, dsl_mm_id)
print("matching...") 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"]): for match, color in zip(generator, ["red", "orange"]):
print("\nMATCH:\n", match) print("\nMATCH:\n", match)
@ -206,7 +206,7 @@ def main():
# Render conformance # Render conformance
uml += plantuml.render_trace_conformance(state, dsl_m_id, dsl_mm_id) 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"])): for i, (match, color) in enumerate(zip(generator, ["red", "orange"])):
uml += plantuml.render_trace_match(state, match, lhs_id, dsl_m_id, color) uml += plantuml.render_trace_match(state, match, lhs_id, dsl_m_id, color)

View file

@ -1,5 +1,18 @@
from api.od import ODAPI 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): def render_petri_net(od: ODAPI):
dot = "" dot = ""
@ -10,20 +23,21 @@ def render_petri_net(od: ODAPI):
dot += "edge [arrowhead=vee];" dot += "edge [arrowhead=vee];"
dot += "node[fontname=Arial,fontsize=10];\n" dot += "node[fontname=Arial,fontsize=10];\n"
dot += "subgraph places {" 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"): for _, place_state in od.get_all_instances("PlaceState"):
place = od.get_target(od.get_outgoing(place_state, "of")[0]) place = od.get_target(od.get_outgoing(place_state, "of")[0])
place_name = od.get_name(place) place_name = od.get_name(place)
num_tokens = od.get_slot_value(place_state, "numTokens") 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 += "}\n"
dot += "subgraph transitions {" 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"): 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" dot += "}\n"
for _, arc in od.get_all_instances("arc"): for _, arc in od.get_all_instances("arc"):
src_name = od.get_name(od.get_source(arc)) src_name = od.get_name(od.get_source(arc))
tgt_name = od.get_name(od.get_target(arc)) tgt_name = od.get_name(od.get_target(arc))
dot += f"{src_name} -> {tgt_name};" dot += f"{src_name} -> {tgt_name};"
return make_url(dot, engine="circo") show_graphviz(dot, engine="circo")
return ""