Dienstag, 4. Dezember 2012

How to run Alloy from the command line

I've recently started evaluating my Alloy models by script. This is a challenge, because Alloy does not offer simple command line parameters in order to be run from promt. However, there is a way, and Felix Chang tells us:
You can invoke it like this: (it will execute every command
in every Alloy file you specified, and if an assertion
has a counterexample, it will show the values of every sig
and every relation in that counterexample)
Here's a sample promt:
java -cp alloy4.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler file1.als file2.als
And the same thing for Alloy 4.2:
java -cp alloy4.2-rc.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler file1.als file2.als
This is actually a different program and it's important to account for the differences.

What the output means

If you've used the Alloy Analyzer to check assertions, you expect the it to tell you about counter-examples. So suppose we have an assertion that we think is valid. Running Alloy from the command line, we get this:

>java -cp alloy4.2-rc.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler example.als
=========== Parsing+Typechecking example.als =============
============ Command Check exampleCheck for 4: ============
---OUTCOME---
Unsatisfiable.
We expected that the response would be "may be valid" and not "unsatisfiable". From Alloys perspective, the two are actually the same thing. When Alloy goes looking for counter-examples, it does not examine the facts F and assertion A in the way they're written it down. The result of solving {F, A} would always be SAT and that doesn't tell us anything about whether A is valid. Instead, Alloy takes the negation  ¬A and evaluates {F, ¬A}. If this yields SAT, Alloy has found a counter-example and will display it:

>java -cp alloy4.2-rc.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler example.als
=========== Parsing+Typechecking example.als =============
============ Command Check badExampleCheck for 4: ============
---INSTANCE---
integers={}
univ={IID$0, Interface$0, Interface$1, Component$0}
…
this/IID={IID$0}
this/LegalInterface={}
this/Interface={Interface$0, Interface$1}

So to conclude this section, these responses correspond to each other:

Alloy Analyzer 4.2ExampleUsingTheCompiler class
Counterexample found. Assertion is invalid.---INSTANCE---
No counterexample found. Assertion may be valid.---OUTCOME---
Unsatisfiable.

Why it works

As a reminder, the usual call to Alloy looks like this:
java -jar alloy4.jar
So what does that do? This command will simply load the given .jar file and look for the "Main-Class" that is given in the jar's manifest. In Alloy's case that class is "edu.mit.csail.sdg.alloy4whole.SimpleGUI". So instead of letting Java decide which class to run, we can explicitly tell it to:
java -cp alloy4.jar edu.mit.csail.sdg.alloy4whole.SimpleGUI
 This call starts Alloy analyzer GUI. And we now notice the difference to the command line prompt: In order to run from the command line, we swap the "normal" Main-Class for one that takes command line parameters. And this class is called "ExampleUsingTheCompiler".

Kommentare:

  1. Can we use Alloy command line to enumerate all solutions. I mean that I need to enumerate all instance solutions.
    Thank you

    AntwortenLöschen
  2. No, you'll have to extend the class with your own code:

    Create a copy of the file edu/mit/csail/sdg/alloy4whole/ExampleUsingTheCompiler.java (for editing) and go to line 71. There you will find the variable "ans". It's an A4Solution object which represents a single instance solution. Call the method "next()" on this object to get the next instance solution like this:

    A4Solution anothersolution = ans.next();

    You can find the documentation for this method in the API here:

    AntwortenLöschen