有没有办法找到在合金中运行“没有实例找到”的原因？

Question

我用合金写过模型。但是，对于运行谓词来查找实例的某些条件失败，它说没有找到实例。我尝试增加约16个实例的绑定，但它没有找到任何实例。

有没有什么办法可以调试这个，这样我就可以看到哪些事实失败，导致Alloy无法找到实例？

谢谢！

Answer 1

如果您将默认坐标解算器更改为不含核心的minisat，则可以突出显示在同一个实例中不能满足的约束。

另一种可能的解决方案是逐个评论你的约束，直到分析产生一个实例，从而找出哪个约束可能会导致麻烦。

对于更具体的答案，请分享你的模型。