【发布时间】：2017-10-29 06:39:14
【问题描述】：
我使用合金在模型中编写。但是，在某些情况下，运行谓词以查找实例失败，并且表示找不到实例。我尝试将绑定增加到大约 16 个实例，但它没有找到任何实例。
有什么方法可以调试它，以便我可以看到哪些事实失败导致 Alloy 无法找到实例？
谢谢！
【问题讨论】：
标签： alloy formal-languages formal-verification formal-methods
【发布时间】：2017-10-29 06:39:14
【问题描述】：
如果您将默认 sat 求解器更改为具有 unsat 核心的 minisat，则可以突出显示在同一实例中无法满足的约束。
另一种可能的解决方案是逐个注释您的约束，直到分析产生一个实例，从而确定哪个约束可能导致问题。
如需更具体的答案，请分享您的模型。
【讨论】：
-
如何更改 SAT 求解器？我是否从选项选项卡中选择它？但是对我来说，除了 SAT4J 之外，它没有显示任何其他选项。
-
是的，其他求解器作为二进制文件存在于 jar 文件中。它们可能与您正在运行的系统不兼容。因此，我建议您使用第二种选择试试运气，如果没有任何结果，请随时分享您的模型