Alloyapi解集

Question

我有一个用 Alloy 编写的简单模型：

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

如果我运行使用 alloy 分析器 GUI，它说：

No counterexample found. Assertion may be valid. 11ms.

但是如果我运行与我的 java 中的 API 相同的模型编程它 returns:

---OUTCOME---

Unsatisfiable.

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

任何人都可以帮我检测问题吗？

java 中的代码使用 API:

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.[=14= 的命令]

Alloyapi解集

Alloy api solution set

java

model

alloy