java - 如何将 Sig 从 Alloy 传递到 Java 并从 Java 执行合金模型

Question

我构建了一个合金模型，其中放置了我所有的系统逻辑。我想做一个大规模的分析。为此，我的逻辑是使用 Java 读取数据文件，然后将这些数据传递给 Alloy 以检查它们是否满足我在 Alloy 中定义的约束。为此，我的逻辑是使用这些数据创建 sig 对象并将其传递给 Alloy。

由于我的系统模型很复杂，我尝试使用以下代码总结我的问题-

sig A{
val: Int
}

sig B{
chunk: Int
}


fact {

    A.val > 10 && A.val < 15
}

现在，我想传递以下 sig 对象并从 Java 运行命令。

sig C{

name: String
}

run {} for 4

我如何传递该代码？我正在关注此链接 https://github.com/ikuraj/alloy/blob/master/src/edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java .但无法弄清楚。

Answer 1

目前有分行pkriens/api正在进行中，这使得这很容易。查看 classic test 中的测试用例项目。

我们正在努力尽快(在 2019 年底之前)将其集成到 master 分支中。