DOT graph generation via CLI wrapper

[swamp-agr]

Hello,

Hope you are doing well.

Summary

Please find attached the link to CLI script for generating DOT files for model instances without triggering any GUI at all: https://gist.github.com/swamp-agr/560f0d9bf8dc034f99d6055a5a197285 (logic located below L2040).

Comments are welcome.

Motivation

• I wanted to include Alloy as a new "backend interpreter" for my telegram bot (https://github.com/swamp-agr/proof-assistant-bot/ sorry, it is not there yet. Upd. it is there! now it is generating images and GIFs out of model instances) and, therefore, to provide basic IRC-like interface to it.
• Meantime I realised that Alloy by default is a GUI app and it was not convenient to use it on server remotely.
• So I decided to play with Alloy API and examples and see where it leads me.

Implementation

Disclaimer: I am not Java programmer and, to be honest, I am not familiar with OOP. I wrote some Java code in the past but it was too long ago. Now I am using Haskell for my job and also in my spare time.

• I took your example ExampleUsingTheCompiler in the beginning.
• I managed to detach Alloy VizState (see BackgroundState) from the main AWT UI thread and its event loop.
• In order to generate graph I had to modify StaticGraphMaker (see SilentGraphMaker). However, some Java Swing/AWT UI primitives forced CLI script to make an attempt to render GUI window. Of course, without parent JPanel it didn't work out and when script terminated the window was closed. Anyway, it was annoying and it impacted the overall time of script.
• It turned out that DotStyle and DotShape have javax.swing.Icon as private class propertiy and they force UI window rendering because of Icon usage.
• Also all the stuff below that used in Graph, GraphNode and GraphEdge classes to draw diagram on JPanel triggered UI window rendering:

import java.awt.BasicStroke;
import java.awt.Font;
import java.awt.FontMetrics;
import java.awt.Graphics2D;
import java.awt.Polygon;
import java.awt.Shape;
import java.awt.font.FontRenderContext;
import java.awt.font.GlyphVector;
import java.awt.geom.Line2D;
import java.awt.geom.RoundRectangle2D;
import java.awt.geom.CubicCurve2D;
import java.awt.geom.GeneralPath;
import java.awt.geom.Rectangle2D;
import java.awt.image.BufferedImage;

Result

By making local copies of mentioned classes and removing all that Swing/AWT stuff (except java.awt.Color) I was able to draw DOT file and produce the plot.

Before:

After:

Conclusions

• Since all those classes were final and their internals were private I cannot easily extend/implement those classes to disable GUI and its primitives. The only way for me was to rewrite the code to get DOT as soon as possible. So now I am able to continue working on adding Alloy (via its very primitive CLI Wrapper) to the bot.
• I do realise that if you want to have the feature in the upstream you cannot just use the code from my gist. You will need some Graph interfaces and separate implementations for GUI/DOT/PDF/....
• I have only 15 minutes per day and with my previous experience it will take more than three months to prepare the patch for you. And I think, two more months to pass the review for pull request. I am afraid, I cannot be any more help to you.

Nevertheless, thank you for your great work!
It was quite fun to play with the Alloy app and with Alloy API too. 😄

Feel free to close the issue if you decide not to have such a feature in upstream.

Best Regards,
Andrey

[swamp-agr]

Since yesterday Alloy 6 is generating images (for model instances) and GIFs (for temporal models) via both Telegram Bot interface and CLI Wrapper described in a previous message.

You can probably add it to your show cases.