约束语法谓词和断言答案

【问题标题】：Constraints syntax a predicate and in an assert约束语法谓词和断言
【发布时间】：2014-01-30 08:06:18
【问题描述】：

我想知道在谓词中使用的约束语法是否与在断言中使用的不同。

约束all disj x1,x2:X | x1 =x2 在执行时会给出不同的结果谓词和断言。

例如，假设以下模型：

sig A {}

sig B {x: one A}

assert S1 
{all x1,x2: x | x1 = x2}

检查 S1 是否有 2 - 反例作为 x1 和 x2 的非等价实例

assert S2
{! (all x1,x2: x | x1 = x2)}

检查 S2 是否为 2——高阶量化误差

pred P1 
{(all x1,x2: x | x1 = x2)}

run P1 for 2 -- higher-order quantification error

pred P2
{! (all x1,x2: x | x1 = x2)}

run p2 for 2 -- 生成 x1 和 x2 的非等效实例

为什么有些约束是可以量化的，而它们的否定却不是，反之亦然！

谢谢

阿卜杜拉·雷汉

【问题讨论】：

标签： alloy

【解决方案1】：

在所有这 4 个示例中，您都有一个高阶量词：您正在尝试对二进制字段 (x: A -> B) 进行量化，因此当您说 all x1, x2: x | ... 时，它的意思是“对于所有二进制元组 x1 和x2 从二元关系 x" 中得出。合金是一阶的，通常不能处理高阶的东西。在某些情况下它不会抱怨的原因是它能够“skolemize”量词，因此它不必检查任何大于 1 的 all 元组.

例如，当您说check S1 时，您是在询问Alloy 是否存在适用于所有二进制元组的东西；由于 Alloy 是一个有界模型查找器，它会尝试通过找到一个 single 这样的元组来反驳这一点——其中没有更高的顺序，所以这种情况将工作。当您说“检查 S2”时，您是在询问 Alloy 是否对所有二进制元组都适用某些东西是不正确的，因此要反驳 Alloy 实际上必须检查主体是否适用于每个这样的二进制tuple---那是高阶，Alloy 做不到。

我不知道您是否打算首先进行这种高阶量化。只是猜测，也许您想要的只是all b: B, a: b.x | ...，它是一阶的并且可以正常工作。

【讨论】：