使用用于Java的Alloy API动态修改Alloy模块

Question

我正在使用Alloy API for Java，从文件中读取模块，执行其命令，并检查其可满足性。如果不满意，我想对模块进行更改，特别是放宽给定事实集内的约束。例如，如果我在模块中有以下事实

事实S0 {a：AS | a.score> = 80}

然后，我希望能够更改该事实以具有不同的分数阈值。按照API示例，我正在Java中像这样加载模块：

CompModule world = CompUtil.parseEverything_fromFile（rep，null，fullFileName）;] >>

然后，我可以调用world.addGlobal（“ S0”，Expr），并且可以将原来的事实替换为新的事实。但是，尚不清楚如何将事实创建为Expr传递给此方法。 API中没有Fact类，并且我还没有找到有关如何将事实创建为Expr的示例或API描述。

我正在使用Alloy API for Java，从文件中读取模块，执行其命令，并检查其可满足性。如果不满意，我想对模块进行更改，特别是放宽...

Answer 1

这也是我的问题。有人解决了吗？