合金api解决方案集

Question

我有这个用合金写的简单模型：

module login

sig Email {}
sig Password {}

sig User {
    login: one Login
}

sig Login {
    email: one Email,
    password: one Password,
    owner: one User,
}

fact {
    all u:User | u.login.owner = u
}

assert a {
    all l:Login | one l.owner
    all u:User | one u.login.email
    all u:User | u.login.owner = u
}

check a for 3

如果我使用合金分析仪 GUI 运行它，它会显示：

没有找到反例。断言可能是有效的。 11 毫秒。

但如果我在我的 java 程序中使用 API 运行相同的模型，它会返回：

---结果---

不满意。

甚至没有显示 1 个解决方案。

谁能帮我发现问题？

下面是使用 API 的 java 代码：

A4Reporter rep = new A4Reporter();

            try {

                Module loaded_model = CompUtil.parseEverything_fromFile(rep, null, model.getModelpath());
                A4Options options = new A4Options();
                options.solver = A4Options.SatSolver.SAT4J;
                Command cmd = loaded_model.getAllCommands().get(0);

                A4Solution sol = TranslateAlloyToKodkod.execute_command(rep, loaded_model.getAllReachableSigs(), cmd, options);
                System.out.println(sol.toString());
                while (sol.satisfiable()) {
                    System.out.println("[Solution]:");
                    System.out.println(sol.toString());
                    sol = sol.next();
                }
                
            } catch (Err e){
                e.printStackTrace();
            }

谢谢

Answer 1

在这两种情况下都没有找到反例。

请注意，通过方法调用loaded_model.getAllCommands().get(0)得到的命令是check a for 3，也就是说，你让Alloy去寻找反例。

如果您想获得一个满足您的约束的实例 - 即，不是反例 - 您应该使用包含关键字 run 而不是 check 的命令。