与合金中矛盾事实的一致性检查

Question

我不明白 Alloy 中的事实如何运作。在这个小例子中，有两个相互矛盾的事实，但谓词 testWithoutParameters 找到了一个实例（不是预期的），而谓词 testWithParameters 却没有（预期的）。这两个断言都没有在应该这样做时找到反例。我的解释中的错误在哪里？代理代码和执行的输出。

sig A{
    aset: set B
}

sig B{
    bset: set B
}

fact Rule_1{
    all a: A |
    #a.aset < 3
}

fact Rule_2{
    all a: A |
    #a.aset > 3
}

pred testWithoutParameters[]{
    all a:A |
    #a.aset = 3
}

pred testWithParameters[a:A, b:B]{
    #a.aset = 3
}

assert test_aset{
    all a:A |
    {
        #a.aset = 3
    }
}

assert testWithoutSense{
    all a: A |
    #a.aset > 3 and #a.aset < 3
}

run testWithParameters for 10
run testWithoutParameters for 10
check test_aset for 10
check testWithoutSense for 10

执行“Run testWithParameters for 10” Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2910 个变量。 240 个初级变量。 6294 条。 14 毫秒。 未找到实例。谓词可能不一致。 3 毫秒。

执行“Run testWithoutParameters for 10” Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2602 个变量。 220 个初级变量。 5499 条。 14 毫秒。 .成立。谓词是一致的。 21 毫秒。

执行“检查 test_aset 是否为 10” Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2834 个变量。 230 个初级变量。 6162 条。 14 毫秒。 没有找到反例。断言可能是有效的。 3 毫秒。

执行“检查 testWithoutSense for 10” Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2844 个变量。 230 个初级变量。 6191 条。 13 毫秒。 没有找到反例。断言可能是有效的。 7 毫秒。

执行了 4 个命令。结果是： #1：没有找到实例。 testWithParameters 可能不一致。 #2： .testWithoutParameters 是一致的。 #3：没有找到反例。 test_aset 可能有效。 #4：没有找到反例。 testWithoutSense 可能是有效的。

Answer 1

查看testWithoutParameters 的解决方案：集合A 始终为空。普遍量化的公式对于空集总是正确的，所以矛盾并不重要。

另一方面，testWithParameters 包含一个隐含的事实，即A 中至少有一个元素：参数a。但是不可能有满足矛盾事实的a，所以这个谓词没有解。

编辑：由于相同的根本原因，没有找到testWithoutSense 的反例。由于相互矛盾的事实Rule_1 和Rule_2，您的模型始终被限制为在A 中不包含任何元素。对于空的A，断言testWithoutSense 是微不足道的。