alloy - 如何枚举所有解决方案？

Question

我想使用 Alloy Analyzer 从给定范围内的谓词中枚举所有解决方案。Alloy 是否支持此功能？如果可以，如何从命令行调用它？

谢谢

Answer 1

这是执行此操作的代码。在此示例中，您编写了一个常规 Alloy 模型文件（在其中指定范围）并使用此代码运行它，即为模型文件中存在的每个命令枚举所有解决方案。

public void run(String filename) {
    A4Reporter rep = new A4Reporter();
    Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
    A4Options options = new A4Options();
    options.solver = A4Options.SatSolver.SAT4J;
    // options.symmetry = 0; // optionally turn off symmetry breaking
    for (Command command: world.getAllCommands()) {
        // Execute the command
        A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
        while (sol.satisfiable()) {
            System.out.println("[Solution]:");
            System.out.println(sol.toString());
            sol = sol.next();
        }
    }
}

Answer 2

是的，Alloy 确实允许您在有限的宇宙中列举所有“可能的”解决方案。但是，它使用对称破坏（SB）算法来破坏所有的对称性（嗯，大部分）。因此，您将无法列举每一个可能的解决方案。另一方面，即使您可以关闭 SB，您也可以获得相当数量的模型实例。它最终会终止，但您只是不知道何时终止，这实际上取决于您的范围。我记得在 jar 文件（ExampleUsingTheCompiler.java 和 ExampleUsingTheAPI）中，有一些关于使用 API 调用合金的示例，您可以使用它来枚举您的解决方案。