Alloy 的谓词类型检查中的行为可能不一致？

Question

对任何新手错误表示歉意 - 这是我第一次在这里发帖。

我不确定这是否是一个错误，或者是 Alloy 类型检查中某些微妙之处的结果。在下面的示例中，我希望谓词“奇怪”是不一致的，因为 B 和 C 是不相交的集合。但是，Alloy（4.2 版）声称可以找到谓词的模型。它显示的模型看起来不对。例如，有一个模型只包含一个原子 B$0，标记为见证 $strange_a。在这个模型中，Evaluator 告诉我 isB[B$0] 是真的，并且 isC[B$0] 给了我一个类型错误，正如预期的那样。然而，奇怪[B$0] 的计算结果为真。我使用的合金代码是：

abstract sig A {}

sig B, C extends A {}

pred isB [b:B] { }

pred isC [c:C] { }

pred strange [a:A] {isB[a] and isC[a]}

run strange

Answer 1

你是对的：这令人惊讶。 Alloy 的类型检查器使用谓词和函数的 decls 来检查它们的主体，但它不会将它们作为约束强加，除非谓词或函数在顶层运行。我们这样做是因为我们无法在所有使用上下文中找到这些约束的连贯语义（例如，当在量词内或在否定条件下调用谓词时）。