0

我真的很困惑为什么我的以下断言总是有一个反例。

//assertions must NEVER by wrong
assert Symmetric{
all r: univ -> univ | some ~r iff (some x, y: univ | x not in y and y not in x and 
                                  (x->y in r) and (y->x in r))
}

check Symmetric

反例总是显示 1 univ set 中的元素。然而，这不应该是这样，因为我指定会有一些 ~r iff x 不在 y 中并且 y 不在 x 中。唯一的元素不应该满足这个陈述。

然而，为什么该模型总是对我的断言提出反例呢？

---INSTANCE---
integers={}
univ={Univ$0}
Int={}
seq/Int={}
String={}
none={}
this/Univ={Univ$0}
skolem $Symmetric_r={Univ$0->Univ$0}

非常感谢一些指导！

4

1 回答 1

1

在 Alloy 中，断言用于检查逻辑语句（模型的属性）的正确性，而不是指定应始终保留在模型中的属性。所以你没有指定

如果 x 不在 y 中且 y 不在 x 中，将会有一些 ~r

r相反，您问 Alloy 对于所有二元关系,和 Alloy是否是真的some ~r iff x not in y and y not in x [...]，而 Alloy 回答说这不是真的，并给了您一个该属性不成立的具体示例（反例）。

其他几点

  • some ~r并不意味着“r 是对称的”；它只是意味着转置r是非空的，这是不一样的。如果二进制关系等于它的转置，则它是对称的，所以你可以写r = ~r来表达它；

  • 而不是some x, y: univ | x not in y and y not in x and [...]你可以等效地写some disj x, y: univ | [...];

  • however, that some expression doesn't really express the symmetry property, because all it says is that "there are some x, y such that both x->y and y->x are in r"; instead, you want to say something like "for all x, y, if x->y is in r, then y->x is in r too".

于 2012-11-26T15:37:47.153 回答