合金中的多态空关系？

Question

我运行了一个 Alloy 命令，该命令涉及为一些存在物寻找证人，比如这个：

pred foo { 
  some x, y : E -> E | 
    baz[x,y] || qux[x,y] 
}

Alloy 提出了一个模型，其中foo 为真。我在 Visualizer 中查看模型，发现 y 恰好是空关系。我想深入挖掘模型，看看baz 或qux 是否正确。所以我启动了评估器窗口并输入baz[$foo_x, ???]。但是我可以为??? 输入什么内容？由于y 为空，因此没有名称为$foo_y 的变量。输入none 或{} 会出现类型检查错误。

Alloy 是否提供可用于任何类型的空关系？或者有什么方法可以让y 见证人即使它是空的？

Answer 1

我相信 baz[$foo_x, none->none] 应该可以工作。关系 none 的元数为 1，通过使用叉积，您可以获得所需元数的空关系。对此的解释可以在 Jonathan Edwards、Daniel Jackson 和 Emina Torlak 的论文“A Type System for Object Models”中找到。