如何评估合金源代码中的谓词？

【问题标题】：How to evaluate a predicate in Alloy source code?如何评估合金源代码中的谓词？
【发布时间】：2014-03-10 17:13:47
【问题描述】：

我的 Alloy 模型中有一个谓词，称为 LS，它获取一个称为 st 的 sig 实例。我试图在源代码中的一个名为 st$0 的 st 实例上评估这个谓词。我可以找到 A4Solution 类型的解决方案，称为 ans。但我不知道如何在这个解决方案上评估这个谓词。

【问题讨论】：

请贴出你已有的骨架代码，然后我可以帮你实现缺少的部分

标签： alloy

【解决方案1】：

以下是使用 API 评估谓词的一般方法

String fileName = "<file path to your alloy model>";
Module world = CompUtil.parseEverything_fromFile(rep, null, fileName);
A4Options opt = new A4Options();
opt.solver = A4Options.SatSolver.SAT4J;

// run the first command for the sake of this example
Command cmd = world.getAllCommands().get(0);
A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), cmd, opt);

// evaluate the first defined function/predicate applied to the first defined Sig
Func func = world.getAllFunc().get(0);
Sig sig = world.getAllSigs().get(0);
System.out.println(sol.eval(func.call(sig)));

【讨论】：