Visualization for Alloy — what do you want?

Since there was a recent mention of visualization here, I thought it may be useful to open a discussion on that.

Some of you may know about Sterling, a visualizer for Alloy built by @tristan during his PhD under John Baugh at NCSU. Tristan is now a post-doc at Brown with @tim and me, where he’s continuing this work.

Sterling is a web-based visualizer for Alloy that introduces some additional features that aim to make your instances a little easier to work with and understand. Most notably, these include the ability to move nodes out of the rows in which they are initially placed, as well as consistent node placement when stepping through projections.

If you’d like to see some of these features in action, there’s a brief tour that includes a few video demonstrations. There’s also an online demo version with some built-in instances to explore, or you can upload an XML file from your own model (note that the evaluator is not functional in the demo, as it’s not connected to Alloy!).

The Sterling visualizer is rather portable, and can be used to visualize Alloy-like data regardless of the source. We are using it in another tool at Brown (which we’d like to publicize soon).

This thread seems like a great place to open up a visualization discussion and to coordinate efforts for those of us who are working on visualization related tools. So let’s start with two questions:

  • What are some features you would find useful in an Alloy visualizer?
  • Is a directed graph representation good enough for your needs, or are there other visual representations that might be better (tables, text, something custom)?

For those who are also working on visualization tools:

  • What visualization problems are you addressing, and what impact will your tools have on the broader Alloy community?

We know @DanielJackson has a student working on visualization; we’d love to hear from others with interests as well.


Mine may have been the mention of visualization you are referring to. I never use it, believing (rightly or wrongly) from past experience that my models are too complex. If anyone is interested, I have a large set of visualization problems to offer! The material is in 3 or 4 files, which I could post if there is a way to do that, or email them on demand.

1 Like

@pamela I would love to take a look if you’re willing to share! It’s all too easy for me to fall into the habit of using the same models over and over during development, so adding diversity will really help me (and everyone else working on vis!) to create well-rounded tools. I’m not sure if it’s possible to attach files to posts here – if not, could you email them to me at Thank you!

1 Like

I have prepared a zip file of materials I can email to anyone who is interested.

1 Like

Good to know that @tristan will continue this interesting work with you and @tim.

As Electrum is going to be merged into Alloy in the near future (giving rise to Alloy 6), I think an important requirement is to address navigation in traces. I am quite fond of the possibility to see two consecutive states side-by-side, but it could be improved:

  • An obvious improvement is to be able to spot differences between two consecutive states easily.
  • The issue of placement is quite important too, and quite convoluted: some nodes should -ideally- not move between consecutive states, some should probably. E.g. a (fixed) location vs a message.
  • Also, as traces are infinite but represented as lasso traces, you may want a node to appear at position p in a given state but in position p’ != p in a future state, even though these states happen to be represented by the same index in the lasso.

Apart from time-related issues, I can think of these topological issues:

  • a circular layout is nice in the (large) domain of ring-based protocols (I guess there are other applications)
  • Alloy is good to model some architectural stuff, but note that nice to render it: one misses hierarchical components and component ports (as in the diagram here, from elkjs/sprotty).

Finally, I’d love such a framework to also be usable without Alloy (as you seem to indicate), using a simple API and nice FFI (to use it with my favorite language, the name of which doesn’t start with J).

Hope I haven’t been off-topic!

1 Like

These are all good comments, thanks.

We agree traces are critical. In the short term we’ve decided to NOT focus on traces (“focus” meaning, they will “work”, but not necessarily “natively”) because we are already thinking hard about issues like

  • multiple states side-by-side (even for trace-less systems)

  • helping people see differences

The two are related. t’s actually a more complicated problem than most people give it credit for, because ultimately it comes down to cognitive/perceptual factors; a few hacks and arguing about colors is not at all guaranteed to achieve the intended effect.

Stability of nodes is something Tristan has already been thinking about and working on. This also relates to things like node-naming (what does stability “mean” otherwise).

Starting last fall Tristan made efforts for Sterling to be used stand-alone, which is how we’re able to call it from my favorite language, which also does not begin with J. None of my favorites do, in fact. <-;

Coming into this thread a bit late, but wanted to make some comments. First of all, thank you Tristan for this excellent work, and Shriram for opening this important discussion. Second, a few thoughts about the current state of Sterling:
– Is there a theme-like facility for saving customizations? I believe that’s critical, because it amortizes the cost of editing the customization across sessions. It would be even better to be able to save styles that can apply to different models.
– The diagrams (and especially the textual labels) look slightly blurry in my browser.
– Is it possible to change the font? That would be a priority for me.
– I wish labels didn’t collide.
– When you select a node or edge, it would be nice to select the appropriate field in the form to edit it; I know this is hard (and not always even unambiguous)
– In the Alloy viz, we switch the text color from dark to light when the fill is switched from light to dark
– When you adjust the layout, the graph sometimes moves off screen
– I expected the table layouts to adjust alignment within tables, not of tables themselves within window: wouldn’t you always want them centered in the window, eg?
– Undo is a feature missing from the Alloy viz that would be really nice