Example of converting Alloy's XML output to GraphViz with clusters (containers/groups) and tables.

alloy_xml_to_gv.py

# Alloy forum post: https://alloytools.discourse.group/t/is-it-possible-to-group-container-nodes-in-the-visualizer
#
# I usually paste the GraphViz to sketchviz.com. The details are hard-coded
# to the specifics of the model, but shared in the hope that the overall
# structure of the parsing and printing is potentially useful.
#
# See example diagram at:
#
# https://twitter.com/typesanitizer/status/1551575106194878464?s=20
#
# Couple of workflow tips:
# 1. Use 'entr' (https://github.com/clibs/entr) to re-run the script
#    if you change the script or the input XML file.
# 2. Use 'pbcopy' to automate copying to the clipboard so that you
#    can paste it into sketchviz.com (of course, you can use some
#    other graphviz visualizer too)

import xml.etree.ElementTree as ET

CRATE_COLOR = "#A35D21"

def node_text(s):
  s = (s.replace("Crate$", "Crate ")
   .replace("Trait$", "Trait ")
   .replace("Type$", "T_")
   .replace("TypeParameter$", "α_")
   .replace("SubstitutionMap$", "Σ_")
   .replace("Substitution$", "σ_")
   .replace("PartiallySubstImpl$", "impl[Σ[α]]_")
   .replace("DefinedImpl$", "impl_")
   .replace("InstantiatedImpl$", "impl[Σ[α...ω]]_"))
  return s

def crate_subgraph(i, k, vs, subst_info):
  s = '  subgraph cluster_{} {{\n'.format(i)
  s += '    color = "{}";\n'.format(CRATE_COLOR)
  s += '    label = "{}";\n'.format(node_text(k))
  vs = [v for v in vs]
  vs.sort()
  for v in vs:
    if v in subst_info.map_to_subst:
      # Substitution maps are printed inside impls
      continue
    s += '    "' + node_text(v) + '"'
    if 'impl' in v.lower(): #
      # Print substitution map here
      s += format_impl_table(v, subst_info)
    s += ';\n'
  s += '    crate_{} [shape=point, style=invis];\n'.format(i)
  s += '  }\n';
  return s

# via https://spin.atomicobject.com/2017/11/15/table-rel-diagrams-graphviz/
def format_impl_table(impl, subst_info):
  f = ' [shape=plain, label=<'
  f += '\n      <table border="1" cellborder="0" cellspacing="0">{}'
  f += '\n      </table>'
  f += '\n    >]'
  s = '\n        <tr><td>{}</td></tr>'.format(node_text(impl))
  if impl in subst_info.impl_to_map:
    sm = subst_info.impl_to_map[impl]
    pairs = []
    for sub in subst_info.map_to_subst[sm]:
      p = subst_info.subst_to_param[sub]
      ty = subst_info.subst_to_type[sub]
      pairs.append((p, ty))
    pairs.sort()
    for p, ty in pairs:
      s += '\n        <tr><td>✓ {} := {}</td></tr>'.format(node_text(p), node_text(ty))
  else:
    todo = [node_text(tp) for tp in subst_info.unsubst_params[impl]]
    todo.sort()
    s += '\n        <tr><td>unsubst: {}</td></tr>'.format(' '.join(todo))

  return f.format(s)

def graphviz(deps_info, ownership_info, subst_info, impl_info):
  s = 'digraph synthetic {\n'
  s += '  compound=true;\n'
  c_to_i = {}
  for i, (c, vs) in enumerate(ownership_info.crate_contents.items()):
    c_to_i[c] = i
    s += crate_subgraph(i, c, vs, subst_info)

  for i1, i2 in impl_info.root.items():
    if i1 in impl_info.parent:
      i2 = impl_info.parent[i1]
    s += '  "{}" -> "{}";\n'.format(node_text(i1), node_text(i2))

  for i in set(list(impl_info.root.values())):
    t = impl_info.trait[i]
    s += '  "{}" -> "{}";\n'.format(node_text(i), node_text(t))

  s += '}'
  return s

def grab_tuple_pairs(f):
  tuples = f.findall('tuple')
  for t in tuples:
    atoms = t.findall('atom')
    assert(len(atoms) == 2)
    yield(atoms[0].attrib['label'], atoms[1].attrib['label'])

class OwnershipInfo:
  def __init__(self):
    self.crate_contents = {}
    self.is_owned = set()

  def handle_owner(self, f):
    for (elt, c) in grab_tuple_pairs(f):
      self.is_owned.add(elt)
      assert("Crate" in c)
      if c in self.crate_contents:
        self.crate_contents[c].add(elt)
      else:
        self.crate_contents[c] = {elt}

class DepsInfo:
  def __init__(self):
    self.deps = {}

  def handle_deps(self, f):
    for c1, c2 in grab_tuple_pairs(f):
      if c1 in self.deps:
        self.deps[c1].add(c2)
      else:
        self.deps[c1] = {c2}

class ImplInfo:
  def __init__(self):
    self.parent = {}
    self.root = {}
    self.trait = {}

  def handle_parent(self, f):
    for i1, i2 in grab_tuple_pairs(f):
      assert(i1 not in self.parent)
      self.parent[i1] = i2

  def handle_root(self, f):
    for i1, i2 in grab_tuple_pairs(f):
      assert(i1 not in self.root)
      self.root[i1] = i2

  def handle_trait(self, f):
    for i, t in grab_tuple_pairs(f):
      assert(i not in self.trait)
      self.trait[i] = t

class SubstInfo:
  def __init__(self):
    self.impl_to_map = {}
    self.map_to_subst = {}
    self.subst_to_param = {}
    self.subst_to_type = {}
    self.unsubst_params = {}

  def handle_subst_map(self, f):
    for impl, sm in grab_tuple_pairs(f):
      # One impl only has 1 substitution map
      assert(not impl in self.impl_to_map)
      self.impl_to_map[impl] = sm

  def handle_entries(self, f):
    for sm, s in grab_tuple_pairs(f):
      if sm in self.map_to_subst:
        self.map_to_subst[sm].add(s)
      else:
        self.map_to_subst[sm] = {s}

  def handle_param(self, f):
    for s, tp in grab_tuple_pairs(f):
      assert(not s in self.subst_to_param)
      self.subst_to_param[s] = tp

  def handle_unsubst_params(self, f):
    for i, tp in grab_tuple_pairs(f):
      if i in self.unsubst_params:
        self.unsubst_params[i].add(tp)
      else:
        self.unsubst_params[i] = {tp}

  def handle_type(self, f):
    for s, ty in grab_tuple_pairs(f):
      assert(not s in self.subst_to_type)
      self.subst_to_type[s] = ty


def default_main():
  tree = ET.parse('coherence.xml')
  root = tree.getroot()
  instance = root.find('instance')
  sigs = { sig.attrib['label']: sig for sig in instance.findall('sig') }

  subst_info = SubstInfo()
  ownership_info = OwnershipInfo()
  deps_info = DepsInfo()
  impl_info = ImplInfo()

  for f in instance.findall('field'):
    label = f.attrib['label']
    if label == 'subst_map':
      subst_info.handle_subst_map(f)
    elif label == 'entries':
      subst_info.handle_entries(f)
    elif label == 'type':
      subst_info.handle_type(f)
    elif label == 'param':
      subst_info.handle_param(f)
    elif label == 'type_params':
      subst_info.handle_unsubst_params(f)
    elif label == 'deps':
      deps_info.handle_deps(f)
    elif label == 'parent':
      impl_info.handle_parent(f)
    elif label == 'root':
      impl_info.handle_root(f)
    elif label == 'trait':
      impl_info.handle_trait(f)
    elif label == 'owner':
      ownership_info.handle_owner(f)

  print(graphviz(deps_info, ownership_info, subst_info, impl_info))

if __name__ == '__main__':
  default_main()