Using Alloy API to provide custom instances to all

问题:

I've just read the Software Abstractions book and really like Alloy for its intended purpose. But I'd like to use it for more than its intended purpose. Thinking creatively, I'd like to use Alloy to find counterexamples in model instances extrapolated from real data (assertion checking). Is it possible to use the Alloy API against your own data instances? I'm hoping that the underlying API is modular enough that I can code my own workflow without having to learn the whole system in detail. If there are examples of this, I would appreciate the pointers. Thank you.

回答1:

Using the Alloy java API, you can easily evaluate expressions in an instance.

1. Get the module the instance has been generated from using one of the methods of the CompUtil class.
2. Then retrieve the instance you are interested in (that has been previously saved in an xml file) as follows : A4SolutionReader.read(module.getAllReachableSigs(), new XMLNode(new File("full/path/to/yourInstance.xml"))) ;
3. Finally use the eval(ExprVar e) method of the A4Solution object you just obtained in order to evaluate an expression in your instance. (you will need to use the method parseOneExpression_fromString from the computil class to get an ExprVar object from a String.)

If you are reluctant to use the API, there is another way of doing what you want to do solely using the Analyzer. It is to over-constraint your original model such that only the instance you are interested in can conform to it. You then just have to check your assertion on this model.

A small example on how to constraint your model :

Suppose you have a model :

sig A{
} 
sig B{
  a:A
}
sig C{}

and you are interested in the instance :

A:{A$0,A$1}
B:{B$0} 
a:> (B$0,A$0)
C:{}

Then your over-constrained model would be :

//=== model ====
abstract sig A{
} 
abstract sig B{
  a:A
}
abstract sig C{}

//==== instance ===
one sig A_0,A_1 extends A{}
one sig B_0 extends B{
}{ 
   a=A_0
}

fact {
  no C // should be specified explicitly as the Alloy analyzer will instantiate abstract signatures if they are not inherited.   
}