使用 Alloy API 为 alloy 分析器提供自定义实例

Question

我刚刚阅读了《软件抽象》一书，非常喜欢 Alloy 它的预期用途。但我想将它用于超出其预期目的的用途。创造性地思考，我想使用 Alloy 在从真实数据推断的模型实例中找到反例（断言检查）。是否可以针对您自己的数据实例使用 Alloy API？我希望底层 API 足够模块化，这样我就可以编写自己的工作流程，而无需详细了解整个系统。如果有这方面的例子，我将不胜感激。谢谢。

Answer 1

使用 Alloy java API，您可以轻松地计算实例中的表达式。

使用 CompUtil class.
然后检索您感兴趣的实例（之前已保存在 xml 文件中），如下所示：A4SolutionReader.read(module.getAllReachableSigs(), new XMLNode(new File("full/path/to/yourInstance.xml"))) ;
最后使用您刚刚获得的 A4Solution 对象的 eval(ExprVar e) 方法来计算实例中的表达式。（您需要使用 computil class 中的方法 parseOneExpression_fromString 从字符串中获取 ExprVar 对象。）

如果您不愿意使用 API，还有另一种方法可以仅使用分析器来完成您想做的事情。就是过度约束你原来的模型，只有你感兴趣的实例才能符合它。然后你只需要检查你对这个模型的断言。

一个关于如何约束模型的小例子：

假设你有一个模型：

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

并且您对实例感兴趣:

A:{A[=11=],A}
B:{B[=11=]} 
a:> (B[=11=],A[=11=])
C:{}

那么您的过度约束模型将是：

//=== 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.   
}

使用 Alloy API 为 alloy 分析器提供自定义实例

Using Alloy API to provide custom instances to alloy analyzer

alloy