How can I run Alloy in command line?

Questions
1

I have version 6.1.0.202111031525 which, as I understand, is fairly recent.

Unfortunately I must say that the GUI is not suitable for me. I have a finely tuned emacs installation that I should rather edit my Alloy code with. I can then open a file in Alloy’s GUI and press some buttons to make it check my models — but this is far from an ideal working environment.

With other languages, I can write a one line shell script that watches for changes in my source code and runs the compiler automatically every time I save my project. I should like to have a similar arrangement with Alloy. How can I achieve it? Ideally I should like for Alloy to check the model, print the instances and also save their graph representations to files that I can view with a viewer of my choice.

I see that there are some command line possibilities:

% alloy --help --quit
Usage: alloy [options] file ...
  //  -d/--debug                  set debug mode
  -h/--help                   show this help
  -q/--quit                   do not continue with GUI
  -v/--version                show version

So, I can do like this:

% alloy --quit example.als

— But this does not seem to do anything. Truly it will exit successfully even if I give it a random file. It does not even check the syntax!

2

Here are two ways of integrating scripts with Alloy without writing any new Java code.

#1 There are some other classes in the Alloy jar that expose a main method that might be useful. Here’s an example of abusing the ExampleCompilingFromSource class to evaluate a model that has been packed into a single command line argument:

$ java -cp org.alloytools.alloy.dist.jar edu.mit.csail.sdg.alloy4whole.ExampleCompilingFromSource "sig Room {link: set Room } {#link < 4} fact { some home:Room | home.*link = Room } run {} for exactly 5 Room"

#2 You can use Alloy’s Java APIs directly from scripting languages using a foreign function interface library. Here’s an example of calling into the Alloy jar from Python using JPype:

1 Like
3

Alloy from Python is just what I needed.

Thank You!

Evelyn Mitchell

5

Hello everyone. Could you share your emacs setup for alloy?

I’m new to alloy and I’m probably missing something, but only I see here a way to generate an instance just like I pressed the execute button. How to emulate the new button?

And how to get png or dot from generated data?

6

As far as I understand, the solution in the linked example is of type A4Solution, and it has a next() method.

https://alloytools.org/documentation/alloy-api/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.html#next()

And it seems there’s no prev() method. But the good news is we can just log all the solutions we’ve seen so far.

Now, how to convert an instance to png or dot?