add renderer for Port + Petri Net + traceability
This commit is contained in:
parent
e4c12b7349
commit
3ddfc96532
5 changed files with 163 additions and 37 deletions
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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 = ""
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
@ -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 = ""
|
||||
|
|
|
|||
68
examples/semantics/translational/renderer.py
Normal file
68
examples/semantics/translational/renderer.py
Normal file
|
|
@ -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)
|
||||
Loading…
Add table
Add a link
Reference in a new issue