首页 文章

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

提问于
浏览 次
2

我不明白合金中的事实是如何运作的 . 在这个小例子中有两个相互矛盾的事实，但谓词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

执行“运行testWithParameters for 10”Solver = sat4j Bitwidth = 0 MaxSeq = 0 SkolemDepth = 1 Symmetry = 20 2910 vars . 240个主要变种 . 6294条款 . 14MS . 找不到实例 . 谓词可能不一致 . 为3ms .

执行“运行testWithoutParameters for 10”Solver = sat4j Bitwidth = 0 MaxSeq = 0 SkolemDepth = 1 Symmetry = 20 2602 vars . 220个主要变种 . 5499条款 . 14MS . . 找到 . 谓词是一致的 . 21ms .

执行“检查test_aset为10”Solver = sat4j Bitwidth = 0 MaxSeq = 0 SkolemDepth = 1 Symmetry = 20 2834 vars . 230个主要变种 . 6162条款 . 14MS . 没有找到反例 . 断言可能有效 . 为3ms .

执行“检查testWithoutSense for 10”Solver = sat4j Bitwidth = 0 MaxSeq = 0 SkolemDepth = 1 Symmetry = 20 2844 vars . 230个主要变种 . 6191条款 . 13毫秒 . 没有找到反例 . 断言可能有效 . 7毫秒 .

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

alloy

1 回答

  • 3

    看一下 testWithoutParameters 的解决方案：set A 总是为空 . 对于空集，通用量化公式总是如此，因此矛盾并不重要 .

    另一方面， testWithParameters 包含 A 中至少有一个元素的隐含事实：参数 a . 但是没有 a 能够解决矛盾的事实，所以这个谓词没有解决方案 .

    编辑：找不到 testWithoutSense 的反例，其原因相同 . 由于事实 Rule_1 和 Rule_2 是矛盾的，因此您的模型始终被约束为不包含 A 中的元素 . 空 A ，断言 testWithoutSense 是非常正确的 .

    回复于

相关问题