improve (Port + Petri Net + traceability)-renderer

This commit is contained in:
Joeri Exelmans 2024-12-09 17:43:01 +01:00
parent bd1588d809
commit fd8bc3bc40
2 changed files with 44 additions and 8 deletions

View file

@ -1,5 +1,6 @@
import functools import functools
from uuid import UUID from uuid import UUID
from api.od import ODAPI
from services import scd, od from services import scd, od
from services.bottom.V0 import Bottom from services.bottom.V0 import Bottom
from concrete_syntax.common import display_value, display_name, indent from concrete_syntax.common import display_value, display_name, indent
@ -9,13 +10,18 @@ def make_graphviz_id(uuid, prefix="") -> str:
result = 'n'+(prefix+str(uuid).replace('-',''))[24:] # we assume that the first 24 characters are always zero... result = 'n'+(prefix+str(uuid).replace('-',''))[24:] # we assume that the first 24 characters are always zero...
return result return result
# Parameter 'reify': If true, will create a node in the middle of every link. This allows links to be the src/tgt of other links (which muMLE supports), at the cost of a larger diagram. def render_object_diagram(state, m, mm,
# Parameter 'only_render': if specified, only render instances of these types. E.g., ["Place", "connection"] render_attributes=True, # doesn't do anything (yet)
# Parameter 'type_to_style': mapping from type-name to graphviz style. E.g., { "generic_link": ",color=purple" } prefix_ids="",
def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", reify=False, only_render=None, type_to_style={}): reify=False, # If true, will create a node in the middle of every link. This allows links to be the src/tgt of other links (which muMLE supports), but will result in a larger diagram.
only_render=None, # List of type names or None. If specified, only render instances of these types. E.g., ["Place", "connection"]
type_to_style={}, # Dictionary. Mapping from type-name to graphviz style. E.g., { "generic_link": ",color=purple" }
type_to_label={}, # Dictionary. Mapping from type-name to callback for custom label creation.
):
bottom = Bottom(state) bottom = Bottom(state)
mm_scd = scd.SCD(mm, state) mm_scd = scd.SCD(mm, state)
m_od = od.OD(mm, m, state) m_od = od.OD(mm, m, state)
odapi = ODAPI(state, m, mm)
make_id = functools.partial(make_graphviz_id, prefix=prefix_ids) make_id = functools.partial(make_graphviz_id, prefix=prefix_ids)
@ -26,6 +32,10 @@ def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", r
if only_render != None and class_name not in only_render: if only_render != None and class_name not in only_render:
continue continue
make_label = type_to_label.get(class_name,
# default, if not found:
lambda obj_name, obj, odapi: f"{display_name(obj_name)} : {class_name}")
output += f"\nsubgraph {class_name} {{" output += f"\nsubgraph {class_name} {{"
if render_attributes: if render_attributes:
@ -39,7 +49,7 @@ def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", r
output += f"\nnode [shape=rect,{custom_style}]" output += f"\nnode [shape=rect,{custom_style}]"
for obj_name, obj_node in m_od.get_objects(class_node).items(): for obj_name, obj_node in m_od.get_objects(class_node).items():
output += f"\n{make_id(obj_node)} [label=\"{display_name(obj_name)} : {class_name}\"] ;" output += f"\n{make_id(obj_node)} [label=\"{make_label(obj_name, obj_node, odapi)}\"] ;"
#" {{" #" {{"
# if render_attributes: # if render_attributes:
@ -59,6 +69,10 @@ def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", r
if only_render != None and assoc_name not in only_render: if only_render != None and assoc_name not in only_render:
continue continue
make_label = type_to_label.get(assoc_name,
# default, if not found:
lambda lnk_name, lnk, odapi: f"{display_name(lnk_name)} : {assoc_name}")
output += f"\nsubgraph {assoc_name} {{" output += f"\nsubgraph {assoc_name} {{"
custom_style = type_to_style.get(assoc_name, "") custom_style = type_to_style.get(assoc_name, "")
@ -81,9 +95,9 @@ def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", r
# intermediary node: # intermediary node:
output += f"\n{make_id(src_obj)} -> {make_id(link_edge)} [arrowhead=none]" output += f"\n{make_id(src_obj)} -> {make_id(link_edge)} [arrowhead=none]"
output += f"\n{make_id(link_edge)} -> {make_id(tgt_obj)}" output += f"\n{make_id(link_edge)} -> {make_id(tgt_obj)}"
output += f"\n{make_id(link_edge)} [xlabel=\"{display_name(link_name)} : {assoc_name}\"]" output += f"\n{make_id(link_edge)} [xlabel=\"{make_label(link_name, link_edge, odapi)}\"]"
else: else:
output += f"\n{make_id(src_obj)} -> {make_id(tgt_obj)} [label=\"{display_name(link_name)}:{assoc_name}\", {custom_style}] ;" output += f"\n{make_id(src_obj)} -> {make_id(tgt_obj)} [label=\"{make_label(link_name, link_edge, odapi)}\", {custom_style}] ;"
output += '\n}' output += '\n}'

View file

@ -3,6 +3,7 @@ from concrete_syntax.graphviz.renderer import render_object_diagram, make_graphv
from concrete_syntax.graphviz.make_url import show_graphviz from concrete_syntax.graphviz.make_url import show_graphviz
from examples.petrinet.renderer import render_petri_net_to_dot from examples.petrinet.renderer import render_petri_net_to_dot
from examples.semantics.operational.port.renderer import render_port_to_dot from examples.semantics.operational.port.renderer import render_port_to_dot
from examples.semantics.operational.port import helpers
# COLORS # COLORS
PLACE_BG = "#DAE8FC" # fill color PLACE_BG = "#DAE8FC" # fill color
@ -31,6 +32,7 @@ def render_port(state, m, mm):
# Petri Net types not included (they are already rendered by other function) # Petri Net types not included (they are already rendered by other function)
# Port-State-types not included to avoid cluttering the diagram, but if you need them, feel free to add them. # Port-State-types not included to avoid cluttering the diagram, but if you need them, feel free to add them.
], ],
# We can style nodes/edges according to their type:
type_to_style={ type_to_style={
"Place": graphviz_style_fg_bg(PLACE_FG, PLACE_BG), "Place": graphviz_style_fg_bg(PLACE_FG, PLACE_BG),
"Berth": graphviz_style_fg_bg(BERTH_FG, BERTH_BG), "Berth": graphviz_style_fg_bg(BERTH_FG, BERTH_BG),
@ -50,7 +52,27 @@ def render_port(state, m, mm):
# purple line # purple line
"generic_link": "color=purple,fontcolor=purple,arrowhead=onormal", "generic_link": "color=purple,fontcolor=purple,arrowhead=onormal",
} },
# We have control over the node/edge labels that are rendered:
type_to_label={
"CapacityConstraint": lambda capconstr_name, capconstr, odapi: f"{capconstr_name}\\nshipCapacity={odapi.get_slot_value(capconstr, "shipCapacity")}",
"Place": lambda place_name, place, odapi: f"{place_name}\\nnumShips={helpers.get_num_ships(odapi, place)}",
"Berth": lambda berth_name, berth, odapi: f"{berth_name}\\nnumShips={helpers.get_num_ships(odapi, berth)}\\nstatus={odapi.get_slot_value(helpers.design_to_state(odapi, berth), "status")}",
"Clock": lambda _, clock, odapi: f"Clock\\ntime={odapi.get_slot_value(clock, "time")}",
"connection": lambda conn_name, conn, odapi: f"{conn_name}\\nmoved={odapi.get_slot_value(helpers.design_to_state(odapi, conn), "moved")}",
# hide generic link labels
"generic_link": lambda lnk_name, lnk, odapi: "",
"WorkerSet": lambda ws_name, ws, odapi: f"{ws_name}\\nnumWorkers={odapi.get_slot_value(ws, "numWorkers")}",
# hide the type (it's already clear enough)
"Generator": lambda gen_name, gen, odapi: gen_name,
},
) )
return dot return dot