Is it possible to group "container nodes" in the visualizer?

I’ve been toying around with using Alloy for understanding complex interactions between programming language features (it’s been fun so far!). Typical programming language constructs have lots of “contains” relationships (e.g. a type is defined inside a module).

Uniformly representing all of these using arrows gets messy in the visualizer, and it takes a bunch of hovering + projections to better understand what is going on. Here is an example:

The details aren’t super important, but the point is that some of the arrows are about contains relationships. For example, if I could have a big box with the label Crate0, that box would contain the boxes for T0, impl[Σ[α..ω]]1. Similarly for Crate1 and so on.

At the same time, just selectively hiding the arrows is not a solution (I’ve already hidden the non-essential ones above), because it is hard to understand the relationships otherwise.

GraphViz (for example) supports grouping nodes together using the subgroup construct (unfortunately, I don’t think it is flexible enough to support intersection between groups, but that’s OK for my use case).

Is it possible to do something similar in Alloy natively?

If not, any suggestions for how to develop a custom visualization? I took at look at Sterling which looks like it consumes XML generated by Alloy. (via @shriram’s post: Visualization for Alloy — what do you want?). I suppose it should not be terribly hard to set up a file watcher + reloading script where I consume the XML and have it regenerate a custom diagram in a separate window; this would avoid having to dive into internals of the Alloy visualizer.

Example GraphViz visualization with subgroups from (posted in a separate comment since Discourse won’t let me post two media files in my first comment to the forum)

I just saw that GraphViz output is supported. After some manual tweaking, it looks like

This is still not easy as understand as it could be (I should probably “inline” the subst_map entries as α_n = T_m) but it seems like a good start in terms of direction. It might make sense to parse the graphviz directly since it’s a simple format.

I ended up writing a custom visualizer using GraphViz by consuming the XML output, in about 150 lines of Python code.

This seems like the best way to go, since it let me tailor a bunch of things such as showing certain relations in only certain situations.

Nice, it may be useful to others too: how generic is your script? Can you share it?

It’s quite special-cased for my use case, but perhaps the overall structure/skeleton might be useful if you don’t write much code day-to-day? I’ve posted it as a gist here: Example of converting Alloy's XML output to GraphViz with clusters (containers/groups) and tables. · GitHub

1 Like