alloy - 有没有办法找出在 Alloy 中运行时导致“未找到实例”的原因？

Question

我已经使用合金在模型中编写。但是，在某些情况下，运行谓词以查找实例失败，并且它表示找不到实例。我尝试将绑定增加到大约 16 个实例，但它没有找到任何实例。

有什么方法可以调试它，以便我可以看到哪些事实失败导致合金无法找到实例？

谢谢 ！

Answer 1

如果您将默认 sat 求解器更改为具有 unsat 核心的 minisat，则可以突出显示在同一实例中无法满足的约束。

另一种可能的解决方案是逐个注释您的约束，直到分析产生一个实例，从而确定哪个约束可能会导致麻烦。

如需更具体的答案，请分享您的模型。