diff --git a/api/od.py b/api/od.py index 85ea368..c23160d 100644 --- a/api/od.py +++ b/api/od.py @@ -104,6 +104,7 @@ class ODAPI: result.append(i) return result + # Returns list of tuples (name, obj) def get_all_instances(self, type_name: str, include_subtypes=True): if include_subtypes: all_types = self.cdapi.transitive_sub_types[type_name] diff --git a/concrete_syntax/graphviz/renderer.py b/concrete_syntax/graphviz/renderer.py index 4942af3..94ae54a 100644 --- a/concrete_syntax/graphviz/renderer.py +++ b/concrete_syntax/graphviz/renderer.py @@ -1,26 +1,45 @@ +import functools from uuid import UUID from services import scd, od from services.bottom.V0 import Bottom from concrete_syntax.common import display_value, display_name, indent +# Turn ModelVerse/muMLE ID into GraphViz ID +def make_graphviz_id(uuid, prefix="") -> str: + result = 'n'+(prefix+str(uuid).replace('-',''))[24:] # we assume that the first 24 characters are always zero... + return result -def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids=""): +# 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. +# Parameter 'only_render': if specified, only render instances of these types. E.g., ["Place", "connection"] +# Parameter 'type_to_style': mapping from type-name to graphviz style. E.g., { "generic_link": ",color=purple" } +def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids="", reify=False, only_render=None, type_to_style={}): bottom = Bottom(state) mm_scd = scd.SCD(mm, state) m_od = od.OD(mm, m, state) - def make_id(uuid) -> str: - return 'n'+(prefix_ids+str(uuid).replace('-',''))[24:] + make_id = functools.partial(make_graphviz_id, prefix=prefix_ids) output = "" # Render objects for class_name, class_node in mm_scd.get_classes().items(): + if only_render != None and class_name not in only_render: + continue + + output += f"\nsubgraph {class_name} {{" + if render_attributes: attributes = od.get_attributes(bottom, class_node) + + custom_style = type_to_style.get(class_name, "") + if custom_style == "": + output += f"\nnode [shape=rect]" + else: + output += f"\nnode [shape=rect,{custom_style}]" + 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}\", shape=rect] ;" + output += f"\n{make_id(obj_node)} [label=\"{display_name(obj_name)} : {class_name}\"] ;" #" {{" # if render_attributes: @@ -31,17 +50,42 @@ def render_object_diagram(state, m, mm, render_attributes=True, prefix_ids=""): # output += f"\n{attr_name} => {display_value(val, type_name)}" # output += '\n}' + output += '\n}' + output += '\n' # Render links for assoc_name, assoc_edge in mm_scd.get_associations().items(): + if only_render != None and assoc_name not in only_render: + continue + + output += f"\nsubgraph {assoc_name} {{" + + custom_style = type_to_style.get(assoc_name, "") + if custom_style != "": + output += f"\nedge [{custom_style}]" + if reify: + if custom_style != "": + # created nodes will be points of matching style: + output += f"\nnode [{custom_style},shape=point]" + else: + output += "\nnode [shape=point]" + for link_name, link_edge in m_od.get_objects(assoc_edge).items(): src_obj = bottom.read_edge_source(link_edge) tgt_obj = bottom.read_edge_target(link_edge) src_name = m_od.get_object_name(src_obj) tgt_name = m_od.get_object_name(tgt_obj) - output += f"\n{make_id(src_obj)} -> {make_id(tgt_obj)} [label=\"{display_name(link_name)}:{assoc_name}\"] ;" + if reify: + # intermediary node: + 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)} [xlabel=\"{display_name(link_name)} : {assoc_name}\"]" + else: + output += f"\n{make_id(src_obj)} -> {make_id(tgt_obj)} [label=\"{display_name(link_name)}:{assoc_name}\", {custom_style}] ;" + + output += '\n}' return output @@ -50,10 +94,8 @@ def render_trace_match(state, name_mapping: dict, pattern_m: UUID, host_m: UUID, class_type = od.get_scd_mm_class_node(bottom) attr_link_type = od.get_scd_mm_attributelink_node(bottom) - def make_pattern_id(uuid) -> str: - return 'n'+(prefix_pattern_ids+str(uuid).replace('-',''))[24:] - def make_host_id(uuid) -> str: - return 'n'+(prefix_host_ids+str(uuid).replace('-',''))[24:] + make_pattern_id = functools.partial(make_graphviz_id, prefix=prefix_pattern_ids) + make_host_id = functools.partial(make_graphviz_id, prefix=prefix_host_ids) output = "" diff --git a/examples/petrinet/renderer.py b/examples/petrinet/renderer.py index 25c1828..2d51fad 100644 --- a/examples/petrinet/renderer.py +++ b/examples/petrinet/renderer.py @@ -1,5 +1,6 @@ from api.od import ODAPI from concrete_syntax.graphviz.make_url import show_graphviz +from concrete_syntax.graphviz.renderer import make_graphviz_id try: import graphviz @@ -14,37 +15,46 @@ def render_tokens(num_tokens: int): return '●●\\n●●' return str(num_tokens) -def render_petri_net(od: ODAPI): +def render_petri_net_to_dot(od: ODAPI) -> str: 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=.35,width=.35];" - for _, place in od.get_all_instances("PNPlace"): - place_name = od.get_name(place) + dot += " node [fontname=Arial,fontsize=10,shape=circle,fixedsize=true,label=\"\", height=.35,width=.35];" + for place_name, place in od.get_all_instances("PNPlace"): + # place_name = od.get_name(place) try: place_state = od.get_source(od.get_incoming(place, "pn_of")[0]) num_tokens = od.get_slot_value(place_state, "numTokens") except IndexError: num_tokens = 0 - dot += f" {place_name} [label=\"{place_name}\\n\\n{render_tokens(num_tokens)}\\n\\n­\"];\n" + print("PLACE", place) + dot += f" {make_graphviz_id(place)} [label=\"{place_name}\\n\\n{render_tokens(num_tokens)}\\n\\n­\"];\n" dot += "}\n" - dot += "subgraph transitions {" - 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("PNTransition"): - dot += f" {transition_name} [label=\"{transition_name}\\n\\n\\n­\"];\n" + dot += "subgraph transitions {\n" + dot += " edge [arrowhead=normal];\n" + dot += " node [fontname=Arial,fontsize=10,shape=rect,fixedsize=true,height=.3,width=.12,style=filled,fillcolor=black,color=white];\n" + for transition_name, transition in od.get_all_instances("PNTransition"): + dot += f" {make_graphviz_id(transition)} [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};" + src = od.get_source(arc) + tgt = od.get_target(arc) + # src_name = od.get_name(od.get_source(arc)) + # tgt_name = od.get_name(od.get_target(arc)) + dot += f"{make_graphviz_id(src)} -> {make_graphviz_id(tgt)};" for _, inhib_arc in od.get_all_instances("inh_arc"): - src_name = od.get_name(od.get_source(inhib_arc)) - tgt_name = od.get_name(od.get_target(inhib_arc)) - dot += f"{src_name} -> {tgt_name} [arrowhead=odot];\n" - show_graphviz(dot, engine="neato") - return "" + src = od.get_source(inhib_arc) + tgt = od.get_target(inhib_arc) + dot += f"{make_graphviz_id(src)} -> {make_graphviz_id(tgt)} [arrowhead=odot];\n" + return dot + +# deprecated +def render_petri_net(od: ODAPI, engine="neato"): + show_graphviz(render_petri_net_to_dot(od), engine=engine) + +# use this instead: +def show_petri_net(od: ODAPI, engine="neato"): + show_graphviz(render_petri_net_to_dot(od), engine=engine) \ No newline at end of file diff --git a/examples/semantics/operational/port/renderer.py b/examples/semantics/operational/port/renderer.py index d0518e6..63bebb3 100644 --- a/examples/semantics/operational/port/renderer.py +++ b/examples/semantics/operational/port/renderer.py @@ -2,12 +2,14 @@ from concrete_syntax.common import indent from concrete_syntax.graphviz.make_url import make_url from examples.semantics.operational.port.helpers import design_to_state, state_to_design, get_time, get_num_ships -def render_port_graphviz(od): +def render_port_to_dot(od, + make_id=lambda name,obj: name # by default, we just use the object name for the graphviz node name +): txt = "" def render_place(place): name = od.get_name(place) - return f'"{name}" [ label = "{name}\\n ships = {get_num_ships(od, place)}", style = filled, fillcolor = lightblue ]\n' + return f'"{make_id(name,place)}" [ label = "{name}\\n ships = {get_num_ships(od, place)}", style = filled, fillcolor = lightblue ]\n' for _, cap in od.get_all_instances("CapacityConstraint", include_subtypes=False): name = od.get_name(cap) @@ -26,10 +28,10 @@ def render_port_graphviz(od): for _, berth_state in od.get_all_instances("BerthState", include_subtypes=False): berth = state_to_design(od, berth_state) name = od.get_name(berth) - txt += f'"{name}" [ label = "{name}\\n numShips = {get_num_ships(od, berth)}\\n status = {od.get_slot_value(berth_state, "status")}", fillcolor = yellow, style = filled]\n' + txt += f'"{make_id(name,berth)}" [ label = "{name}\\n numShips = {get_num_ships(od, berth)}\\n status = {od.get_slot_value(berth_state, "status")}", fillcolor = yellow, style = filled]\n' for _, gen in od.get_all_instances("Generator", include_subtypes=False): - txt += f'"{od.get_name(gen)}" [ label = "+", shape = diamond, fillcolor = green, fontsize = 30, style = filled ]\n' + txt += f'"{make_id(od.get_name(gen),gen)}" [ label = "+", shape = diamond, fillcolor = green, fontsize = 30, style = filled ]\n' for _, conn in od.get_all_instances("connection"): src = od.get_source(conn) @@ -37,23 +39,26 @@ def render_port_graphviz(od): moved = od.get_slot_value(design_to_state(od, conn), "moved") src_name = od.get_name(src) tgt_name = od.get_name(tgt) - txt += f"{src_name} -> {tgt_name} [color=deepskyblue3, penwidth={1 if moved else 2}];\n" + txt += f"{make_id(src_name,src)} -> {make_id(tgt_name,tgt)} [color=deepskyblue3, penwidth={1 if moved else 2}];\n" for _, workers in od.get_all_instances("WorkerSet"): already_have = [] name = od.get_name(workers) num_workers = od.get_slot_value(workers, "numWorkers") - txt += f'{name} [label="{num_workers} worker(s)", shape=parallelogram, fillcolor=chocolate, style=filled];\n' + txt += f'{make_id(name,workers)} [label="{num_workers} worker(s)", shape=parallelogram, fillcolor=chocolate, style=filled];\n' for lnk in od.get_outgoing(design_to_state(od, workers), "isOperating"): berth = od.get_target(lnk) already_have.append(berth) - txt += f"{name} -> {od.get_name(berth)} [arrowhead=none, color=chocolate];\n" + txt += f"{make_id(name,workers)} -> {make_id(od.get_name(berth),berth)} [arrowhead=none, color=chocolate];\n" for lnk in od.get_outgoing(workers, "canOperate"): berth = od.get_target(lnk) if berth not in already_have: - txt += f"{name} -> {od.get_name(berth)} [style=dotted, arrowhead=none, color=chocolate];\n" + txt += f"{make_id(name,workers)} -> {make_id(od.get_name(berth),berth)} [style=dotted, arrowhead=none, color=chocolate];\n" - return make_url(txt) + return txt + +def render_port_graphviz(od): + return make_url(render_port_to_dot(od)) def render_port_textual(od): txt = "" diff --git a/examples/semantics/translational/renderer.py b/examples/semantics/translational/renderer.py new file mode 100644 index 0000000..c520224 --- /dev/null +++ b/examples/semantics/translational/renderer.py @@ -0,0 +1,68 @@ +from api.od import ODAPI +from concrete_syntax.graphviz.renderer import render_object_diagram, make_graphviz_id +from concrete_syntax.graphviz.make_url import show_graphviz +from examples.petrinet.renderer import render_petri_net_to_dot +from examples.semantics.operational.port.renderer import render_port_to_dot + +# COLORS +PLACE_BG = "#DAE8FC" # fill color +PLACE_FG = "#6C8EBF" # font, line, arrow +BERTH_BG = "#FFF2CC" +BERTH_FG = "#D6B656" +CAPACITY_BG = "#F5F5F5" +CAPACITY_FG = "#666666" +WORKER_BG = "#D5E8D4" +WORKER_FG = "#82B366" +GENERATOR_BG = "#FFE6CC" +GENERATOR_FG = "#D79B00" +CLOCK_BG = "black" +CLOCK_FG = "white" + +def graphviz_style_fg_bg(fg, bg): + return f"style=filled,fillcolor=\"{bg}\",color=\"{fg}\",fontcolor=\"{fg}\"" + +def render_port(state, m, mm): + dot = render_object_diagram(state, m, mm, + reify=True, + only_render=[ + # Only render these types + "Place", "Berth", "CapacityConstraint", "WorkerSet", "Generator", "Clock", + "connection", "capacityOf", "canOperate", "generic_link", + # 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. + ], + type_to_style={ + "Place": graphviz_style_fg_bg(PLACE_FG, PLACE_BG), + "Berth": graphviz_style_fg_bg(BERTH_FG, BERTH_BG), + "CapacityConstraint": graphviz_style_fg_bg(CAPACITY_FG, CAPACITY_BG), + "WorkerSet": "shape=oval,"+graphviz_style_fg_bg(WORKER_FG, WORKER_BG), + "Generator": "shape=parallelogram,"+graphviz_style_fg_bg(GENERATOR_FG, GENERATOR_BG), + "Clock": graphviz_style_fg_bg(CLOCK_FG, CLOCK_BG), + + # same blue as Place, thick line: + "connection": f"color=\"{PLACE_FG}\",fontcolor=\"{PLACE_FG}\",penwidth=2.0", + + # same grey as CapacityConstraint + "capacityOf": f"color=\"{CAPACITY_FG}\",fontcolor=\"{CAPACITY_FG}\"", + + # same green as WorkerSet + "canOperate": f"color=\"{WORKER_FG}\",fontcolor=\"{WORKER_FG}\"", + + # purple line + "generic_link": "color=purple,fontcolor=purple,arrowhead=onormal", + } + ) + return dot + +def render_port_and_petri_net(state, m, mm): + od = ODAPI(state, m, mm) + dot = "" + dot += "// petri net:\n" + dot += render_petri_net_to_dot(od) + dot += "\n// the rest:\n" + dot += render_port(state, m, mm) + return dot + + +def show_port_and_petri_net(state, m, mm, engine="dot"): + show_graphviz(render_port_and_petri_net(state, m, mm), engine=engine)