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。但无法弄清楚。

标签： javaalloydeclarative

Answer 1

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

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