在合金中测试特定解决方案

Question

我在我的.als文件中定义了一些约束条件，但是当我点击执行时，找不到解决方案。我有一个特定的解决方案，我怀疑“应该”的工作，但显然失败的原因只有合金可以发现的一些晦涩的理由。

我想要的是将我提出的解决方案手动输入Alloy Visualiser，然后要求Alloy告诉我哪些约束被违反。这可能吗？

Answer 1

我要做的第一件事就是运行Unsat Core来强调不一致性。那么你可能会通过将约束从事实转化为谓词来削弱模型;您可以直接在评估程序中评估谓词和函数。还要注意的是，合金分析仪认识到构建实例公式和表格

r = a -> b + c -> d 

合金不会让你只要输入一个实例，并对其进行评估，但是他们优化例如那些。