Kev*_*vin 3 formal-verification formal-methods formal-languages alloy
我用Alloy写了模型.但是,对于某些运行谓词以查找实例的条件失败,它表示找不到实例.我尝试将绑定增加到大约16个实例,但它没有找到任何实例.
有什么方法可以调试这个,这样我就可以看出哪些事实失败导致Alloy无法找到实例？
谢谢 !
如果将默认的sat解算器更改为具有不饱和核心的minisat,则可以突出显示在同一实例中无法满足的约束.
另一种可能的解决方案是逐个评论您的约束,直到分析产生一个实例,从而确定哪个约束可能导致麻烦.
如需更具体的答案,请分享您的型号.